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

[isabelle-dev] Changed theory merge behaviour

[Manuel Eberl]

During a minor overhaul of some theories in the distribution, I
discovered some problems with theory imports.

Apparently, the theory merge behaviour changed in one of the most recent
commits. I haven't been able to pin down which one it is exactly; I
might do a bisection later if needed.

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).

This can cause the theory merge to fail when importing both theories A
and B in a third theory C, but I was unable to extract a minimal example
– apparently, it doesn't /always/ happen.

One example of this behaviour in the wild is
Library/Formal_Power_Series, where I think the clash is caused by the
GCD theory. Another is Euler_MacLaurin in the AFP, where the clas is
caused by Multiset.

Strangely enough, this does /not/ happen when using "isabelle build"; it
only happens in Isabelle/jEdit, which is why the CI tests did not catch it.

There was no NEWS entry for this changed behaviour and I am a bit
confused about how to proceed now. Is this discrepancy between build and
IDE intended? Is there some canonical way to write import paths and the
affected theories violate it somehow?

Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev