Proposal to move project coq-serapi to coq-community

[ejgallego]

Project name:

coq-serapi

Initial author(s):

Emilio J. Gallego Arias, Clément Pit-Claudel, Karl Palmskog

Current URL:

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

Kind:

Coq Tooling

License:

Coq's LICENSE

Description:

Machine-Friendly, Data-Centric Serialization for Coq

Status:

maintenance only / unmaintained

All use cases are better served by coq-lsp suite of tools, however I'm opening this issue to see if there is community interest into maintaining SerAPI.

New maintainer:

looking for volunteers

[ejgallego]

Zulip discussion https://coq.zulipchat.com/#narrow/stream/256331-SerAPI/topic/Call.20for.20new.20maintainers.20.2F.20move.20to.20Coq.20Community

[palmskog]

For the record, the plan is for Alectryon to be ported away from SerAPI during spring of 2025. This leaves one major planned Coq version without Alectryon (chronologically 8.21.0). @ejgallego how much do you estimate the effort to be to keep SerAPI alive until then?

[ejgallego]

I estimate that the effort to keep SerAPI alive is more than the effort to port Alectryon to coq-lsp/fcc.

[dhilst]

How complex/often is the maitenance of coq-serapi? I remember doing one PR..

I'm currently not employed so I have some free time, I may maintain it depending on the complexity, as it is a new codebase to me

[ejgallego]

We already have a goaldump plugin in fcc, so if I understand things correctly, it should be trivial to update that plugin so it outputs the list of all sentences + goals in SEXP format.

This output should be a drop-in replacement for the current input of Alectryon.

[ejgallego]

How complex/often is the maintenance of coq-serapi? I remember doing one PR.

That's a good question. As of today, it is just a thin layer over Coq's STM and serlib, which is now hosted at coq-lsp monorepos. Maintaining it for new Coq versions should be easy.

However, developing new features or fixing some of the current bugs would be very hard, as these inherit from Coq's STM.

Hence, we phased SerAPI out and developed Flèche

[ejgallego]

Hi folks,

due to other commitments I won't be able to maintain SerAPI anymore, in particular I won't be able to make more releases.

I'm unsure how to proceed here in terms of timing, but if no interest in moving the project to Coq Community appears soon, I will officially remove coq-serapi from Coq's CI and archive the repository in the first week of November.