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:
sertop
) in the style of Alectryon, or 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: Jun 01 2023 at 12:01 UTC