[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