isabelle - AFP Dijkstra 的最短路径算法

Question

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

另一个问题，由于 Dijkstra.thy 依赖于许多其他理论，是否有一种方法可以更快地加载所有内容？

*) 现在已修复。

Answer 1

(法新社现在好像出了什么问题，请告诉编辑。)

一般情况下，您可以下载法新社词条的源码，自己制作文档，如下所示:

• 获取并解压all AFP sources -- 也提供下载单独的条目，但您必须手动解开依赖项。

• 像这样调用 isabelle build:

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

  这里的afp-2013-03-02是当前法新社源码解包得到的目录。

另见 Isabelle System manual关于“Isabelle session 和构建管理”，这是 Isabelle2013 中的全新内容。

请参阅那里的 isabelle build -b，通过从 session 中生成持久堆镜像来加快加载速度。