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