Using a heap image · Beginner Questions

I'm trying to make a "Session" so that loading up the work I've done already will be quicker.

I've read through #Beginner Questions > Issue opening with prebuilt parent session image and think I understand a bit more. I've even successfully built a heap image using the following ROOT file, because opening up Chapter1-3, which includes 1-1 and 1-2, from another file currently takes a couple of minutes, and I'd like it to be quicker.

session CS1951Y2025 = HOL +
sessions
  "HOL-Library"
  "HOL-Analysis"
theories
    "Chapter1-1"
    "Chapter1-2"
    "Chapter1-3"

  document_files
    "root.tex"

ls -l ~/.isabelle/Isabelle2025/heaps/polyml-5.9.1_arm64_32-darwin/CS1951Y2025

-rw-r--r--@ 1 jhughes  staff  97684232 Nov 15 06:49 /Users/jhughes/.isabelle/Isabelle2025/heaps/polyml-5.9.1_arm64_32-darwin/CS1951Y2025

which indicates that this heap file was created about 10 minutes before I began typing this question.

But when I start Isabelle in the usual way for me (use Spotlight-search on my Mac to find the Isabelle2025 app) and load up Chapter1-3.thy, it still takes about 2 minutes, suggesting to me that Isabelle is not using that prebuilt heap. I searched the Systems manual for the word heap, but didn't find anything about how to make sure a particular heap is loaded when I start jEdit. Looking through the Isabelle/jEdit documentation led me to try

/Applications/Isabelle2025.app/bin/isabelle jEdit -d .

from Terminal while in the directory where the ROOT file (above) is located. Still, when I opened Chapter1-3.thy, I see all the various subordinate theories slowly loading -- no speed improvement at all.:
image.png

I even discovered the dropdown at the upper right of the "Theories" panel and tried selecting CS1951Y2025:

Is there some other invocation I should have used? Did I build the session wrong?

Mathias Fleury (Nov 15 2025 at 12:38):

After selecting the base session, you need to restart Isabelle do have any effect

Mathias Fleury (Nov 15 2025 at 12:39):

/Applications/Isabelle2025.app/bin/isabelle jEdit -d . -l CS1951YS2025

John Hughes (Nov 17 2025 at 14:00):

It turns out that I'm still (slightly) stuck. The terminal variant works, but when I select CS1951Y2025 in the Theory Panel, and then quit, and then try to start Isabelle from SpotLight search (or the Applications menu), etc., I get an error. Let me repeat the steps I've taken (on a Mac M1):

% echo -n 'export PATH="/Applications/Isabelle2025.app/bin:$PATH"' >> ~/.zshrc
<open a new terminal window>
% cd /Users/jhughes/Documents/Projects/CS1951Y-2025
% ls Chapter1*.thy
Chapter1-1-9-12.thy Chapter1-1.thy      Chapter1-2.thy      Chapter1-3.thy
 % ls document
ls: document: No such file or directory
% isabelle mkroot

Initializing session "CS1951Y-2025" in "/Users/jhughes/Documents/Projects/CS1951Y-2025"
  creating "ROOT"
  creating "document/root.tex"

Now use the following command line to build the session:

  isabelle build -D .
%
<edit ROOT>
% cat ROOT
session CS1951Y2025 = HOL +
  (*options [document = root.tex, document_output = "output"]*)
sessions
  "HOL-Library"
  "HOL-Analysis"
theories
    "Chapter1-1"
    "Chapter1-2"
    "Chapter1-3"

  document_files
    "root.tex"
% isabelle build -D .
0:00:03 elapsed time

That "elapsed time" troubles me, because previously it's been a couple of minutes. Also, even though it's now 8:48 AM, I see this:

% ls -lt ~/.isabelle/Isabelle2025/heaps/polyml-5.9.1_arm64_32-darwin/

total 190864

drwxr-xr-x@ 6 jhughes  staff       192 Nov 17 08:08 log
-rw-r--r--@ 1 jhughes  staff  97718836 Nov 17 08:08 CS1951Y2025

but perhaps isabelle knows that nothing has changed and hence has figured out it doesn't need to rebuild anything.

% isabelle jEdit -d . -l CS1951Y2025

and jEdit appears, and in the Theories panel, the dropdown at the top right shows my new whatever-it's-called (a Session? A heap file?):
image.png

I can load a theory that depends on Chapter1-3.thy and it happens almost instantly. So this seems like a success so far. But if I run Isabelle in the "normal" way (using SpotLight search), CS1951Y2025 is no longer listed in the Theories panel, and loading is once again slow.

% isabelle jEdit -d . -l CS1951Y2025

and select CS1951Y2025 from the dropdown, quit, and then start Isabelle from SpotLight search, I get an error:
image.png

The "Theories" panel is no longer visible, so I can't unselect this choice, and the only way to get rid of the problem is to again run isabelle from the command line, unselect my session, and quit. After that I can run Isabelle...but with no access to my new 'session'. It seems as if a jar file should have gotten built somewhere but didn't.

I apologize for the long question, but I wanted all the details to be available.

Mathias Fleury (Nov 17 2025 at 14:29):

Mathias Fleury (Nov 17 2025 at 14:30):

exactly like when you install the AFP, you have to tell Isabelle that it has to search in the AFP directory

Mathias Fleury (Nov 17 2025 at 14:31):

This is what -d . does: it tells Isabelle to also search in the local directory.

John Hughes (Nov 17 2025 at 18:50):

When I run Isabelle from spotlight search, I don't have to tell it where to look for Main or Complex_Main, or HOL-Algebra. I was hoping that after I'd done this build-stuff, I wouldn't have to tell it where to look for my CS1951Y2025 'heap' either.

If it turns out that when I build my own heaps, I have to use the command line from now on, that's fine. Is this really what should be happening?

Mathias Fleury (Nov 17 2025 at 20:24):

Just follow the instruction for the AFP https://www.isa-afp.org/help/ replacing the path to the AFP with the path to CS1941Y2025

Stream: Beginner Questions

Topic: Using a heap image

John Hughes (Nov 15 2025 at 12:22):