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
sernameonly 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: Feb 06 2023 at 06:29 UTC