[isabelle-dev] Bad theory import "Main"

[Makarius]

On 23/04/17 18:10, Blanchette, J.C. wrote:
> 
> Yes, it does both I guess. The "half-decent error message" looks like this:
> 
> /Users/blanchette/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
> Cannot start: 
> *** No such file: "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** No such file: "/Users/blanchette/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
> *** The error(s) above occurred for theory "HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** No such file: "/Users/blanchette/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
> *** The error(s) above occurred for theory "HOL-Lib.Polynomial_Factorial" (line 29 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** The error(s) above occurred in session "HOL-Lib" (line 1 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> 
> But then I can't use Isabelle/jEdit.

The problem is in the HOL-Lib session from isafor. It is somewhere in
your ROOTS (or -d specifications).

Are you working with IsaFoR on purpose, or is this just an accident?


The transition from unqualified theories to qualified theories is not
smooth -- there can be intermediate situations, where certain sessions
cannot import certain theories anymore.

The emerging tool "isabelle imports" tools helps to sort out the
situation, but it requires some care to use it and I am still exploring
the overall situation.

In current Isabelle/6acb28e5ba41 it is also possible to use something
like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
to the requirements of MY_SESSION.


	Makarius