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?


isabelle-dev mailing list

Reply via email to