isabelle - 使用 `isabelle` 与 jEdit 构建 session

Question

我一直在 Isabelle 2019 session 上工作，该 session 变得有点大，有时我无法再使用 isabelle build 来构建它。在我的 8G RAM 机器中。尽管如此，当我使用 jEdit(运行 isabelle jedit -d .)打开主理论文件时， session 的构建没有问题。

How can I tune the building process so it works as smoothly as the graphical interface?

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

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

在开发中，调整使用 ML_OPTIONS至 "--minheap 5500"足以解决这个问题，但后来我们决定将 session 分成两部分(不再添加代码，只是更改 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 on the list 提供.我引用:

both PIDE and build are using multiple threads by default, but the overall profile of the parallel application comes out quite differently. E.g. in PIDE proofs are only parallel in terminal positions (e.g. by).

You can also try this:

isabelle build -o parallel_proofs=0

I.e. multithreading is enabled, but proofs are not forked.

这似乎是我正在寻找的设置。

对于那些(像我一样)对 isabelle 的接触有限的人工具包装器，命令

isabelle options -l

将显示整个 Isabelle 系统的完整选项列表。