loading a precompiled heap image in Isabelle

Question

Following how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle and another advice I created an image for Nominal Isabelle:

isabelle build -v -b -d . Nominal2

The heap image was created under ~/.isabelle:

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

Then I started

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

I expected the system to quickly load a theory that imports a part of Nominal but it took almost a minute. Is that usual?

Answer 1

Your process of building a heap image looks correct. In fact, you don't actually need to the isabelle build step, because isabelle jedit will automatically trigger a build if the heap doesn't exist or isn't up to date.

You can determine if isabelle jedit is using the heap based on two facts:

• If it needs to build a heap, you will see a dialog box pop up showing the build progress when you first start jEdit. This will typically take 10 seconds to several hours, depending on the size of the heap that needs to be built. The screenshot below shows an example of the build dialog; in this case, I am building the Main heap:

  

• If it isn't using the heap at all (for instance, if you forgot to specify -l Nominal2), all the theories that Nominal2 includes will need to be opened up in jEdit, and you will see them in the jEdit "Theories" panel.

  In the image below, for example, Scratch imports a file AutoCorres, which in turn imports MapExtra, Padding, BitOperations, and so on. If I was using the correct AutoCorres heap, none of these files would need to be loaded, because they would already be pre-compiled into the heap:

  

Even if Isabelle is using a heap, it still has to load it into memory when it starts up. This usually takes a few seconds, which, when compounded by the not-particularly-amazing startup times of jEdit itself, might be what you are experiencing.