*To*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP*From*: Makarius <makarius at sketis.net>*Date*: Fri, 1 Aug 2014 20:54:34 +0200 (CEST)*Cc*: Fabian Immler <immler at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <A021A615-3CE5-4540-B5D3-5AB8C8CEFDD8@in.tum.de>*References*: <F8C86CDF-EEC4-46D5-B86C-72424AC17460@in.tum.de> <F1852934-2395-4226-B454-E4CD1341F36F@in.tum.de> <A021A615-3CE5-4540-B5D3-5AB8C8CEFDD8@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 1 Aug 2014, Jasmin Christian Blanchette wrote:

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.The attached changeset for "isabelle-release" fixes it. In short, it'snaive to expect "Thm.proof_body_of" never to throw any exceptions.

There is some documentation about it in the implementation manual: \item @{ML Thm.proof_of}~ at {text "thm"} and @{ML Thm.proof_body_of}~ at {text "thm"} produce the proof term or proof body (with digest of oracles and theorems) from a given theorem. Note that this involves a full join of internal futures that fulfill pending proof promises, and thus disrupts the natural bottom-up construction of proofs by introducing dynamic ad-hoc dependencies. Parallel performance may suffer by inspecting proof terms at run-time.

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

OK, I will push this over to bitbucket soon.

Makarius

**References**:**[isabelle] Fwd: Isabelle2014-RC0 segfault / sledgehammer raises exception DUP***From:*Fabian Immler

**Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP***From:*Jasmin Christian Blanchette

- Previous by Date: Re: [isabelle] 2014-RC1 issues: Duplicate annotations
- Next by Date: Re: [isabelle] 2014-RC1 issues: Duplicate annotations
- Previous by Thread: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Thread: [isabelle] Dependency cycle in code generator
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list