Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] update Isabelle2019->20, session


view this post on Zulip 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

view this post on Zulip 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: Sep 28 2021 at 19:14 UTC