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