How to use persistent heap images to make loading

问题:

Let's assume I have a directory isabelle_afp where a lot of theories are stored. This directory is a library and I do not plan to change the files in it. I want to speed up the start-up time of Isabelle/jEdit (by default, all theories in isabelle_afp my current theory depends on are processed anew).

How can I skip this step? The system manual tells me to build a persistent heap image. What is the easiest way to do so?

And how can I tell Isabelle/jEdit to load this heap image?

回答1:

Isabelle/jEdit in Isabelle2013 already takes care of building your heap images, by a relatively basic mechanism that uses the isabelle build_dialog tool internally (which has a separate entry in the cited documentation).

You have two main possibilities doing it without using isabelle build_dialog or the isabelle build power-tool manually:

• The jEdit dialog "Utilities / Options / Plugin Options / Isabelle / General" provides a choice for "Logic", with a tiny tool tip saying that you have to restart the application after changing it. Doing that, the heap image will be produced on restart.

• The command line option -l, e.g. isabelle jedit -l HOL-Word

For AFP sessions you need to tell the system separately about session directories. This can be done on the command line via isabelle jedit -d DIR1 -d DIR2 or in your $ISABELLE_HOME_USER/ROOTS file (list each directory on a separate line).

A pure command-line solution would look like this:

isabelle jedit -d isabelle_afp -l Simpl

Note that in this example, isabelle_afp is a (relative or absolute) directory name, while Simpl is the logical session name.

回答2:

First, you need to set up a "session" for your isabelle_afp directory. This is done by creating a file ROOT (inside isabelle_afp) which contains an entry of the following shape (see also isabelle doc system Chapter 3: Isabelle sessions and build management)

session session_name = HOL +
  theories
    Theory1
    Theory2
    Theory3

This roughly means that the heap image session_name should be based on the HOL heap image and additionally contain the theories Theory1, Theory2, ...

Now invoke isabelle jedit -d isabelle_afp -l session_name. When done for the first time, this builds the heap image of session session_name. As long as nothing in isabelle_afp changes, any further invocations will directly start Isabelle/jEdit on top of the prebuilt heap image session_name.