Re: [isabelle] proof terms & program extraction
On 10/23/2014 11:28 AM, Daniel Weller wrote:
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
I found some information on that (maybe explicit proof terms have not been
generated by Isabelle?), but it seems outdated:  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, ...)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and