[meta] General roadmap
ejgallego opened this issue · 11 comments
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 JSONserapi: DSL for communication with Coq, usingserlibfor Coq datasertop: several toplevels with different use cases, usually replacements forcoqc/coqtop;sertopis really couple withserapi, just a tiny shell over it, howeversercompand friends only depend onserlib
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.
coq/coq#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.
@ejgallego how do you see the future for sertop and its sibling tools? My reading is that if serlib is upstreamed into Coq itself, serapi and sertop could take on their own independent existences as consumers of serlib, and it may make sense to package them separately. Would you still retain sertop in the coq-serapi repo here as serlib usage examples?
@ejgallego how do you see the future for sertop and its sibling tools? My reading is that if serlib is upstreamed into Coq itself, serapi and sertop could take on their own independent existences as consumers of serlib, and it may make sense to package them separately. Would you still retain sertop in the coq-serapi repo here as serlib usage examples?
sertop really depends on the serapi protocol, so I'm not sure how we would make them independent, maybe you mean sercomp?
Well, I meant sertop and serapi existing separately as packages so that people could select to install/use one or the other (and getting serapi as an implicit dependency of sertop). sertop could also be separated from sercomp, I guess.
serapi is just an OCaml library, you mean that? Sure, we could do that very easily if we have a need.
The idea would be that ejgallego/coq-serapi (the repo) provides a set of components/packages, buildable separately via Dune and opam but interrelated, that solve various research problems, e.g.,
coq-serapi: pure OCaml library that depends on serlib upstreamed in Coqcoq-sertop: OCaml library and CLI tool, depends oncoq-serapicoq-sertools:sercomp,sertokand related CLI tools, could depend oncoq-serapior not
What do you think?
Sounds good, I'd be happy to do the split if there is a need.
Only problem is that the package name for coq-serapi would conflict with the current one, suddenly, users wouldn't get sertop after doing opam install coq-serapi; IMHO that's a problem.
But you said that you consider serapi and sertop to be independent components (even as one depends on the other). The options then seem to be:
- have them continue to live in the same repo and package, even in spite of this
- set a roadmap goal that their independence should become better reflected to users and developers
For example, one could make coq-serapi a meta-package for coq-serapi-lib and coq-sertop, if user expectations are a concern.
Actually sertop is just a very thin shell over the serapi protocol, so indeed I shall correct my description on the issue.
It is sercomp and friends who are independent, and indeed don't depend on serapi, so we could indeed split these and make them depend on serlib.
Update on the roadmap, SerAPI 0.17 will introduce a new protocol based on Flèche, rest of points are to be discussed, as actually fleche depends on coq-serlib.
But at some point, we could envision the 2.0 serapi protocol as LSP + a query language + a visualization language.
The moment has come, SerAPI 0.17 will be the last release with official support for the "classic mode".
Starting with 0.18 , serapi will be based on coq-lsp; classic mode will hopefully be still be supported but frozen / deprecated, as long as there is not a critical problem in Coq itself impeding that.