Re: [isabelle] proof terms & program extraction



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






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