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
