Re: [isabelle] "Duplicate session"



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.