Shea Levy (Oct 06 2020 at 20:25): Shea Levy (Oct 06 2020 at 20:25):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?
Karl Palmskog (Oct 06 2020 at 20:35):if you are building proof terms outside of Coq that need to be checked by Coq, you basically only have two reasonable options:
Shea Levy (Oct 06 2020 at 20:37):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?
Karl Palmskog (Oct 06 2020 at 20:40):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
Karl Palmskog (Oct 06 2020 at 20:46):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: May 31 2023 at 09:01 UTC