[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