[2/3] 你还真别说，DC-ROMA II 这台 RISC-V 笔记本上的 GPU 可用，而且 OpenCL 接口是工作正常的，虽然不知道具体性能如何，但有总比没有强。正所谓 “CPU 不够 GPU 来凑”，如果我能找到一个办法让 GPU 来参与 HOL 表达式的 β-规约（本质上就是个变量替换，可并行完成），那就完美了。 ​​​