[isabelle-dev] NEWS: proper session directories and faster PIDE startup

Makarius makarius at sketis.net
Thu Sep 12 20:32:58 CEST 2019

On 12/09/2019 16:04, Christian Sternagel wrote:
> On 9/12/19 3:04 PM, Makarius wrote:
>> *** General ***
>> * Session ROOT files need to specify explicit 'directories' for import
>> of theory files. Directories cannot be shared by different sessions.
>> (Recall that import of theories from other sessions works via
>> session-qualified theory names, together with suitable 'sessions'
>> declarations in the ROOT.)
> I often use a single ROOT file along
> the following lines
>   session S_base = HOL + ...
>   session S = S_base + ...
> where S_base typically collects a lot of stuff (from the AFP say) into a
> single heap image to make processing faster for my actual work that is
> done in S.
> I wonder what a suitable replacement for the above setup would be, now
> that directories cannot be shared by different sessions anymore?

Has everything become clear already?

There might be a remaining confusion about the meaning of "session
directory": it is a place where .thy files may reside in order to be
incorporated into the session-qualified theory name space. Each
directory stands for itself, without inclusion of subdirectories.

Here is also a concrete example from AFP:


It uses the subdirectory "Lib" for the auxiliary session, but that does
not contribute any theories on its own.

Whenever I pass by this JNF-AFP-Lib session, I wonder if there is any
remaining use of it. It quotes a lot of theories without a check if they
are actually needed. Loading the material takes only 30s in my 8core

For interactive development there is "isabelle jedit -R" (option "-S"
with its session focus restriction is obsolete). Is that sufficient, or
is something else required?


More information about the isabelle-dev mailing list