Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP



Hi Lars & Fabian,

> I have recently seen this behavior as well (in Isabelle2014-RC1) and can reproduce it as follows (it seems important that mashine learning is "finished"):
> 
> theory Scratch imports Main begin
> 
> lemma True sledgehammer learn_isar by (rule TrueI)
> 
> notepad begin
> fix P
> have "P"
>   by nothing
> have "P"
>   (* invoke s/h here *)
> 
> inserting a textual "sledgehammer" or "sledgehammer learn_isar" command shows nothing in the output, but colors the command in red.

Thank you for your report! The attached changeset for "isabelle-release" fixes it. In short, it's naive to expect "Thm.proof_body_of" never to throw any exceptions.

Makarius: Could you apply the attached changeset to "isabelle-release"? Thanks.

Jasmin

Attachment: try_proof_body
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.