Coq manual build with dune

Developing the Coq system
1

Sorry for the very naive question, I have not compiled Coq for some time. I have read INSTALL.md and dev/doc/build-system.dune.md, but I can’t I find an explanation for this:

$ cd ~/coqdev
$ git clone https://github.com/coq/coq.git
$ cd coq
$ configure -prefix "$(pwd)/install"
$ make dunestrap
$ dune build -p coq-core,coq-stdlib,coq
$ dune install -prefix="$(pwd)/install" coq-core coq-stdlib coq
        opam (internal)
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
Deleting /home/courtieu/.opam/default/lib/coq-core/META
Installing /home/courtieu/.opam/default/lib/coq-core/META
Deleting /home/courtieu/.opam/default/lib/coq-core/boot/boot.a
Installing /home/courtieu/.opam/default/lib/coq-core/boot/boot.a
...

Why would a dune install -prefix=somewhere would install stuff somewhere else? Is it somehow due to that warning?
My main goal is to have a working coqtop somewhere that I can specify to proofgeneral.

2

The problem is really silly, dune install -prefix actually means dune install -p -r -e -f -i -x which actually dune things is a valid set of (separate) options, but different from dune --prefix which is what you want!

dune install should not accept all these options, please open a bug upstream.

3

Ha! Silly indeed! Thanks!

1 Like
4

Very silly; this has been fixed in Dune finally tho. Still some challenges remain in order to make dune more ergonomic.