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

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Nov 17 11:58:42 CET 2011

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. 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

    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".

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 find out.


More information about the isabelle-dev mailing list