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 already with revision 6975db7fd6f0, i.e. it has nothing
to do with my recent changes to the "metis" proof method and is apparently
unrelated to the AFP failure. To reproduce it, fire up Proof General with the HOL image
and process
theory Scratch
imports Main
begin
lemma "a : {x. P x} ==> P a"
proof -
assume "a : {x. P x}"
hence "a : P" apply (metis Collect_def) done
The disturbing error message should appear on the "done".
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 intermediate handlers
reset the trace (cf. Poly/ML SVN 1110);
It has the advantage that the exception trace becomes again more
informative (as it used to be in Poly/ML 5.3), at the cost of some
irrelevant traces about Toplevel.UNDEF, which is part of the normal
operation of the Isar interpreter.
BTW, you seem to have Toplevel.debug enabled by default. Without that you
don't get traces in the first place. (At the moment Toplevel.debug
controls exactly the exception trace, no more no less.)
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 since a couple of weeks,
but this is only due to an update of my LaTeX installation on Mac OS X.
Otherwise the session seems to be fine, and should still work on the usual
Linux systems.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
