Caching theorems · Beginner Questions

Every time I want to update a comment, Isabelle/jEdit seems to check the whole proof script. Similarly, when I reopen a session, it checks every file, even though nothing has changed since a previous session. Is there a way to get isabelle to cache theorems in case (2), if not case (1)?

Mathias Fleury (Mar 20 2026 at 18:51):

The normal way is to have sessions for the parts you do not touch anymore (like HOL): the state is dumped and reloaded instead of rerunning everything. But when it is dumped, you cannot change the state anymore.

Maximilian Schäffeler (Mar 20 2026 at 18:54):

Some hints:
Regarding 1), a partial solution on older hardware might be to disable continuous checking whilst editing documentation. I don't think you can do much better as it is difficult to decide whether your edits further up invalidate subsequent proofs. Splitting your development into smaller files might also help in certain situations.
Regarding 2), initiate an isabelle project using mkroot, specify the dependencies in the ROOT file, then build its dependencies only once, e.g. invoke isabelle jedit -R <your_session_name>. Check the Isabelle system manual or ROOT files in the AFP/Isabelle distribution for examples.

Ant S. (Mar 20 2026 at 18:55):

Mathias Fleury said:

have sessions

could you elaborate on what it means to "have a session for the parts you don't touch?". If this is in the manual, where should I be looking?

Mathias Fleury (Mar 20 2026 at 18:58):

https://isabelle.in.tum.de/dist/Isabelle2025-2/doc/system.pdf, chapter 2

Ant S. (Mar 20 2026 at 18:59):

thanks! I'll take a look. (I'll try to dig through the manual before asking a question like this, sorry about that)

Mathias Fleury (Mar 20 2026 at 19:00):

But the manual is not that useful for the big picture

Ant S. (Mar 20 2026 at 19:00):

In any case, so I can be more precise when I ask something

Mathias Fleury (Mar 20 2026 at 19:03):

The idea is:

1. split your theories in groups. Let's call them A, B, C (this can change) over time
2. create your sessions (see the manual for the details), but you basically say for all your theories if they belong to A, B, or C
3. Now (before you start Isabelle!), you decide on what you are going to work (usually the latest, C). So you start Isabelle with -R C as @Maximilian Schäffeler suggested. You can also set the base session in some jEdit panel. But: you cannot touch A and B.
4. Sometimes you will want to work on everything, then you to -R A and work on everything (useful for refactoring / moving theorems).