[coq] Deprecation and removal of `(lang coq)` for Dune 3.24

[ejgallego]

Hi folks,

this issue is a reminder to remove (lang coq) from dune once Dune 3.23 is released.

(lang coq) has been replaced by (lang rocq), which is expected to reach stability very soon. Existing users of the experimental (lang coq) build language are expected to upgrade to Rocq, and add upper bounds to dune for packages that would need to work in older dune versions.

cc: #12035 #11572 #6445 #9348

[shilangyu]

Thanks for your effort in bringing Rocq 9 support!

I see the new Rocq plugin was merged. What would be a way to test this dune plugin so that I can provide feedback?

[ejgallego]

Thanks for your interest @shilangyu ; best way to test this right away is to use opam to pin dune to the main branch.

There may be easier ways to do so with Nix, but I'm not familiar with them myself.

[Alizter]

3.21 will also be released soon so the changes should land there.

[shilangyu]

Tested dune 3.21 from the main branch. Replaced coq directives in dune files to the rocq equivalents. Replace the coq opam package with rocq-prover. I additionally used the (new?) _RocqProject file generation. Everything works great!

Pinned with opam pin add dune.3.21.0 https://github.com/ocaml/dune.git#6e9d965bb5bbadfe9cbf89314cb6f8ecaa845bd9.

Looking forward to the release!

[ejgallego]

Great! Thanks for the feedback @shilangyu ; props to all the contributors to Rocq's great test-suite, they did a huge effort to write a large number of tests which has been proven useful in testing the new mode.