Re: [isabelle] building session confuses paths to theories
On Tue, 12 Jan 2016, 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 , 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
PS: The list of errors in full length is
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/Complex_Main.thy" (line 6 of
"/usr/local/isabisac/src/HOL/Mutabelle/Complex_Main.thy" (line 2 of
The error(s) above occurred in session "Protocol2015" (line 1 of
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and