Stream: SerAPI

Topic: Query proof terms


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Oct 18 2021 at 08:58):

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

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

view this post on Zulip 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]

view this post on Zulip 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: Feb 06 2023 at 06:29 UTC