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

Question

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

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

我如何告诉 Isabelle/jEdit 加载这个堆图像？

Answer 1

Isabelle2013 中的 Isabelle/jEdit 已经通过使用 isabelle build_dialog 的相对基 native 制负责构建堆图像。内部工具(在引用的文档中有单独的条目)。

如果不使用 isabelle build_dialog，您有两种主要的可能性。或 isabelle build手动电动工具:

jEdit 对话框“Utilities/Options/Plugin Options/Isabelle/General”提供了“Logic”的选择，带有一个小工具提示，提示您必须在更改后重新启动应用程序。这样做，将在重新启动时生成堆镜像。

命令行选项 -l ，例如isabelle jedit -l HOL-Word

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

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

isabelle jedit -d isabelle_afp -l Simpl

请注意，在此示例中， isabelle_afp是(相对或绝对)目录名，而 Simpl是逻辑 session 名称。