Email Gateway (Aug 22 2022 at 12:31): Email Gateway (Aug 22 2022 at 12:31):From: Walther Neuper <wneuper@ist.tugraz.at>
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 ???
Email Gateway (Aug 22 2022 at 12:31):From: Peter Lammich <lammich@in.tum.de>
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?
Email Gateway (Aug 22 2022 at 12:31):From: Walther Neuper <wneuper@ist.tugraz.at>
Thank you, Peter, for the helpful explanation.
It is hard here to find out, what is really going on, by we have already
partial success:
https://intra.ist.tugraz.at/hg/isa/rev/ebf4a8a63371
Walther
Email Gateway (Aug 22 2022 at 12:32):From: Makarius <makarius@sketis.net>
These tons of errors prove that there is an attempt to refer to standard
Main or Complex_Main stuff from an image that does not contain these
theories.
Theory imports are resolved relatively to the "master directory" of the
current .thy file, or taken from a pre-built image. The latter case
ignores path information. This usually happens for Main and Complex_Main
in other libraries.
An example for that is src/HOL/Mutabelle/MutabelleExtra.thy. You appear
to import that without a proper HOL image.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC