[isabelle-dev] Towards the Isabelle2017 release

[Makarius]

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
official name.

 (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:

  sessions "S"
  theories "S.T"

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.


	Makarius