在Isabelle中加载预编译的堆映像

Question

按照how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle和另一个建议，我为名义的伊莎贝尔创建了一个图像：

isabelle build -v -b -d . Nominal2

堆映像在~/..isabelle下面创建：

.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-linux/Nominal2

然后我开始

isabelle jedit -d /path/to/Nominal-distribution -l Nominal2

我预计这个系统很快就会加载一种理论，即从名义上进口一部分商品，但几乎花了一分钟时间。这是平常的吗？

Answer 1

构建堆映像的过程看起来是正确的。事实上，您实际上不需要isabelle build步骤，因为如果堆不存在或没有更新，isabelle jedit将自动触发构建。

您可以根据两个事实确定isabelle jedit是否在使用堆：

• 如果需要构建堆，您将看到第一次启动jEdit时弹出一个对话框，显示生成进度。这通常需要10秒到几个小时，这取决于需要构建的堆的大小。下面的屏幕截图显示了构建对话框的一个示例；在本例中，我正在构建Main堆：

​

• 如果它根本没有使用堆(例如，如果您忘记指定-l Nominal2)，则需要在jEdit中打开Nominal2包含的所有理论，您将在jEdit“理论”面板中看到它们。 例如，在下面的图像中，Scratch导入一个文件AutoCorres，然后导入MapExtra、Padding、BitOperations等等。如果我使用的是正确的AutoCorres堆，则不需要加载这些文件，因为它们已经被预编译到堆中：

​

即使Isabelle正在使用堆，它在启动时仍必须将其加载到内存中。这通常需要几秒钟的时间，当jEdit本身的启动时间并不特别惊人时，这可能就是你正在经历的事情。