COQ_USE_DUNE affects the build of coq through opam

coq / opam

Archive for all Coq related OPAM packages organized in various repositories

https://coq.inria.fr/opam/www/

GNU Lesser General Public License v2.1

122 stars 165 forks source link

COQ_USE_DUNE affects the build of coq through opam #1736

Open ana-borges opened 3 years ago

ana-borges commented 3 years ago

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. https://github.com/coq/coq/issues/14469 and the zulip discussion.

Blaisorblade commented 2 years ago

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

palmskog commented 2 years ago

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 commented 2 years ago

I think the problem was solved by https://github.com/ocaml/opam-repository/pull/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.