[isabelle-dev] NEWS: proper session directories and faster PIDE startup

Makarius makarius at sketis.net
Thu Sep 12 15:04:23 CEST 2019

*** 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.)

*** Isabelle/jEdit Prover IDE ***

* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
the "session focus" of option "isabelle jedit -S" has become obsolete
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
sufficient and more convenient to start editing a particular session.

*** System ***

* The command-line tool "isabelle imports" has been discontinued: strict
checking of session directories enforces session-qualified theory names
in applications -- users are responsible to specify session ROOT entries

This refers to Isabelle/9cde8c4ea5a5 and AFP/98320942654a. It means that
session directories are much better defined than ever before, and the
overall session/theory management has become more robust and faster.

The scheme turned out a bit more liberal than I anticipated some years
ago: it is still possible to have multiple directories for a single
session, even though this often obscures its content.


More information about the isabelle-dev mailing list