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

Makarius makarius at sketis.net
Thu Sep 12 16:33:02 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.)
> (at least for document preparation) 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?

You merely need to invent a dummy directory that no other session is
using. The theory imports refer to "collected" theories from other
sessions via session-qualified names, so that directory is irrelavant.

If you do have additional local theories for the "base" session, you put
them into this separate session directory.

I have already cleaned up AFP in this respect: unexpectedly it was
rather easy.

> While logically such "collecting sessions" might be irrelevant, they are
> very convenient in terms of saving build time.

Even worse, they often waste more time than they save.


More information about the isabelle-dev mailing list