使用 `isabelle` 与 jEdit 构建会话

Question

我一直在 Isabelle 2019 会议上工作，该会议已经变得有点大，并且在某些时候我无法再isabelle build在我的 8G RAM 机器上使用它来构建它。尽管如此，当我使用 jEdit（运行isabelle jedit -d .）打开主理论文件时，会话的构建没有问题。

如何调整构建过程，使其像图形界面一样顺利运行？

接下来，我将提供更多细节。

主要症状是 Poly/ML 过程在某个时刻停止；它并没有真正失败，但不会在合理的时间内终止（大约 20 分钟，当成功构建在我的计算机中需要 3' 时）。

在开发过程中，调整使用ML_OPTIONSto"--minheap 5500"就足以解决这个问题，但后来我们决定将会话分成两部分（不再添加代码，只是更改了 ROOT 文件），之后没有进一步调整解决了问题。另一方面，一台具有 16G RAM 的机器无需任何进一步设置就可以毫无问题地构建。

编辑。我检查了 jEdit 使用的选项；那些相关的（我相信）是--minheap 500 --gcthreads 0（最后一个是默认值）。我尝试了这些但没有成功。我还注意到 build 命令有一个不同的--eval Command_Line.tool0 (fn () => (Build.build "/tmp/isabelle-pedro/buildNNNNNNNNNNNNN"))选项，其中NNNNNNNNNNNNN有一些数字。

Answer 1

根据 @ManuelEberl 的建议，我在isabelle-users list中提出了这个问题，要点似乎是 PIDE (jEdit) 使用的构建过程并不像命令那样并行密集isabelle build。本回答中的所有信息均由列表中的 M. Wenzel提供。我引用：

默认情况下，PIDE 和 build 都使用多个线程，但并行应用程序的整体配置文件却截然不同。例如，在 PIDE 证明中，仅在终端位置平行（例如by）。

你也可以尝试这个：

isabelle build -o parallel_proofs=0

即启用了多线程，但未分叉证明。

这似乎就是我一直在寻找的设置。

对于那些（像我一样）对工具包装器接触有限的人来说isabelle，命令

isabelle options -l

将显示整个伊莎贝尔系统的完整选项列表。