我一直在进行Isabelle 2019的 session ， session 变得有些大，有时我无法在8G RAM机器中使用isabelle build来构建它。但是，当我使用jEdit(运行isabelle jedit -d .)打开主理论文件时，该 session 的建立没有问题。
接下来，我提供一些更多的细节。
主要症状是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是一些数字。
最佳答案
遵循@ManuelEberl的建议，我在isabelle-users list中问了这个问题，关键是似乎PIDE(jEdit)使用的构建过程不像isabelle build命令那样并行。此答案中的所有信息均由M. Wenzel on the list提供。我引用:
这似乎是我一直在寻找的设置。
对于那些(像我一样)对isabelle工具包装的访问有限的人，请使用以下命令
isabelle options -l
将显示整个Isabelle系统的选项的完整列表。
关于isabelle - 使用 `isabelle`与jEdit建立 session ，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/59931542/