Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] DONE *** Duplicate session "RAW"

Email Gateway (Aug 22 2022 at 10:19):

From: Walther Neuper <wneuper@ist.tugraz.at>
the error message

*** Duplicate session "xxx"

correctly indicates, that
(1) one ROOTS contains duplicate entries "xxx", and/or
(2) duplicate ROOTS contain the entry "xxx".

The latter might occur in cases, where several Isabelle code collections
contain their own ROOTS: Isabelle session management checks all ROOTS
found by

yyy$ ./bin/isabelle build -D .

in the directory "yyy" and also in "~~/".

Hope this helps

On 2015-06-18 15:08, Walther Neuper wrote:

annoyed by the above error message in another context I found, that

isabisac$ .bin/isabelle jedit -l Isac

has appeased me with working nicely in faulty settings for a long time.
The faulty settings became apparent with

isabisac$ ./bin/isabelle build -D . -d src/Tools/isac/ -b
*** Duplicate session "Isac" (line 15 of "src/Tools/isac/ROOT")
(line 15 of "/usr/local/isabisac/src/Tools/isac/ROOT")

where line 15 of "src/Tools/isac/ROOT" refers to [1] and the faulty
settings seem to be:

isabisac$ ./bin/isabelle getenv ISABELLE_HOME
ISABELLE_HOME=/usr/local/isabisac #(1) ok

isabisac$ ./bin/isabelle getenv ISABELLE_HOME_USER
ISABELLE_HOME_USER=/home/wneuper/.isabelle/Isabelle2014 #(2) NOT ok

system.pdf says that these variables are "determined automatically from
the location of the binary that has been run". Reading section 1.1.1,
however, I cannot figure out, how to change (2) to

ISABELLE_HOME_USER=/home/wneuper/.isabelle/isabisac

Help is very much appreciated!

Walther

[1]
https://intra.ist.tugraz.at/hg/isa/file/43c1e5222f0e/src/Tools/isac/ROOT#l15

Last updated: Nov 21 2024 at 12:39 UTC