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 [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

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 "/usr/local/isabisac/libisabelle-protocol/isabelle-2015/ROOT")

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.


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