Rocq 9.0 release + Coq 9.0 compatibility packages

[mattam82]

See e.g. rocq-prover.org/release/9.0.0

[proux01]

This is also missing a coq metapackage, something along the lines

synopsis: "Compatibility metapackage for Coq after the Rocq renaming"
maintainer: ["The Rocq development team <coqdev@inria.fr>"]
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/"
doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
  "rocq-prover" {= version}
  "coq-core" {= version}
  "coq-stdlib" {= "9.0.0"}
  "coqide-server" {= version}
]
dev-repo: "git+https://github.com/coq/coq.git"

as well as the coqide-server package.

[SkySkimmer]

The "lower bounds" jobs are failing on ocaml 5.x
This may be related to whatever the ocamlfind changelog means by "1.9.6:: Support for OCaml-5 (as far as foreseeable) (David Allsopp)" as we see CI downgrade ocamlfind 1.9.8 to 1.9.5 (we advertise compatibility with ocamlfind down to 1.8.1 but I guess some other bound stops it from downgrading that low, on ocaml 4.09 it did downgrade to 1.8.1)

[mattam82]

This is also missing a coq metapackage, something along the lines

synopsis: "Compatibility metapackage for Coq after the Rocq renaming"
maintainer: ["The Rocq development team <coqdev@inria.fr>"]
authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/"
doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
  "rocq-prover" {= version}
  "coq-core" {= version}
  "coq-stdlib" {= "9.0.0"}
  "coqide-server" {= version}
]
dev-repo: "git+https://github.com/coq/coq.git"

as well as the coqide-server package.

There are in a separate PR (along with rocqide) to not slow down this one, i.e. #27614

[proux01]

There are in a separate PR (along with rocqide) to not slow down this one, i.e. #27614

Why not but coqide-server is usually ok, since it does not depend from lablgtk.

[mattam82]

There are in a separate PR (along with rocqide) to not slow down this one, i.e. #27614

Why not but coqide-server is usually ok, since it does not depend from lablgtk.

Oh right, I missed that.

[mattam82]

The ocaml-ci problems with "no-source" are similar to #27237 , for our compatibility metapackages that do not build or install anything by themselves.

[mattam82]

Now rebased on revdeps fix