COQ_USE_DUNE affects the build of coq through opam

[ana-borges]

If COQ_USE_DUNE is set, then the opam installation of coq will try to use dune and end up not installing anything.

Steps to reproduce:

export COQ_USE_DUNE=true
opam switch create test 4.12.0
opam update
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq -vv # observe dune is being used and an error is produced

Cf. rocq-prover/rocq#14469 and the zulip discussion.

[Blaisorblade]

Seems a duplicate of ocaml/opam-repository#18836, has the same instructions, and coq-released does not package Coq. This can probably be closed.

[palmskog]

Hmm, I don't think there was a solution to the opam-repository issue, and we have lots of Coq packages here in core-dev, so I think we should keep this open in case people run into it or there is a solution.

[ejgallego]

I think the problem was solved by ocaml/opam-repository#19663 , so indeed we can update the opam files here in a similar fashion. This is not a problem anymore in coq.dev , that is to say, Coq master doesn't use that variable anymore.