[isabelle] building session confuses paths to theories



in all the years with Isabelle I never saw something like that and now I have not even an idea how to cut down the problem. The problem "confused paths" happens when creating a session of libisabelle [1], but it seems independent from that component.

The problem occurs when creating the session by

   isabisac$ ./bin/isabelle jedit -l Protocol2015 &

which shows a list of errors in Isabelle's bootstrap window beginning with

   No such file: "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy"
   The error(s) above occurred for theory "Complex_Main"
   (required by "Protocol" via "Build_Thydata" via "Isac" via "Frontend" via "xmlsrc" via "MutabelleExtra") (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
   :

while we have

   isabisac$ find -name Complex_Main.thy
   ./src/HOL/Complex_Main.thy


Is there somebody who has a quick idea, what is going on here, or who could give a direction of how to search for the reason of these errors ?

Any help would be highly appreciated!!!
Walther


[1] https://github.com/larsrh/libisabelle
     https://github.com/larsrh/libisabelle-protocol

______________________________
PS: The list of errors in full length is

No such file: "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy"
The error(s) above occurred for theory "Complex_Main"
(required by "Protocol" via "Build_Thydata" via "Isac" via "Frontend" via "xmlsrc" via "MutabelleExtra") (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
No such file: "/usr/local/isabisac/src/HOL/Library/Main.thy"
The error(s) above occurred for theory "Main"
(required by "Protocol" via "Build_Thydata" via "Isac" via "Frontend" via "xmlsrc" via "MutabelleExtra" via "Refute") (line 11 of "/usr/local/isabisac/src/HOL/Library/Refute.thy")
No such file: "/usr/local/isabisac/src/Tools/isac/Knowledge/Real.thy"
The error(s) above occurred for theory "Real"
(required by "Protocol" via "Build_Thydata" via "Isac" via "Vect") (line 1 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Vect.thy")
Incoherent imports for theory "Complex_Main":
  "/usr/local/isabisac/src/Tools/isac/Knowledge/Complex_Main.thy" (line 9 of "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_ML.thy")
  "/usr/local/isabisac/src/Tools/isac/Knowledge/Complex_Main.thy" (line 6 of "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
  "/usr/local/isabisac/src/Tools/isac/Knowledge/Complex_Main.thy" (line 7 of "/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
  "/usr/local/isabisac/src/Tools/isac/Knowledge/Complex_Main.thy" (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
  "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (line 9 of "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_ML.thy")
  "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (line 6 of "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
  "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (line 7 of "/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
  "/usr/local/isabisac/src/Tools/isac/Complex_Main.thy" (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
  "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy" (line 9 of "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_ML.thy")
  "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy" (line 6 of "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
  "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy" (line 7 of "/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
  "/usr/local/isabisac/src/Tools/isac/ProgLang/Complex_Main.thy" (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
  "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (line 9 of "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_ML.thy")
  "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (line 6 of "/usr/local/isabisac/src/Tools/isac/KEStore.thy")
  "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (line 7 of "/usr/local/isabisac/src/Tools/isac/ProgLang/ListC.thy")
  "/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (line 2 of "/usr/local/isabisac/src/HOL/Mutabelle/MutabelleExtra.thy")
The error(s) above occurred in session "Protocol2015" (line 1 of "/usr/local/isabisac/libisabelle-protocol/isabelle-2015/ROOT")


The definition of "Protocol2015" is at

   https://intra.ist.tugraz.at/hg/isa/file/f9daba301a41/libisabelle-protocol/isabelle-2015/ROOT#L1

and within the same ROOT the other session "HOL-Protocol2015"

   session Protocol2015 = Codec +
     theories
       Protocol

   session "HOL-Protocol2015" = "HOL-Codec" +
     theories
       Protocol

builds without errors, and so do all the other sessions in the repository.

There is only one ROOTS in the code

   isabisac$ find -name ROOTS
   ./ROOTS

etc ???




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