[isabelle] ERROR Duplicate session "Isac"



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 convenient!

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" ?

Walther


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)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86-linux"
ML_HOME="/home/neuper/.isabelle/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"

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

(*  Title:  create a heap image for isac on Isabelle2013
    Author: Walther Neuper, TU Graz, 130715
   (c) due to copyright terms

$ cd /usr/local/isabisac/
$ ./bin/isabelle build -v -b Isac

see ~~/etc/settings
  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
before out-outcommenting (*, browser_info = true*) below and ...
$ ./bin/isabelle build -o browser_info -v -c HOL
$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac     ERROR: duplicate session Isac ?!?
*)

session Isac in "~~/src/Tools/isac" = HOL +
  description {*
    Isac core, prototype of a math-engine and knowledge 
    for a TP-based educational mathematics assistant.

    The java front-end is under development at TU Graz,
    the PolyML math-engine and Isabelle knowledge at RISC Linz.
    See http://www.ist.tugraz.at/isac/.
  *}
  options [document = false (*, browser_info = true*)]
  theories Build_Isac


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