[isabelle-dev] AFP failure in Lam-ml-Normalization

[Makarius]

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