[isabelle-dev] Fwd: status (AFP)

Lukas Bulwahn bulwahn at in.tum.de
Thu Oct 20 23:29:40 CEST 2011

Hi all,

JinjaThreads currently probably fails because of the changeset 
6e422d180de8 (http://isabelle.in.tum.de/repos/isabelle/rev/6e422d180de8)

*** empty result sequence -- proof command failed
*** At command "apply" (line 2941 of "/home/kleing/afp/devel/thys/JinjaThreads/Compiler/JVMJ1.thy")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error

I could not even inspect the proof state where it fails, as my machine 
is not able to load the theory.
If anyone here has an educated guess how this proof can be fixed, you 
should try.
There are at least two machines, lxbroy10 in Munich, and one in 
Australia, running regularly that can check these guesses once you push 


-------- Original Message --------
Subject: 	status (AFP)
Date: 	Fri, 21 Oct 2011 06:31:55 +1100
From: 	Gerwin Klein <kleing at ertos.nicta.com.au>
To: 	undisclosed-recipients:;

The status of the following AFP entries changed or remains FAIL:
[JinjaThreads] is still on FAIL.

Full entry status athttp://afp.sourceforge.net/status.shtml

AFP version: development -- hg id a98f0ac6930a
Isabelle version: devel -- hg id c4fab1099cd0
Test ended on: lemma, Fri Oct 21 06:31:55 EST 2011.

Have a nice day,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111020/796913e3/attachment-0002.html>

More information about the isabelle-dev mailing list