Stream: Coq devs & plugin devs

Topic: Renamig tasks


view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:08):

Since I missed the Coq call I'm catching up with the notes.
The renaming project on GH looks nice. I did add an item, since it looks important to me, not sure essential as noted in the title, although other items look alike mine.
It is about the opam archive for rocq packages.

view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:09):

I think there is a little more general question about CI, i.e. being able to ci for coq 8.20 and rocq 9 (coq 8.21) without too many backflips

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:11):

Yep, we chatted a bit about that. The hope is to have some way to make user packages work with both Coq and Rocq versions, maybe by having a compat Coq 9 packages depending on Rocq 9 + a compat layer. I don't know if you're aware but you can click on items to display the notes about them

view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:14):

Yes, I looked into that, but I though you only talked about the coq package, not, say, coq-mathcomp.

view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:18):

Anyway, if my item has no place, just remove it

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:24):

Indeed I added no notes about what we discussed, but precisely we thought about coq-mathcomp :) The two items Rocq/Coq opam packages and the opam Rocq/Coq archive make sense

view this post on Zulip Pierre Roux (Sep 18 2024 at 08:34):

What we discussed was: having a coq.9 package that depends on rocq.9 and provides symlink/compat coq* commands that just call rocq*.

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 08:34):

The idea was: coq-mathcomp will depend on coq (which, starting at version 9, will depend on rocq) and rocq-mathcomp (when it exists) will depend only on rocq. The rocq package alone will not ship the compat layer.

view this post on Zulip Karl Palmskog (Sep 18 2024 at 08:35):

you mean coq-mathcomp-ssreflect will depend on Coq like ("coq" {>= "9.0"} | "rocq" {>= "9.0"}) in opam parlance?

view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:36):

I guess more like ("coq" {>= "8.18"} | "rocq")

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:36):

Ideally it won't need to depend on rocq explicitly. Only rocq-mathcomp-ssreflect would

view this post on Zulip Enrico Tassi (Sep 18 2024 at 08:36):

(assuming 8.18 is the lower bound)

view this post on Zulip Karl Palmskog (Sep 18 2024 at 08:37):

OK, so "rocq" will/can depend on "coq-core"?

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 08:37):

The converse

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 08:38):

coq-core.9 will depend on rocq-core.9 and add a layer of compat

view this post on Zulip Karl Palmskog (Sep 18 2024 at 08:38):

it seems one would need some separate infrastructure to test this stuff, our opam archive CI will not cut it

view this post on Zulip Pierre Roux (Sep 18 2024 at 08:39):

Indeed, OPAM CI will need some update

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:40):

Why?

view this post on Zulip Karl Palmskog (Sep 18 2024 at 08:40):

you would have to at least test with and without the compat layer, no?

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:41):

For rocq-* packages yes, for coq-* packages you would always need the compat layer

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 08:42):

Do you anticipate that rocq-* packages may fail when the compat layer is installed? It seems quite unlikely to me.

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:43):

They might silently depend on coq* stuff being installed

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:44):

So the converse :)

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 08:44):

OK, then the CI should catch that, because it will test them in a fresh context where coq is not installed...

view this post on Zulip Matthieu Sozeau (Sep 18 2024 at 08:46):

Yep, I think that's exactly what @Karl Palmskog was refering to, needing an environment with coq=rocq+compat and one with just rocq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 18 2024 at 11:50):

Another tasks that could be done (but would be a bit more work) is to take the chance and start packing the rocq-core libraries, so we can have a Rocq namespace in the OCaml-land.

It would be a bit more work as we couldn't use Dune's (deprecated_library_name ...) directly, but we would have to build some wrappers.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 18 2024 at 13:47):

Another possible TODO: change the default branch of Rocq from master to main

view this post on Zulip Mario Carneiro (Sep 18 2024 at 14:15):

are the two occurrences of "coq" in https://github.com/coq/coq getting renamed, and if so, what is the fallout of that? Does github let you rename an organization?

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:20):

Yes, both will change and yes, GitHub lets you rename: https://docs.github.com/en/organizations/managing-organization-settings/renaming-an-organization
I guess the full name will be rocq-prover/rocq (on the model of Lean). I have already registered the organization to avoid having the name preempted by someone else as a username or an organization name.
We discussed yesterday when to do the org/repo renaming, and the conclusion was: at the same time that we make the new website public (so rather late in the cycle, likely close to Christmas).

view this post on Zulip Yann Leray (Sep 18 2024 at 14:22):

What can be done to ensure that coq/coq redirects to the new repo for as long as possible ?

view this post on Zulip Karl Palmskog (Sep 18 2024 at 14:23):

if org renaming works like repo renaming, there will be a permanent redirect

view this post on Zulip Yann Leray (Sep 18 2024 at 14:24):

I should have opened the link first; Coq is big enough that the redirect should indeed be permanent

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:25):

From the GitHub documentation, there will be a redirect for as long as a new coq/coq is not created. Because the old organization name can be preempted by anyone, we should recreate a coq organization right after having renamed the current one, and not create any repositories in it (in particular avoid any repository name of the former coq organization).

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:27):

Oh @Yann Leray, are you refering to "or that had more than 100 clones" -> "GitHub permanently retires the old owner name and repository name combination (OLD-OWNER/REPOSITORY-NAME) when you rename your account."?

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:27):

I had missed this because it is buried among two cases that seem specific to GitHub Actions.

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:27):

I am planning in any case to write to GitHub support soon to clarify all of this and make sure we don't do anything wrong when renaming.

view this post on Zulip Enrico Tassi (Sep 18 2024 at 14:28):

do they also redirect coq.github.io? IIRC the opam repository uses that for the metadata

view this post on Zulip Enrico Tassi (Sep 18 2024 at 14:30):

but maybe I'm mistaken, things changed "recently"

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:32):

Hum, I'm not sure, but we should indeed also check what needs to be done for the opam repository, because currently coq.inria.fr has a CNAME pointing to coq.github.io, but rocq-prover.org is instead using a dedicated VM, it won't use GitHub Pages anymore. (And this also raises the question of how we deploy the documentation.)

view this post on Zulip Théo Zimmermann (Sep 18 2024 at 14:34):

In any case, this is another argument in favor of renaming the organization late in the process.


Last updated: Oct 13 2024 at 01:02 UTC