CoqSerapi Usage Question

[ana-brendel]

I've been trying to use the provided module to execute some Coq code and reason about it in OCaml, but I have not been successful. I was wondering if there are any sample projects or bits of code that use Serapi to show how to use it?

For example, suppose that I just wanted add a definition for a list type and a fixpoint to compute the length, and then query for the length of some list. I had tried following various instructions from the documentation but had kept getting various errors (most common was the no such state exists or is found one). I figured I should ask to see if there was any example code that I could look at to learn from.

Thanks for your time!

[ejgallego]

Hi @ana-brendel !

What do you mean by "in OCaml" ?

The usual interface for SerAPI is via a SEXP-based top (which often people interface thru via Python).

In this model, you can just do:

(Add () "Definition a := 3.")
(Exec 2)
(Query ((sid 2)) ...)

Note that 2 is the sentence id returned by Add. Rest of ops are documented in the documentation from the README.

You may be facing two additional problems here:

• Displaying results from Coq is done via Feedback messages, that's incovenient.
• The Query protocol may not likely cover all your use cases.

Note that SerAPI has been replaced by Flèche (https://github.com/ejgallego/coq-lsp) which I'm sure will be much easier for you to use.

I recommend stopping by Coq's Zulip to further discuss any problems you may have.

[ana-brendel]

Sounds good, thank you! I'll take a look at Flèche. Thank you!

[ejgallego]

Cool @ana-brendel .

Unfortunately documentation may not yet be the most user-friendly, as the project is new and evolving quickly, but we'll be very happy to be of help; don't hesitate to ask if you have trouble with your use case.

[ejgallego]

In particular things that used to be pretty cumbersome to do in SerAPI are now easy, the model is quite different.

In some cases the reduction on code for SerAPI users is dramatic, so indeed let us know what is your concrete use case, and we'll try to figure how what is the right API for you.

[ana-brendel]

Is this a good place to explain the use case to get further insight, or would it be easier/better to send an email or communicate else where (I haven't really asked questions via GitHub before so I'm not sure what the best way to communicate)?

[ejgallego]

Hi @ana-brendel , I think Coq's Zulip, either in public or private is the most efficient way.