[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