Re: [isabelle] building session confuses paths to theories



This error often happens if you re-arrange theories in the build.

Isabelle only seems to check the theory path the first time it sees the
import, any further imports of the same theory seem to be somewhat path
insensitive ... so wrong import paths may slip through, and only
manifest them later.

Are you sure that the image that you are building with actually contains
Complex_Main?

--
  Peter


On Di, 2016-01-12 at 12:35 +0100, Walther Neuper wrote:
> 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.