Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Importing from session 2019 vs. 2020

view this post on Zulip Email Gateway (Jul 24 2020 at 13:58):

From: Makarius <>
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
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


Last updated: Sep 25 2021 at 08:21 UTC