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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
