Isabelle:在运行 Isabelle/jEdit 的普通电脑之外的另一台机器上运行 sledgehammer

Question

我正在我的实验室上使用 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 系统。

这可能并且易于设置吗？

Answer 1

没有简单的方法可以从用户级别实现这一目标。但这里有一些想法:

1. 您可以修改“src/HOL/Tools/ATP/scripts/remote_atp”(与 SystemOnTPTP 对话的脚本)以使用 super 欺骗服务器。

2. 主要问题是并行性。在 jEdit 中，Sledgehammer 面板无法同时运行比它认为您的机器可以处理的线程更多的线程，即使某些线程大部分是远程运行的。如果您使用“sledgehammer”命令手动调用 Sledgehammer，您也许可以解决该限制，但我不确定。

顺便说一句，运行超过 4 或 5 个证明者对成功率的影响非常有限。