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

[Christian Sternagel]

On 9/12/19 4:33 PM, Makarius wrote:
> 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.

Thanks. In hindsight that was obvious and quite easy too.

You made the start-up time great again.

> 
> 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.

While what you say is true and in addition such "build sessions" (we
have for example "IsaFoR_1", ..., "IsaFoR_4" in the IsaFoR project) can
be tedious to maintain I find them necessary from time to time.

For example in IsaFoR I (depending on the machine I am working on) and
some students are in a situation where thy-files that are very close to
the final code generation session are really hard to work with in
Isabelle/jEdit since RAM is close to or already swapping and every
single edit takes quite some time before taking effect. In such
situations (especially when you have to restart Isabelle/jEdit) I find
it convenient to have a heap image that contains everything up to the
single file I am currently working on.

Maybe there is a better way to achieve the same goal without creating
superfluous ad-hoc sessions?

cheers

chris
> 
> 
> 	Makarius
>