如何使用持久堆圖像在Isabelle/jEdit中更快加載理論？

我們假設我有一個目錄isabelle_afp，其中存儲了很多理論。這個目錄是一個庫，我不打算改變其中的文件。我想加快Isabelle/jEdit的啓動時間（默認情況下，我現在的理論依賴的所有理論都會重新處理）。如何使用持久堆圖像在Isabelle/jEdit中更快加載理論？

如何跳過這一步？ system manual告訴我要構建一個持久堆映像。最簡單的方法是什麼？

我該如何告訴Isabelle/jEdit加載這個堆映像？

來源

2013-03-08 corny

Isabelle/jEdit在Isabelle2013中已經採用內部使用isabelle build_dialog工具（在引用的文檔中有單獨條目）的相對基本的機制來建立堆圖像。

你必須這樣做，而不使用isabelle build_dialog或手動isabelle build動力工具的兩個主要的可能性：

的jEdit的對話「工具/選項/插件選項/伊莎貝爾/常規」提供了一個選擇。「邏輯「，用一個小小的工具提示說，你必須在改變它之後重新啓動應用程序。這樣做，堆圖像將在重新啓動時生成。
命令行選項-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-08 11:15:18 Makarius

要列出可用會話，請使用：isabelle build -a -n -v -d isabelle_afp – corny 2013-03-09 13:08:07

首先，您需要爲您的isabelle_afp目錄設置一個「會話」。這是通過創建一個文件ROOT（內isabelle_afp），它包含以下形狀的條目來完成（見isabelle doc system第3章：伊莎貝爾會議和構建管理）

session session_name = HOL + 
    theories 
    Theory1 
    Theory2 
    Theory3

這大概意味着，堆圖像session_name應基於HOL堆圖像並且還包含理論Theory1，Theory2，...

現在調用isabelle jedit -d isabelle_afp -l session_name。第一次完成時，這會建立會話session_name的堆映像。只要isabelle_afp中沒有任何更改，任何進一步的調用將直接啓動Isabelle/jEdit在預先構建的堆映像session_name之上。

來源

2013-03-09 03:35:14 chris

如何使用持久堆圖像在Isabelle/jEdit中更快加載理論？

回答

相關問題