在伊莎貝爾

Question

加載預編譯堆圖像繼how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle和另一個建議，我創建了標稱伊莎貝爾的圖像：

isabelle build -v -b -d . Nominal2 

堆圖像在〜/ .isabelle創建：

.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-linux/Nominal2 

然後我開始

isabelle jedit -d /path/to/Nominal-distribution -l Nominal2 

我期望系統快速加載理論，導入的一部分名義上，但花了差不多一分鐘。那是平常的嗎？

Answer 1

你建立一個堆圖像的過程看起來是正確的。事實上，你實際上並不需要的isabelle build一步，因爲isabelle jedit如果堆不存在或不是最新的，系統會自動構建。

您可以確定是否isabelle jedit是使用基於兩個事實堆：

• 如果需要建立一個堆，你會看到一個對話框彈出顯示當您第一次啓動jEdit的構建過程。這通常需要10秒到幾個小時，具體取決於需要構建的堆的大小。以下屏幕截圖顯示了構建對話框的示例;在這種情況下，我建立Main堆：

  

• 如果不使用堆在所有（舉例來說，如果你忘了指定-l Nominal2），所有的理論是Nominal2包括意志需要在jEdit中打開，你會在jEdit「Theories」面板中看到它們。

  在圖像的下方，例如，Scratch導入文件AutoCorres，這反過來進口MapExtra，Padding，BitOperations，等等。如果我使用的是正確AutoCorres堆，這些檔案都將需要加載，因爲他們已經被預編譯成堆：用

  

即使伊莎貝爾是一個堆，它啓動時仍然需要將它加載到內存中。這通常需要幾秒鐘，當jEdit本身的啓動時間並不是特別驚人的時候，這可能就是您正在經歷的。