[isabelle-dev] NEWS: proper session directories and faster PIDE startup
Makarius
makarius at sketis.net
Thu Sep 12 17:36:57 CEST 2019
On 12/09/2019 15:04, 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.)
An important consequence is that a theory file gets a unique
session-qualified name, without accidental multiplication of theories
that is occasionally seen in applications.
Thus by forcing users to clean up their session/theory arrangement, some
applications might become faster without further ado. (In the past 2
years, I've cleaned up such situations several times in AFP, and it is
all fine in AFP/98320942654a).
Makarius
More information about the isabelle-dev
mailing list