我正在我的实验室上使用 Isabelle/jEdit。
我的笔记本电脑有 4 个核心，即 4 个 CPU。但我在隔壁房间也有一台服务器计算机。服务器有超过20个CPU。
通常我会并行运行 sledgehammer 和 try，因为有时 try 结果会给出 sledgehammer 结果，而 sledgehammer 本身会失败(请参阅 my other question on this )。
所以我猜有相当多的进程可以并行运行。
但是，我无法在我的服务器上使用或运行 Isabelle/jEdit，因为服务器是“ headless ”的，因此没有安装 X 或窗口管理器。
所以我需要我的 Isabelle/jEdit session 将 sledgehammer 调用从我的 labtop 发送到我的服务器，在那里执行 sledgehammer。有点像我自己的 TPTP 系统。
这可能并且易于设置吗？
最佳答案
没有简单的方法可以从用户级别实现这一目标。但这里有一些想法:
您可以修改“src/HOL/Tools/ATP/scripts/remote_atp”(与 SystemOnTPTP 对话的脚本)以使用 super 欺骗服务器。
主要问题是并行性。在 jEdit 中，Sledgehammer 面板无法同时运行比它认为您的机器可以处理的线程更多的线程，即使某些线程大部分是远程运行的。如果您使用“sledgehammer”命令手动调用 Sledgehammer，您也许可以解决该限制，但我不确定。
顺便说一句，运行超过 4 或 5 个证明者对成功率的影响非常有限。
关于Isabelle:在运行 Isabelle/jEdit 的普通电脑之外的另一台机器上运行 sledgehammer，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22146480/