On 23/04/17 08:39, Tobias Nipkow wrote:
> The Isabelle regression test system shows similar behaviour:
>
> 23:23:27 *** No such file:
> "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/Main.thy"
> 23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of
>
The Isabelle regression test system shows up a mistake in a commit of yours and
you ask what its purpose is? And tell us your rarely look there?
LOL
Tobias
On 23/04/2017 14:52, Makarius wrote:
On 23/04/17 08:39, Tobias Nipkow wrote:
The Isabelle regression test system shows similar
>> 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
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:
>>
> 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:
The Isabelle regression test system shows similar behaviour:
23:23:27 *** No such file:
"/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/Main.thy"
23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of
