Desired Behavior

We would like dune's Coq support to be able to call the new rocq binary instead of coqc.
Currently we need to use compatibility shims (opam package coq-core) on top of the rocq-core package to compile Rocq projects.
Ideally we want a solution that's compatible with both coqc and rocq usage.

Example

Dune coq support just fails if coqc is not installed right now.

Discussion

We are currently discussing the various design decisions regarding Rocq <-> dune integration here, and plan to contribute a solution. This issue hence for letting you know we're working on it and soliciting feedback if you have any:

https://rocq-prover.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Dune.20support.20for.20rocq.20binary/with/508283855