Hi all,
Somewhere between 43ca06e6c168 and 6975db7fd6f0, I seem to have broken the AFP
entry Lam-ml-Normalization. However, I cannot reproduce the problem on my
machine -- whether in Proof General nor using isabelle make.
On the other hand, I do get the following disturbing messages in Proof
Hi again,
On the other hand, I do get the following disturbing messages in Proof
General:
Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 494
Toplevel.end_proof(1)(1)(1)
End of trace
Update: The same problem occurs already with revision 6975db7fd6f0, i.e.
On Thu, 17 Nov 2011, Jasmin Christian Blanchette wrote:
On the other hand, I do get the following disturbing messages in Proof General:
Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 494
Toplevel.end_proof(1)(1)(1)
End of trace
Update: The same problem occurs
Hi Makarius,
Am 17.11.2011 um 12:12 schrieb Makarius:
This is merely a consequence of
changeset: 45486:600682331b79
user:wenzelm
date:Mon Nov 14 16:16:49 2011 +0100
files: src/Pure/Isar/runtime.ML
description:
more detailed exception_trace: in Poly/ML 5.4.x
On Thu, 17 Nov 2011, Makarius wrote:
When it comes to the AFP failure, there's a second AFP failure, in
JinjaThreads, that's obviously related to the servers' being down
yesterday; the Lam-ml-Normalization failure could be due to that, too.
I am experiencing Lam-ml-Normalization problems
On 11/17/2011 11:58 AM, Jasmin Christian Blanchette wrote:
Hi again,
When it comes to the AFP failure, there's a second AFP failure, in
JinjaThreads, that's obviously related to the servers' being down yesterday;
the Lam-ml-Normalization failure could be due to that, too. Lukas is helping
