# Re: [isabelle] Exporting Proof Terms to Text File

On Mon, 5 Nov 2012, Gransden, Thomas wrote:

`I'm looking for some guidance to complete a task that I would like to
``do.
`
In my theory file, I have the following code:
ML {*
val thm = @{thm "a1"};
val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm));
*}
ML {*
Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf'');
*}

`which gives me a proof term, as required. I would like to export the
``proof terms for each lemma in my theory file into a text file, so that I
``can do some analysis on the proof steps used in each proof.
`

`These are actually two independent things: writing stuff to a file and
``analysing what the prover did internally. Isabelle/ML is a quite able
``language to do analysis of symbolic datastructures, so if you stay within
``that environment you don't have to read or write files. File-system
``operations introduce statefulness that make it hard to work reliably in a
``multi-version multi-threaded environment like Isabelle --- unless you
``force it into sequential TTY mode and spoil the game.
`

`If you still do need to externalize and export material from Isabelle/ML,
``the current way to do it (in Isabelle2012) is via the XML data encoding,
``and prefereably the YXML transfer syntax (then you don't have to struggle
``with XML parsers on the other side). See $ISABELLE_HOME/src/Pure/PIDE/
``with xml.ML and yxml.ML in particular. There are also Scala versions of
``the same. Example applications are $ISABELLE_HOME/src/Pure/term_xml.ML
``for the main logical datatypes of Isabelle.
`
This is all perfectly normal Isabelle/ML user space.

`Moreover, see https://bitbucket.org/makarius/yxml where the same approach
``is made independent of Isabelle/ML, to work in plain SML or OCaml.
`

`I still hope that more people will pick up this simple and efficient
``approach to externalize ML datastructures, without the full burden of XML
``getting in the way.
`

`When doing the sort/typ/term application myself, I also tried the same for
``the proof datatype, and eliminate the old Pure/Tools/xml_syntax.ML in the
``course. Unfortunately, I failed to apply the proof reconstruction
``functions in the way they were documented 10 years ago, and did not spend
``further time to investigate the current situation.
`

`So ultimately, it is probably a matter to motivate Stefan Berghofer to
``brush up his proof term interfaces to work with current Isabelle and the
``XML/YXML data representation smoothly.
`
Makarius

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