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.

Tobias


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Reply via email to