*To*: Daniel Weller <fraini at gmail.com>*Subject*: Re: [isabelle] proof terms & program extraction*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Fri, 24 Oct 2014 14:30:04 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CA+aehLiwto30-tKaVho4S7HrRsLFcre=twy8giW984P6QjXs+w@mail.gmail.com>*References*: <CA+aehLiwto30-tKaVho4S7HrRsLFcre=twy8giW984P6QjXs+w@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:13.0) Gecko/20120615 Thunderbird/13.0.1

On 10/23/2014 11:28 AM, Daniel Weller wrote:

Dear all, I'd like to try out the Isabelle program extraction mechanism "extract", but I have been unsuccessful so far. I found examples for this mechanism in Isabelle2014/src/HOL/Proofs/Extraction, but trying e.g. Euclid.thy, I get the error "reconstruct_proof: minimal proof object" on the line "extract Euclid". I found some information on that (maybe explicit proof terms have not been generated by Isabelle?), but it seems outdated: [1] gives a solution to the problem, but I could not apply that to the current version of Isabelle ("Isabelle -> Settings -> Full Proofs" does not exist in the jEdit IDE, the "usedir" tool does not exist anymore, ...)

Hi Daniel, it should be sufficient to start Isabelle/jEdit with the HOL-Proofs image, i.e. isabelle jedit -l HOL-Proofs Euclid.thy When using this image, it is no longer necessary to switch on proof objects explicitly. See also the following NEWS entry for Isabelle2013-1 (November 2013): * System option "proofs" has been discontinued. Instead the global state of Proofterm.proofs is persistently compiled into logic images as required, notably HOL-Proofs. Users no longer need to change Proofterm.proofs dynamically. Minor INCOMPATIBILITY. Note that compiling the HOL-Proofs image may require quite some time and memory. Greetings, Stefan

**Follow-Ups**:**Re: [isabelle] proof terms & program extraction***From:*Daniel Weller

**References**:**[isabelle] proof terms & program extraction***From:*Daniel Weller

- Previous by Date: Re: [isabelle] Easier quick PDF generation possible?
- Next by Date: [isabelle] OSX Yosemite
- Previous by Thread: [isabelle] proof terms & program extraction
- Next by Thread: Re: [isabelle] proof terms & program extraction
- Cl-isabelle-users October 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