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

[Tobias Nipkow]

On 12/09/2019 16:33, 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.
> 
> 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.

For paper writing (which Christian referred to) they are indispensible. It would 
kill you if you had to load all the theories once more when you modify the paper 
based on them.

Tobias

> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190912/c1a0c407/attachment-0001.bin>