On 23/04/17 13:43, Blanchette, J.C. wrote:
>>> 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")
That is unrelated. I merely made the most basic mistake in Mercurial
usage, see now:
changeset: 65553:006a274cdbc2
user: wenzelm
date: Sun Apr 23 14:15:09 2017 +0200
files: src/HOL/Main.thy
description:
added missing file (amending f533820e7248);
Concerning the actual problem, I have now made the session_base error
strict (again):
changeset: 65554:a04afc400156
tag: tip
user: wenzelm
date: Sun Apr 23 14:27:22 2017 +0200
files: src/Tools/jEdit/src/plugin.scala
description:
prefer strict operation (despite 8edca3465758): there might be errors
from all_known = true (ae09b9f5980b);
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
