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

[Makarius]

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.


	Makarius