Re: [isabelle-dev] SQLite-related error in testboard-afp job
> As with the old log files, any error to access the persistent data is > turned into a warning, since there might be old files still around, > while the logical data format has changed. > > > I don't know anything about testboard and can't say what is really going > on here. For whatever it's worth, I cleared out all files in 'heaps', which appears to have resolved the problem. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] PLATFORMS: Mac OS X
Please regard the updated Admin/PLATFORMS file http://isabelle.in.tum.de/repos/isabelle/annotate/27c1b5e952bd/Admin/PLATFORMS This means already since 04-Mar-2017 (one month ago): * Mac OS X Mountain Lion is no longer supported and the baseline is Mavericks (on macbroy2). This is relevant when producing Isabelle components! * We have an old test machine updated for macOS Sierra in the Isabelle cronjob. * In total the last 4 Apple OS versions are supported, despite old and crumbling test hardware. (I have a new MacMini at home to compensate this a little.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Changed theory merge behaviour
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
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