Dear Makarius, 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? While logically such "collecting sessions" might be irrelevant, they are very convenient in terms of saving build time. But maybe there is a better way to achieve the same goal? cheers chris _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
