Re: [isabelle] ERROR Duplicate session "Isac"

On 06/24/2014 09:22 AM, Andreas Lochbihler wrote:
Hi Walther,

in the second command, you add your ROOT file twice to Isabelle's session directory (once via ROOTS and once via "-d src/Tools/isac/". Isabelle does not realise that this is the same specification and thus complains. Leave out the "-d ..." and it should work.

Thanks a lot, Andreas --- deleting 3 characters is quick recovering from lengthy studies of system.pdf ;-)))



On 24/06/14 09:03, Walther Neuper wrote:
Building our session "Isac" works very conveniently:

In "~~/ROOTS" we have an entry "src/Tools/isac" and in the latter directory we have a
"ROOT" (attached) with

     session Isac in "~~/src/Tools/isac" = HOL + theories Build_Isac

and "Build_Isac.thy" (*); then in the commandline we execute "isabelle jedit -l Isac" which builds the session automatically if an imported file has been changed -- very

But generating theory browser information causes an ERROR: following system.pdf we execute
on the commandline:

     (1)$ ./bin/isabelle build -o browser_info -v -c HOL
(2)$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac

(1) works perfectly, (2) causes the error "Duplicate session "Isac"" (3) ---

--- where could we have introduced the "Duplicate session" ?


PS(3) the error message in full length:
neuper at neuper:/usr/local/isabisac$ ./bin/isabelle build -o browser_info -d
src/Tools/isac/ -v -b Isac
Started at Tue Jun 24 08:26:03 CEST 2014 (polyml-5.5.1_x86-linux on neuper)


Duplicate session "Isac" (file "src/Tools/isac/ROOT")
Finished at Tue Jun 24 08:26:07 CEST 2014
0:00:04 elapsed time, 0:00:03 cpu time

Walther Neuper                          Mailto: neuper at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home:

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