Re: [isabelle-dev] AFP broken

2016-10-19 Thread Makarius
On 19/10/16 20:23, Florian Haftmann wrote: >> isabelle: ae7c11573922 tip >> afp: 1bffa6708aea tip >> *** [line 5 of >> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] >> error: command "theory" expected, >> *** but identifier was found: >> *** header I have also noticed

Re: [isabelle-dev] Distro broken

2016-10-19 Thread Makarius
On 19/10/16 13:38, Lars Hupel wrote: > Oh, nothing went wrong: Jenkins sent an email immediately after the > push, and the status page also indicated the failure. Automation working > as expected. But that did not help. Florian experienced the broken repository just in the way it occasionally

Re: [isabelle-dev] Distro broken

2016-10-19 Thread Lars Hupel
Oh, nothing went wrong: Jenkins sent an email immediately after the push, and the status page also indicated the failure. Automation working as expected. Cheers Lars On 19 October 2016 11:11:21 CEST, Makarius wrote: >> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb

[isabelle-dev] jdk-8u112

2016-10-19 Thread Makarius
With Isabelle/ae7c11573922 we are on jdk-8u112, which is the current scheduled release by Oracle, see also http://www.oracle.com/technetwork/java/javase/8u112-relnotes-3124973.html Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] AFP broken

2016-10-19 Thread Florian Haftmann
> isabelle: ae7c11573922 tip > afp: 1bffa6708aea tip > *** [line 5 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory