I'm starting a new project that will involve diagrammatic manipulations to generate values and proofs, and I'd like to send those terms to coq for verification/later use. It's not a normal editing interface, the user won't be writing any vernacular commands or terms directly. Is serapi recommended for this kind of use case?

if you are building proof terms outside of Coq that need to be checked by Coq, you basically only have two reasonable options:

- do it in OCaml and use Coq's OCaml API directly or
- use SerAPI in some way, e.g., input the proof terms through SerAPI's protocol

Karl Palmskog said:

if you are building proof terms outside of Coq that need to be checked by Coq, you basically only have two reasonable options:

- do it in OCaml and use Coq's OCaml API directly or
- use SerAPI in some way, e.g., input the proof terms through SerAPI's protocol

Is there some direct AST for gallina terms or something I can work in with SerAPI? Or does it all have to go through (potentially modified) parsing etc. on the coq end?

the AST provided by SerAPI for proof terms is mostly the same as Coq provides at the OCaml level. If you want to actually input Gallina (what a user would write, unelaborated definitions), they can be sent in as strings via SerAPI's protocol, which sends them to the parser, etc. See here for the various stages of processing: https://github.com/ejgallego/coq-serapi/blob/v8.12/FAQ.md#how-many-asts-does-coq-have

just because you use SerAPI, that doesn't mean you have to use the protocol. You can use SerAPI + Coq's OCaml API directly in OCaml, and then SerAPI can potentially save a lot of boilerplate for starting up Coq, etc. It might still be the case that a full-blown standalone Coq plugin is a better solution, though

Last updated: Feb 06 2023 at 05:03 UTC