I'm opening this issue [would a discussion be better, tho it overlaps with Zulip] to keep track of the general road-map for SerAPI.

Thanks to tools like https://github.com/cpitclaudel/alectryon , and several other papers, the number of users of SerAPI has grown considerably these last months; however, SerAPI is still a research, experimental project, and it is expected to evolve considerably.

Despite this, I think it is possible to provide a coordinated road-map for SerAPI users and developers, that should work for everybody.

As of today, SerAPI is composed of three quite independent components:

• serlib: serialization library, providing support for Sexp, Python, and JSON
• serapi: DSL for communication with Coq, using serlib for Coq data
• sertop: several toplevels with different use cases, usually replacements for coqc / coqtop ; sertop is really couple with serapi, just a tiny shell over it, however sercomp and friends only depend on serlib

Indeed, serlib is a quite independent project on its own, and used by other projects. We thus present the roadmap independtly for serlib and serapi:

serlib roadmap

serlib is little more than a wrapper over most Coq datatypes, which adds the corresponding [@@deriving ] clauses and workarounds some limitations of the current Coq's presentation.

The way I understand it, and after dune support landed in Coq, it makes sense to upstream this component to Coq itself. Unfortunately, it is not clear Coq developers will support this, as they don't seem very interested in serlib use cases, and moreover, finding a nice solution could require significant development time depending on the constraints that are required for such a merge.

rocq-prover/rocq#9271 contains a bit of discussion, but there is not general discussion on that yet. @Zimmi48 has expressed interest in the past.

A critical issue to resolve in order to improve serlib's maintenance is ejgallego/coq-lsp#761

serapi roadmap

With regards to serapi itself, the current list of issues are a good indicator of what we are missing. In many cases, most of the problems need to be addressed in Coq first, such as ejgallego/coq-lsp#331 #196 ejgallego/coq-lsp#353 , etc...

Apart from these small improvements, protocol-wise, we would hope to remain quite compatible for a while, tho it would be interesting to support some other standard protocols, as outlined in #26 ; however, LSP support for example has drawbacks from both Coq and LSP itself that makes this a questionable time investment.

But at some point, we could envision the 2.0 serapi protocol as LSP + a query language + a visualization language.

Supporting old SerAPI and Coq versions

Unfortunately, as of today the manpower to develop SerAPI is quite limited. We can only guarantee support for the last stable Coq version. Older versions can however be maintained by volunteers.

Additional considerations

The Coq universe project, to be published soon, should provide a better overview of the general Coq roadmap on many of the areas SerAPI tries to address, and a view on how SerAPI would fit into that.