Hello, I am new to SerAPI. I hope to extract all the proof terms of a coq source file (like the output of "Print LemmaName."). I tried the command like "(Query ((sid 5)) Proof)" but it only returns something like "(Answer 4 (ObjList ((CoqProof ((Ser_Evar 4)) ()))))". Could anyone point out where I made the mistake? Can I extract proof terms using SerAPI?

@Mingzhe Wang to get serialized proof terms, you can either:

- use the SerAPI toplevel (
`sertop`

) in the style of Alectryon, or - use a more low-level command line tool that directly accesses Coq and Serlib, such as sername. Right now,
`sername`

only serializes the**types**of constants/lemmas, not the bodies/proofs of constants, but straightforward to change.

We produced a machine learning dataset of serialized Coq source files and lemma statement terms that should illustrate the general ideas: https://github.com/EngineeringSoftware/math-comp-corpus

Also, worth taking a look at the recent PyCoq which may be a better fit depending on the toolchain: https://github.com/ejgallego/pycoq

@Mingzhe Wang the `Proof`

query is meant to return the current proof, which is always an `Evar`

, that's confusing I know [it is meant to replace the `Show Proof`

command in a different way]

the command you are looking for is `(Query () (Definition "min_r"))`

for example

Last updated: Nov 29 2023 at 19:01 UTC