feat: Release coqorg/coq:8.20-rc1

[erikmd]

cf. @proux01's comment in coq/coq#18882 (comment)

8.20-rc1 is now available in core-dev: coq/opam#3058

bignums is already available in extra-dev: coq/opam#3054

IINM, the last required ingredient before merging the PR is coq-serapi

[erikmd]

Hi @ejgallego ! when you have some time, could you prepare a coq-serapi tag 8.20+rc1+XXX ?

then, we'll be able to open a PR targeting extra-dev similar to this one:

• add coq-serapi.8.19+rc1+0.19.0 to extra-dev coq/opam#2877 (that was opened by @palmskog)

and release 8.20+rc1 in docker-coq.

Many thanks!

[palmskog]

@ejgallego unless you have reservations, I will prepare a SerAPI tag in the next day or so.

[palmskog]

@erikmd @ejgallego it doesn't look feasible for me to do a tag due to rocq-archive/coq-serapi@c4685e3 which makes coq-serapi depend on coq-lsp. Since serlib has moved to coq-lsp, it may be time to remove coq-serapi from the Docker images...

[erikmd]

Hi @palmskog ! OK. What make you think that it'd be tricky (or impossible (or a bad idea)) to still keep coq-serapi in docker-coq ?

And what could we propose for projects that use docker-coq + alectryon?
(FWIW, here is an example project of this kind)

[palmskog]

@erikmd since serlib has migrated to Coq-LSP, you are going to need tags of both Coq-LSP and SerAPI, and I don't know if these will be forthcoming. It's not obvious to me if Coq-LSP as a whole should be included in the Docker images, since it may be updated many times for a single Coq version (so images will have to change a lot).

[proux01]

I do agree, let's remove it. We already have many packages available for 8.20+rc1 in both Nix and Opam, it makes no sense to further delay the Docker image.

[ejgallego]

As you prefer folks, there are many different possibilities here; coq-lsp has a working 8.20 branch so I can make a tag there and a SerAPI tag too.

All the current SerAPI users have been either migrated to coq-lsp or will do soon, so unless someone would like to volunteer to maintain SerAPI the 8.20 release will be the last one.

[erikmd]

Hi, thanks for your comments.

We already have many packages available for 8.20+rc1 in both Nix and Opam, it makes no sense to further delay the Docker image.

@proux01 Note that coqorg/coq:8.20 = coqorg/coq:8.20-alpha is already available from the v8.20 tag, which is codewise equivalent to 8.20+rc1. So the situation is really not blocking for docker-coq users.

Also, not-shipping SerAPI in-docker-coq anymore would be a major change (currently it is included for 8.8 ≤ coq < dev) and if ever we want to do so (do we want it?), I don't believe the sole argument that "it takes more time to release it" would convince end users… again, they can still use the coqorg/coq:8.20-alpha image meanwhile.

As you prefer folks, there are many different possibilities here; coq-lsp has a working 8.20 branch so I can make a tag there and a SerAPI tag too.

@ejgallego IMHO it would be nice indeed.

All the current SerAPI users have been either migrated to coq-lsp or will do soon, so unless someone would like to volunteer to maintain SerAPI the 8.20 release will be the last one.

Can you explain the rationale? Is coq-lsp just a dependency of SerAPI, or is it a drop-in replacement?

For instance, I don't know what will be the impact on Alectryon, which still uses SerAPI AFAIK? (Cc @cpitclaudel)

[ejgallego]

Can you explain the rationale? Is coq-lsp just a dependency of SerAPI, or is it a drop-in replacement?

Not drop in as-is, but could be made if someone would like to port sertop to Flèche. There is little point in doing so as for example ML users get huge advantages from moving to coq-lsp, or better said, Flèche which is the underlying engine.

The main thing that have changed in 8.20 is that serlib now lives in the coq-lsp monorepos. coq-lsp needs a lot of improvements to serlib, and having two separate repositories was nothing sort of a hell. A monorepos works much better for us. Actually here you are witness the hell I was having with coq-lsp, as it was depending on SerAPI, but reversed. (Basically I had to do a serapi release for multiple versions of Coq for any minor tweak)

Sorry I didn't anticipate the docker problem for RCs when I did this move, but I really needed serlib in coq-lsp repos as to implement some critical functionality for some projects.

One quick solution for SerAPI is actually to do the following for the 8.20 tag:

• put back the serlib directory in the 8.20 branch of SerAPI
• release as normal

Unfortunately I cannot do this before July 8th due to a combo of holidays and really critical stuff; but the process is simple, mainly:

• create a SerAPI 8.20 branch
• put back the directory in the sources from coq-lsp 8.20
• sed the dune files there so library names are coq-serapi.serlib instead of coq-lsp.serlib
• remove the dependency on coq-lsp

For instance, I don't know what will be the impact on Alectryon, which still uses SerAPI AFAIK? (Cc @cpitclaudel)

Note that for 8.20 a fully working SerAPI will be still kept. For 8.21, that will only happen if someone volunteers to maintain it.

[proux01]

@proux01 Note that coqorg/coq:8.20 = coqorg/coq:8.20-alpha is already available from the v8.20 tag, which is codewise equivalent to 8.20+rc1. So the situation is really not blocking for docker-coq users.

Wonderful! I didn't understood that. Let me announce the RC then.

[erikmd]

@ejgallego thanks a lot for your detailed explanation 👍 👍

having two separate repositories was nothing sort of a hell

Fully understand that!

Unfortunately I cannot do this before July 8th due to a combo of holidays and really critical stuff; but the process is simple, mainly: […]

OK, looks good! and there's no hurry: given what I said in my previous comment, no worries to wait till next week.

Note that for 8.20 a fully working SerAPI will be still kept. For 8.21, that will only happen if someone volunteers to maintain it.

Okay 👌

[erikmd]

friendly ping @ejgallego

→ if you can prepare a 8.20+rc1+XXX release/tag of coq-serapi this week, let me know! 🚀

[herbelin]

Note that for 8.20 a fully working SerAPI will be still kept. For 8.21, that will only happen if someone volunteers to maintain it.

How would you evaluate the time needed to "maintain" SerAPI relatively to the next versions of Coq compared to the time needed to switch from SerAPI to what coq-lsp provides as a replacement? (For instance, how does it compare to the time already spent at making adaptations to elpi, equations, metacoq or coq-lsp in the CI?) To maintain SerAPI, is it a question of half an hour per release, of several hours, of several days? To switch to coq-lsp, is it a matter of a few hours, of a few days?

[Zimmi48]

If the dual repo setup is inconvenient, what about moving everything in the coq-lsp repo and archiving the SerAPI repo?

IIUC Alectryon uses sertop, so we indeed need to either find a volunteer to maintain sertop (on top of flèche) or to port Alectryon to coq-lsp.

[erikmd]

IIUC Alectryon uses sertop, so we indeed need to either find a volunteer to maintain sertop (on top of flèche) or to port Alectryon to coq-lsp.

Cc @cpitclaudel, in case he wasn't aware of the discussion above

[erikmd]

(rebased on master)

[cpitclaudel]

Thanks @erikmd , I've seen the thread and I wrote about it here: https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Alectryon.20issues/near/455232324

[erikmd]

Hi all, I just chatted with @ejgallego who summarized the status of the SerAPI / coq-lsp release:

As discussed in other forums, we can do 3 things for releasing SerAPI:

1. wait for coq-lsp to reach opam, then release SerAPI for 8.20
2. put both coq-lsp and serapi in the coq-extra-dev repos
3. update serapi's 8.20 branch as not to depend on coq-lsp.

Note that the 2 is pretty hard to do; not long ago I proposed what I deem a better system, which is uploading the Coq RC releases to OPAM main repos (cf. coq/opam#2442).
We converged, but it is pending implementation by the release managers.

Meanwhile for 8.20, @ejgallego just implemented solution 3 and pushed a version of serapi that does not depend on coq-lsp (thanks Emilio!): https://github.com/ejgallego/coq-serapi/tree/v8.20

Cc @palmskog, do you think you could help to release this branch in opam, as soon as the coq-serapi CI passes?
(it would amount to coq-serapi version 8.20+rc1+XXX in coq-extra-dev)

[palmskog]

@erikmd OK, when v8.20 SerAPI branch passes CI I will release 8.20+rc1+0.20.0 and put it in extra-dev

[ejgallego]

@erikmd OK, when v8.20 SerAPI branch passes CI I will release 8.20+rc1+0.20.0 and put it in extra-dev

@palmskog , CI is good now, took a little bit more effort than I had anticipated, but IMHO RC release ready to go (and will be the final one too)

I will open a topic on Zulip to discuss 8.21 plans.

[erikmd]

Thanks a lot @ejgallego!

[ejgallego]

Thanks to you!

[cpitclaudel]

Thanks a lot!! :)

[ejgallego]

How would you evaluate the time needed to "maintain" SerAPI relatively to the next versions of Coq compared to the time needed to switch from SerAPI to what coq-lsp provides as a replacement? (For instance, how does it compare to the time already spent at making adaptations to elpi, equations, metacoq or coq-lsp in the CI?) To maintain SerAPI, is it a question of half an hour per release, of several hours, of several days? To switch to coq-lsp, is it a matter of a few hours, of a few days?

Answer to this @herbelin is that it depends on the expertise and experience of the team in charge of that.

I'd prefer tho to discuss maintenance topics on their own issue / meeting, after catching up it seems to me that the discussion is happening in a scattered way which makes it hard to follow.

IIUC Alectryon uses sertop, so we indeed need to either find a volunteer to maintain sertop (on top of flèche) or to port Alectryon to coq-lsp.

IMHO there is no point for Alectryon to keep using sertop, what Flèche-based tools offer is IMHO much better suited as of today, and much simpler to maintain IMHO.