[isabelle-dev] Changed theory merge behaviour

[Makarius]

On 04/04/17 11:06, Manuel Eberl wrote:
> During a minor overhaul of some theories in the distribution, I
> discovered some problems with theory imports.
> 
> In short: apparently, importing a theory (e.g. Library/Multiset) twice
> in two theories A and B can be problematic when the theory import is
> done in different ways (e.g. once as "~~/src/HOL/Library/Multiset" and
> once as "Multiset" by another theory in Library).

Thanks for keeping an eye on ongoing Isabelle development, by following
the repository and isabelle-dev mailing list.


I am presently in the process to simplify and unify theory imports in
isabelle build and PIDE interaction, in continuation of older attempts
from 3 years ago. In the end, there should be session-qualified theory
names and imports without these slightly odd file-system path fragments.

Intermediate situations are expected to lead to spurious problems,
according to the normal isabelle-dev process. Yesterday (908a27a4b9c9) I
actually tested for situations that you described above, but did not
find any problems just by accident. Now I know that HOL-Library +
HOL-Number_Theory are a good testbed for entangled theory and session
dependencies that are going back and forth several times, also with
non-standard imports from main HOL.

In 7fb5aad28f38, part of the old behaviour is restored, so that
isabelle-dev work can continue. Getting import name resolution really
right will require more iterations. At some point there should be also
some tool "isabelle update_imports" to sanitize theory imports in
Isabelle + AFP, maybe it should also check for cycles in cross-session
imports to help cleaning up entangled. sessions as above.


> There was no NEWS entry for this changed behaviour and I am a bit
> confused about how to proceed now.

The NEWS file documents "user-relevant changes", i.e. it is strictly
speaking not relevant for isabelle-dev repository snapshots -- here the
Mercurial history is the main source for information.

In theory, the latest point to write NEWS entries is during the final
stage of the release process. Nonetheless, I usually write NEWS a few
days or weeks after a new stepping stone of new functionality is
consolidated, when it has become clear where we are and where we can go
at the moment.

I guess that the idea of "continuous releases" somehow came up with the
Jenkins experiments from last year. But that unrealistic model belongs
to Jenkins, and not to Isabelle development.


	Makarius