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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev