CoqSerapi Usage Question about coq-serapi HOT 6 CLOSED

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

from coq-serapi.

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.

from coq-serapi.

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

from coq-serapi.

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.

from coq-serapi.

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.

from coq-serapi.

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)?

from coq-serapi.