[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, usingserlib
for Coq datasertop
: several toplevels with different use cases, usually replacements forcoqc
/coqtop
;sertop
is really couple withserapi
, just a tiny shell over it, howeversercomp
and 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-serapi
coq-sertools
:sercomp
,sertok
and related CLI tools, could depend oncoq-serapi
or 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.