[isabelle-dev] Towards the Isabelle2017 release
makarius at sketis.net
Wed Aug 30 23:22:36 CEST 2017
On 24/08/17 09:38, Thiemann, Rene wrote:
> - Most changes have been caused by integrating session-qualified theory imports.
> This will also require a reform of the splitting of sessions, which previously
> was structured towards a fast build-process, but now should be structured more
> towards logical structure (which is currently reflected in the directory-structure).
Some notes on this.
(1) Isabelle2017-RC0 does not yet have full qualification of all
library theories etc. but I have changed that shortly afterwards, so it
is already in newer snapshots from
http://isabelle.in.tum.de/devel/release_snapshot -- or you just wait a
few days for Isabelle2017-RC1.
(2) Logical structure is indeed defined primarily by the overall
session layout, i.e. a theory T loaded into session S will get a name
S.T that remains valid once and for all. The theory file may reside in a
subdirectory of the session itself, but that does not contribute to its
(3) It possible to refer to theories from other sessions without
creating a new name (actually the prefereed way), using a ROOT
specification like this:
As a corollary it should be quite easy to assemble auxiliary session
images from already existing sessions (without using parent images).
(4) Despite the important reform of session-qualified imports now, it
is still possible to use unqualified imports from parent images. That is
a concession to easy upgrades of existing project sources, although it
is up to the old name confusions. The "isabelle imports -U" tool
eliminates such unqualified imports already, and right after the
Isabelle2017 release the unqualified option will just disappear:
everything *must* be imported as qualified afterwards.
More information about the isabelle-dev