4

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

我怎样才能跳过这一步？系统手册告诉我构建一个持久堆映像。最简单的方法是什么？

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

4

2 回答 2

3

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而是逻辑会话名称。

于 2013-03-08T11:15:18.843 回答
1

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 的堆映像session_name。只要没有任何isabelle_afp变化，任何进一步的调用都将直接在预构建的堆映像之上启动 Isabelle/jEdit session_name。

于 2013-03-09T03:35:14.147 回答