[isabelle-dev] Changed theory merge behaviour

Makarius makarius at sketis.net
Tue Apr 4 16:43:00 CEST 2017

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.


More information about the isabelle-dev mailing list