On 9/12/19 4:33 PM, 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.
Thanks. In hindsight that was obvious and quite easy too. You made the start-up time great again. > > 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. While what you say is true and in addition such "build sessions" (we have for example "IsaFoR_1", ..., "IsaFoR_4" in the IsaFoR project) can be tedious to maintain I find them necessary from time to time. For example in IsaFoR I (depending on the machine I am working on) and some students are in a situation where thy-files that are very close to the final code generation session are really hard to work with in Isabelle/jEdit since RAM is close to or already swapping and every single edit takes quite some time before taking effect. In such situations (especially when you have to restart Isabelle/jEdit) I find it convenient to have a heap image that contains everything up to the single file I am currently working on. Maybe there is a better way to achieve the same goal without creating superfluous ad-hoc sessions? cheers chris > > > Makarius > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev