Email Gateway (Sep 24 2020 at 13:29): Email Gateway (Sep 24 2020 at 13:29):From: Walther Neuper <walther.neuper@jku.at>
updating our project from Isabelle2019 to Isabelle2020 we cannot find
out how to adapt to the new session management:
Both command lines
/usr/local/isabisac$ ./bin/isabelle build -v -b Interpret
/usr/local/isabisac$ ./bin/isabelle build -v -b Isac
as well as Isabelle/jEdit raise the same (very consistent, thanks!) error
*** Duplicate use of directory "/usr/local/isabisac/src/Tools/isac"
*** for session "Interpret" (line 15 of
"/usr/local/isabisac/src/Tools/isac/ROOT")
*** vs. session "Isac" (line 26 of
"/usr/local/isabisac/src/Tools/isac/ROOT")
The respective ROOT is shown in the attachment.
Thank you in advance for help!
Walther
PS: system.pdf presents great new features, but extends the search-space
in the rail-diagram and for trials (a weak excuse ;-)
PPS: Build_Isac.thy imports Interpret.thy ...?... the old version had
"session Isac = HOL +", which caused the same error.
Screenshot-build-Isac.png
Email Gateway (Sep 25 2020 at 08:44):From: Walther Neuper <walther.neuper@jku.at>
sorry for the noise:
simplifying the ROOT led to useful error messages.
thank you for patience,
Walther
Last updated: Jul 15 2022 at 23:21 UTC