[isabelle-dev] Bad theory import "Main"

Blanchette, J.C. j.c.blanchette at vu.nl
Sun Apr 23 18:10:54 CEST 2017


> This means you should see some "Java vomit" on the terminal at startup
> of Isabelle/jEdit, as well as some text popup with a half-decent error
> message. Plugin startup is always a bit fragile.

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. I was better off 2 days ago. Back then, things worked.

Jasmin




More information about the isabelle-dev mailing list