[isabelle-dev] Bad theory import "Main"

Blanchette, J.C. j.c.blanchette at vu.nl
Sun Apr 23 13:43:19 CEST 2017


>> I see. It prints
>> 
>> 	res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None
> 
> There is probably something wrong with the general session layout.  The
> critical changeset shows an old fallback to Pure:
> http://isabelle.in.tum.de/repos/isabelle/rev/ae09b9f5980b#l4.10

I just pulled and updated (f533820e7248) before carrying out any further tests. Now I get the same error as Jenkins:

$ isabelle build -b HOL
*** No such file: "/Users/blanchette/isabelle/src/HOL/Main.thy"
*** The error(s) above occurred for theory "Main" (line 8 of "/Users/blanchette/isabelle/src/HOL/ROOT")
*** The error(s) above occurred in session "HOL" (line 3 of "/Users/blanchette/isabelle/src/HOL/ROOT")

Jasmin




More information about the isabelle-dev mailing list