Email Gateway (Jul 24 2020 at 13:58): Email Gateway (Jul 24 2020 at 13:58):From: Makarius <makarius@sketis.net>
Looking at this again, I found that your example was actually wrong, but the
error message too indirect to see it on the spot: a proper specification
"directories X" was missing in ROOT.
The change
https://isabelle-dev.sketis.net/rISABELLE4768b1facec2367417ff61d26011f37979b67505
in ongoing Isabelle development improves on that, although it is still unclear
how the situation in the next release will be in several months.
You can also see the error in Isabelle2020, if you restrict the selection to
session A of the example:
$ isabelle2020 build -d mwe_2020 A
*** Implicit use of directory "X" for theory "A.TheoryA"
*** Implicit use of session directories: "X"
*** The error(s) above occurred in session "A" (line 1 of
"/home/makarius/tmp/mwe_2020/ROOT")
Makarius
Last updated: Jan 04 2025 at 20:18 UTC