AFP Dijkstra的最短路徑算法

對於AFP條目Dijkstra's Shortest Path Algorithm，證明大綱和證明文檔都不存在*。不幸的是，我沒有找到IsaMakefile來在本地構建這些文檔。什麼是獲得這些文件的最佳方式？AFP Dijkstra的最短路徑算法

另一個問題，因爲Dijkstra.thy取決於很多其他理論，有沒有辦法更快加載一切？

*）現在是固定的。

來源

2013-03-07 corny

（好像有東西，現在在AFP壞了，請告訴編輯它。）

在一般情況下，你可以下載AFP項目的來源和自己產生的文件是這樣的：

獲取並解壓縮all AFP sources - 提供下載單獨的條目，但是您必須手動分解依賴關係。
調用isabelle build這樣的：
```
isabelle build -d afp-2013-03-02 -o document=pdf -v Dijkstra_Shortest_Path 
```
這裏afp-2013-03-02是一個由拆包當前AFP來源獲得的目錄。

又見Isabelle System manual有關「伊莎貝爾會議和構建管理」，這是所有新的Isabelle2013。

請參閱isabelle build -b通過從會話中生成持久堆映像來加快加載速度。

來源

2013-03-07 11:28:43 Makarius

該命令失敗：[鏈接]（http://pastebin.com/RmN6Vr8x） – corny 2013-03-07 16:15:13

奇怪的是，我只是再次嘗試，看看它真的有效。關於'壞會話根目錄：「afp-2013-03-02」'的錯誤意味着Isabelle build沒有找到'afp-2013-03-02/ROOTS'文件，所以它不存在，不可讀，不管。 '-d'選項指定一個相對於當前目錄的目錄，但你已經知道了。 – Makarius 2013-03-07 17:31:57

似乎有根源：[鏈接]（http://pastebin.com/h5tAgfnB） – corny 2013-03-07 17:43:41

法新社條目中的鏈接確實被破壞，現在應該再次修復，對此感到遺憾。

正如Makarius寫道，法新社新版採用了伊莎貝爾的新版本系統，即每個條目都有一個ROOT文件，可用於檢查相關理論和構建文件。

Makarius的答案几乎是正式的做法，但我還建議將AFP設置爲組件。這給你以下步驟：

Download the AFP到例如~/afp
將其設置爲例如組件加入~/afp到~/.isabelle/Isabelle2013/components（也AFP as a component見）
建立條目以

isabelle afp_build Dijkstra_Shortest_Path

來源

2013-03-08 10:59:23 lsf37

您還可以使jEdit的建堆像你。如果AFP是設置作爲成分（看看它的其他答案），剛開始的jEdit與

isabelle jedit -d '$AFP' -l Dijkstra_Shortest_Path

和使用jEdit將選擇Dijkstra_Shortest_Path作爲基本邏輯和（重新）如果有必要建立它。

如果您經常使用AFP，默認情況下添加AFP路徑可能會很有用。爲此，請在$ISABELLE_HOME_USER中創建一個文件ROOTS，其中包含行$AFP（或者添加此行，如果文件已存在）。

來源

2013-06-03 21:26:45

AFP Dijkstra的最短路徑算法

回答

相關問題