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.
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
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
Yes, I looked into that, but I though you only talked about the coq package, not, say, coq-mathcomp.
Anyway, if my item has no place, just remove it
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
What we discussed was: having a coq.9 package that depends on rocq.9 and provides symlink/compat coq* commands that just call rocq*.
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.
you mean coq-mathcomp-ssreflect
will depend on Coq like ("coq" {>= "9.0"} | "rocq" {>= "9.0"})
in opam parlance?
I guess more like ("coq" {>= "8.18"} | "rocq")
Ideally it won't need to depend on rocq explicitly. Only rocq-mathcomp-ssreflect
would
(assuming 8.18 is the lower bound)
OK, so "rocq"
will/can depend on "coq-core"
?
The converse
coq-core.9
will depend on rocq-core.9
and add a layer of compat
it seems one would need some separate infrastructure to test this stuff, our opam archive CI will not cut it
Indeed, OPAM CI will need some update
Why?
you would have to at least test with and without the compat layer, no?
For rocq-*
packages yes, for coq-*
packages you would always need the compat layer
Do you anticipate that rocq-*
packages may fail when the compat layer is installed? It seems quite unlikely to me.
They might silently depend on coq*
stuff being installed
So the converse :)
OK, then the CI should catch that, because it will test them in a fresh context where coq is not installed...
Yep, I think that's exactly what @Karl Palmskog was refering to, needing an environment with coq=rocq+compat and one with just rocq
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.
Another possible TODO: change the default branch of Rocq from master
to main
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?
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).
What can be done to ensure that coq/coq
redirects to the new repo for as long as possible ?
if org renaming works like repo renaming, there will be a permanent redirect
I should have opened the link first; Coq is big enough that the redirect should indeed be permanent
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).
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."?
I had missed this because it is buried among two cases that seem specific to GitHub Actions.
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.
do they also redirect coq.github.io? IIRC the opam repository uses that for the metadata
but maybe I'm mistaken, things changed "recently"
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.)
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