isabelle - 在 Isabelle 中加载预编译的堆镜像

Question

已关注 how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle另一个建议是我为 Nominal 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)，则 Nominal2 包含的所有理论需要在 jEdit 中打开，您将在 jEdit 的“理论”面板中看到它们。

  例如，在下图中，Scratch 导入文件 AutoCorres，该文件又导入 MapExtra、Padding、BitOperations 等。如果我使用正确的 AutoCorres 堆，则不需要加载这些文件，因为它们已经被预编译到堆中:

  

即使 Isabelle 使用堆，它仍然需要在启动时将其加载到内存中。这通常需要几秒钟的时间，再加上 jEdit 本身的启动时间并不是特别惊人，这可能就是您所经历的。