Stream: SerAPI

Topic: Query proof terms

Mingzhe Wang (Oct 18 2021 at 05:37):

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?

Karl Palmskog (Oct 18 2021 at 08:58):

@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

Emilio Jesús Gallego Arias (Oct 18 2021 at 10:27):

@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]

Emilio Jesús Gallego Arias (Oct 18 2021 at 10:29):

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

Last updated: Jun 01 2023 at 12:01 UTC