Please pick the version you prefer for Coq 8.20 in Coq Platform 2025.01

[MSoegtropIMC]

The Coq team released Coq 8.20.0 on September 3rd, 2024.
The corresponding Coq Platform release 2025.01 should be released before Jan 31st, 2025.
It can be delayed in case of difficulties until Feb 28th, 2025, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.20.0.

Coq Platform CI is currently testing opam package coq-serapi.8.20.0+0.20.0
from official repository https://opam.ocaml.org/packages/coq-serapi/coq-serapi.8.20.0+0.20.0/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2025.01, please inform us as soon as possible and before Dec 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.20~2025.01 which already supports Coq version 8.20.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#449

[SkySkimmer]

serapi is unmaintained so probably should be dropped from the platform

[palmskog]

@SkySkimmer indeed it should be dropped in the Rocq 9 platform, but I don't see any point in dropping it right now, when a release for Coq 8.20 exists.

[ejgallego]

There could an issue here tho, if we drop SerAPI and we don't add coq-lsp/fcc/petanque which is the replacement.

I've been trying to get coq-lsp into the plaftorm for a long time, and spend a large amount of time ensuring the project was ready (in particular for Windows), but I'm unsure what the problem is.

cc: @MSoegtropIMC , can you elaborate?

[MSoegtropIMC]

@ejgallego : the problem was that cause of very severe technical issues and also because Romain could not support as much as originally planned there was no bandwidth to add new packages. It will be added soon (assuming there are no objections to the board). I definitely try to get it into the 8.20 release and also into an updated 8.19 release.

[ejgallego]

@ejgallego : the problem was that cause of very severe technical issues and also because Romain could not support as much as originally planned there was no bandwidth to add new packages.

I am not aware of any technical issues with coq-lsp PR for the platform, would you mind pointing them out?

I'm unsure what bandwith means here, the patch to add coq-lsp to the platform these days is a single line:

PACKAGES="${PACKAGES} coq-lsp.0.2.2+8.17"

tho indeed some users would benefit from some backported patches to Coq which I include in my packages.

There are dozen of users of the custom platform installers on windows that are running without issue.

It will be added soon (assuming there are no objections to the board). I definitely try to get it into the 8.20 release and also into an updated 8.19 release.

Cool, thanks! Let me know if I can be of help.

[ejgallego]

On the other hand, if someone would like to do a rocq-serapi release for 8.21, it should not take too long.

There are some minor API changes to adapt to, but that's all.

[Zimmi48]

@ejgallego : the problem was that cause of very severe technical issues and also because Romain could not support as much as originally planned there was no bandwidth to add new packages.

I am not aware of any technical issues with coq-lsp PR for the platform, would you mind pointing them out?

AFAIU the technical issues @MSoegtropIMC is talking about are related to the Coq Platform release, not coq-lsp. The consequence was just that Romain and Michael had no bandwidth left to add new packages to the release.

On the other hand, if someone would like to do a rocq-serapi release for 8.21, it should not take too long.

Here we are talking about the Platform for Coq 8.20 anyway.

[ejgallego]

Here we are talking about the Platform for Coq 8.20 anyway.

Oh sorry, I got confused as we discussed dropping SerAPI from the platform.

serapi is unmaintained so probably should be dropped from the platform

It should be dropped, but not for 8.20, that release is fully functional (unless of course it creates some other problems)

The consequence was just that Romain and Michael had no bandwidth left to add new packages to the release.

I see, thanks. I guess I don't understand the platform process to add new packages.

I was under the impression that once a PR is working and passing CI (as in the case of coq-lsp) it was a zero-effort task for the maintainers (pressing the merge button)

I seem to recall that there was some document on the procedure to add a package to the platform? But I cannot locate it now, do you folks have a pointer?

[MSoegtropIMC]

@ejgallego : another issue is that we decided to have a Coq Platform board to decide on new packages and cause of the technical issues we also didn't have time to make this fully functional, say establish appropriate discussion channels and the like. For LSP it should be a no brainer, but I don't want to question this process before it even was properly established by adding new packages without discussion. All in all you just happened to hit the worst time in quite a few years caused by an unlucky coincidence.

[ejgallego]

Thanks for the info @MSoegtropIMC , please forward coq/platform#319 to the board if needed. (Or let me know how to submit the request myself)

On the other hand, the request is almost 2 years old, so indeed it predates the board.

IMVHO, given that we are talking about a one-line patch with a full promise of platform support from upstream devs, having to wait 2 years is not a very encouraging experience.

[MSoegtropIMC]

This is all handled by the Coq Platform team - nothing to do except creating the issue in Coq Platform.

[MSoegtropIMC]

@ejgallego : can you please file in the Coq Platform repo an issue where you officially request to remove coq-serapi?

[ejgallego]

@MSoegtropIMC happy to do that, however maybe we should do a decision on coq-community/manifesto#160 to be sure no one is interested in maintaining it?

[Zimmi48]

@MSoegtropIMC let's not drop SerAPI in 8.20 though
For Rocq 9.0, there will just likely not be any SerAPI release.
As for the Coq-community issue, it should still remain open for a while I think. At least until the time of preparing the Platform for Rocq 9.0.