如何使用持久堆图像在 Isabelle/jEdit 中更快地加载理论？答案

【问题标题】：How to use persistent heap images to make loading of theories faster in Isabelle/jEdit?如何使用持久堆图像在 Isabelle/jEdit 中更快地加载理论？
【发布时间】：2013-03-08 10:44:28
【问题描述】：

假设我有一个目录isabelle_afp，其中存储了很多理论。该目录是一个库，我不打算更改其中的文件。我想加快 Isabelle/jEdit 的启动时间（默认情况下，我当前的理论所依赖的 isabelle_afp 中的所有理论都是重新处理的）。

如何跳过这一步？ system manual 告诉我构建一个持久堆映像。最简单的方法是什么？

我怎样才能告诉 Isabelle/jEdit 加载这个堆图像？

【问题讨论】：

标签： jedit isabelle

【解决方案1】：

Isabelle2013 中的 Isabelle/jEdit 已经通过一种相对基本的机制负责构建堆映像，该机制在内部使用 isabelle build_dialog 工具（在引用的文档中有单独的条目）。

在不手动使用isabelle build_dialog 或isabelle build 电动工具的情况下，您有两种主要的可能性：

jEdit 对话框“Utilities / Options / Plugin Options / Isabelle / General”提供了一个“Logic”选项，并带有一个小工具提示，提示您必须在更改应用程序后重新启动它。这样做，堆映像将在重新启动时生成。
命令行选项-l，例如isabelle jedit -l HOL-Word

对于 AFP 会话，您需要单独告诉系统有关会话目录的信息。这可以通过isabelle jedit -d DIR1 -d DIR2 在命令行上或在您的$ISABELLE_HOME_USER/ROOTS 文件中完成（在单独的行中列出每个目录）。

纯命令行解决方案如下所示：

isabelle jedit -d isabelle_afp -l Simpl

请注意，在此示例中，isabelle_afp 是（相对或绝对）目录名称，而 Simpl 是逻辑会话名称。

【讨论】：

列出可用会话使用： isabelle build -a -n -v -d isabelle_afp

【解决方案2】：

首先，您需要为您的isabelle_afp 目录设置一个“会话”。这是通过创建一个文件 ROOT（在 isabelle_afp 内）来完成的，该文件包含以下形状的条目（另请参见 isabelle doc system 第 3 章：Isabelle 会话和构建管理）

session session_name = HOL +
  theories
    Theory1
    Theory2
    Theory3

这大致意味着堆映像session_name应该基于HOL堆映像并另外包含理论Theory1，Theory2，...

现在调用isabelle jedit -d isabelle_afp -l session_name。第一次完成时，这会构建会话session_name 的堆映像。只要isabelle_afp 中没有任何变化，任何进一步的调用都将直接在预构建的堆映像session_name 之上启动 Isabelle/jEdit。

【讨论】：