[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.)
>>
> 
> 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:

https://isabelle.sketis.net/repos/afp-devel/file/98320942654a/thys/Polynomial_Factorization/ROOT

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

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?


	Makarius