isabelle - AFP Dijkstra 的最短路径算法

Question

对于AFP条目Dijkstra's Shortest Path Algorithm，证明大纲和证明文件都不存在 *。不幸的是，我没有找到在IsaMakefile本地构建这些文档的方法。获取这些文件的最佳方式是什么？

另一个问题，由于Dijkstra.thy依赖于许多其他理论，有没有办法更快地加载所有内容？

*)现在已修复。

Answer 1

（法新社现在似乎有什么问题，请告诉编辑。）

通常，您可以下载 AFP 条目的来源并自己生成文档，如下所示：

• 获取并解压所有 AFP 源- 也提供下载单独的条目，但是您必须手动解开依赖关系。

• 像这样调用isabelle build：

  isabelle build -d afp-2013-03-02 -o document=pdf -v Dijkstra_Shortest_Path
  

  这afp-2013-03-02是通过解压当前 AFP 源获得的目录。

另请参阅有关“Isabelle 会话和构建管理”的Isabelle 系统手册，这是 Isabelle2013 中的全新内容。

看到isabelle build -b那里通过从会话中生成持久堆图像来加快加载速度。

Answer 2

法新社条目中的链接确实被破坏了，现在应该再次修复，对此感到抱歉。

正如 Makarius 所写，AFP new 使用 Isabelle 的新构建系统，即ROOT每个条目都有一个文件，可用于检查相关理论并构建文档。

Makarius 的回答几乎是官方的做法，尽管我另外建议将 AFP 设置为组件。这为您提供了以下步骤：

• 将 AFP 下载到例如~/afp
• 将其设置为组件，例如通过添加~/afp到~/.isabelle/Isabelle2013/components（另见AFP as a component）

• 建立条目

  isabelle afp_build Dijkstra_Shortest_Path

Answer 3

您还可以让 jEdit 为您构建堆映像。如果 AFP 设置为组件（请参阅其他答案），只需启动 jEdit

isabelle jedit -d '$AFP' -l Dijkstra_Shortest_Path

jEdit 将选择 Dijkstra_Shortest_Path 作为基本逻辑并在必要时（重新）构建它。

如果您经常使用 AFP，则默认添加 AFP 路径可能会很有用。为此，请在$ISABELLE_HOME_USER其中创建一个文件 ROOTS $AFP（或添加此行，如果该文件已存在）。