Stream: SerAPI

Topic: Machine-generated gallina terms?


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

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

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

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?

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

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