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

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

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

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

最佳答案

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

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

isabelle jedit -d isabelle_afp -l Simpl

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

关于jedit - 如何使用持久堆图像在 Isabelle/jEdit 中更快地加载理论？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/15292158/