What is the purpose of coq-serapi's existance and why can't everything be done in coqtop? about coq-serapi HOT 5 CLOSED

Hi @brando90 , that's a legitimate question.

There are many reasons that you may want to prefer serapi over coqtop, I think the main ones are:

• document-oriented API vs REPL: this is very convenient in a lot of applications, morever serapi provides many more operations that are not available in coqtop such as controlled parsing, printing goals at an arbitrary point, invalidation with dep tracking, etc... Moreover, parsing coqtop output can be pretty challenging as it is meant for human readers and can change often.
• serialization: coqtop uses a printer that is in general not injective, that's a requirement for many applications, for example, to be able to properly modify some existing term (think for example of a tool that would like to implement renaming of variables)

from coq-serapi.

@ejgallego same question about the new lsp coq interface. Why do we need it?

Given I don't really know how to manipulate Coq terms in ocaml, is coqtop just all I need? (e.g. to extract data for Machine Learning ML or check ML made proofs)

from coq-serapi.

https://github.com/ejgallego/coq-lsp

from coq-serapi.

Hi @brando90 , I'm sorry the situation is confusing; I'd love to improve it, but we are struggling to get some time to work on these projects as of late.

coq-lsp main reason of existance is to provide a "language server" than can be used from other editors such as emacs or VSCode. It turns out that the core engine is also useful for other users, so indeed, we are using coq-lsp as a unified tool.

You could think of it as "SerAPI 2.0".

I hope this helps, let me know how we can make the current situation less confusing.

from coq-serapi.

I take the freedom to mark this issue as "answered", feel free to re-open or to ping us in Zulip to further discuss.

from coq-serapi.