Re: [isabelle] "Duplicate session"
On Thu, 21 Nov 2013, Walther Neuper wrote:
~$ ./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
PS(1): these are all respective sessions found in the user space:
~/.isabelle$ find -name 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
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
That tool is mostly obsolete. It does not refer to "sessions" at all,
only to heap files in certain directories.
This archive was generated by a fusion of
Pipermail (Mailman edition) and