When Rocq 9.0 is our minimum...

[jdchristensen]

Sometime over the next few months, I recommend that we make Rocq 9.0 (released in March 2025) our minimum supported version. When we decide to do so, here are some tasks:

• Wait for Dune 3.21 which introduces support for Rocq
  • No longer needed
• Update various places that indicate what the minimum version is, e.g. coq-hott.opam.template, flake.nix, maybe more.
• Update CI to no longer do 8.x builds. Instead, do 9.0, 9.1 and dev.
  • ci: bump minimal rocq version and improve ci #2338
• Update README.md and INSTALL.md to mention Rocq instead of Coq.
• Update library name from Coq-HoTT to Rocq-HoTT (or HoTT-Rocq if we want a funny name).
• Update the build scripts to use the new binary name, e.g. rocq instead of coqc. Then remove the opam dependency on coq-core.
• Handle the TODO in Basics/Overture about internal_paths_rew.
• Handle other TODO items that apply (search for 8.19, 8.20, 9.0).
• Get rid of warnings produced by Rocq during builds with >= 9.0. E.g. Notation vs Abbreviation.
• Get rid of places where we have silenced warnings. For example, change "Coq" to "Stdlib" in imports, and remove the silencing of deprecation warnings there.

Items two and three should be done together and be done first, but the rest are fairly independent, so they can be done in independent PRs as people find the time.

Feel free to add tasks to the list or make edits.

[jdchristensen]

@Alizter I just saw that you added "Wait for dune 3.21." But I think items two and three on the list can be done already. (Item 6 probably requires waiting for 3.21.)

Supporting 8.20 with a large development I'm doing is a bit of a pain, so I think it's time to make 9.0 our minimum. Can you adjust the CI to build 9.0, 9.1 and dev, and adjust the opam/nix files to make 9.0 the minimum? Then we can tackle other things on the list as we have time.

[Alizter]

Since the nix flakes use dune to build it has been a bit tricky to update those. We plan to release Dune 3.21 soon enough. It's currently undergoing testing with opam ocaml/opam-repository#29096. 3.21 includes a contribution to add support for Rocq, but I am not certain yet if it fixes the problems here. I can try to have a look over the weekend.

[jdchristensen]

@Alizter I'm a bit confused by your comment, since the nix build already is targeting 9.0, as far as I can see from the build log. So with 9.0 as the minimum, nothing would need to immediately change about the nix build. And our other builds already have at least one job targeting dev, so we are also able to support >= 9.0 with current dune.