Email Gateway (Aug 19 2022 at 12:36): Email Gateway (Aug 19 2022 at 12:36):From: Walther Neuper <wneuper@ist.tugraz.at>
The command
~$ ./bin/isabelle build -d src/Tools/isac/ -v -b Isac
creates the message
Duplicate session "Isac" (file "src/Tools/isac/ROOT")
but no session.
How can the session be created ?
Walther
PS(1): these are all respective sessions found in the user space:
~/.isabelle$ find -name Isac
gives
./Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac
./heaps/polyml-5.5.0_x86-linux/Isac
./Isabelle2011/heaps/polyml-5.4.0_x86-linux/log/Isac
./Isabelle2011/heaps/polyml-5.4.0_x86-linux/Isac
PS(2): the session should be created from an "unauthorized Isabelle
version" derived from Isabelle2013-1; the previous session created from
Isabelle2013 is in "./heaps/polyml-5.5.0_x86-linux/"
PS(3): shouldn't the new session be built into
"./heaps/polyml-5.5.1_x86-linux/" ?
PS(4): deleting "./heaps/polyml-5.5.0_x86-linux/Isac" doesn't help (as
expected from (3))
PS (5): Isabelle2013-1 finds these logics:
~~$ ./bin/isabelle findlogics
HOL Pure
Email Gateway (Aug 19 2022 at 12:36):From: Makarius <makarius@sketis.net>
On Thu, 21 Nov 2013, Walther Neuper wrote:
The command
~$ ./bin/isabelle build -d src/Tools/isac/ -v -b Isac
creates the message
Duplicate session "Isac" (file "src/Tools/isac/ROOT")
but no session.
How can the session be created ?
This merely means that in your hierarchy of ROOTS and ROOT files you have
duplicate "Isac" entries. You should probably omit the build -d option
above.
PS(1): these are all respective sessions found in the user space:
~/.isabelle$ find -name Isac
gives
./Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac
./heaps/polyml-5.5.0_x86-linux/Isac
./Isabelle2011/heaps/polyml-5.4.0_x86-linux/log/Isac
./Isabelle2011/heaps/polyml-5.4.0_x86-linux/Isac
These are directories for heap images, not sessions. Only the static ROOT
entries count for the session name space.
PS(2): the session should be created from an "unauthorized Isabelle version"
derived from Isabelle2013-1; the previous session created from Isabelle2013
is in "./heaps/polyml-5.5.0_x86-linux/"PS(3): shouldn't the new session be built into
"./heaps/polyml-5.5.1_x86-linux/" ?PS(4): deleting "./heaps/polyml-5.5.0_x86-linux/Isac" doesn't help (as
expected from (3))
You should study Isabelle/etc/settings and the "system" manual how this
works. You probably can use ISABELLE_IDENTIFIER to distinguish different
versions. It might be actually easier to work from a repository clone of
Isabelle2013-1, which is identified differently.
In any case, manual tinkering with Isabelle versions is very difficult
these days, since the system is a bit more complex than in the 1990-ies.
PS (5): Isabelle2013-1 finds these logics:
~~$ ./bin/isabelle findlogics
HOL Pure
That tool is mostly obsolete. It does not refer to "sessions" at all,
only to heap files in certain directories.
Makarius
Last updated: Apr 18 2024 at 01:05 UTC