Installing coq.dev
through opam
used to work, but now it seems it is not creating the binaries, or at the very least I can't find them. opam
still thinks it is installed, though.
opam switch create test 4.12.0
opam update
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.dev
opam list # coq appears listed, dev version
whereis coqc # not found
whereis coqtop # not found
ls ~/.opam/test/bin/coq* # nothing
find / -name "coqc" 2> /dev/null # finds only the binaries in my other opam switches
Am I missing something or should I open an issue?
I do not see anything wrong. It should have worked.
I don't think whereis
would return anything, if the switch is not part of your PATH
, but at least ls
should have succeeded.
I just tried it and it worked for me.
Thanks for checking. If it's working for you then it's not as worrying, but I have no idea how to troubleshoot it.
@Ana de Almeida Borges what does opam list
say?
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 3 Virtual package relying on a GMP lib system installation
coq dev Formal proof management system
dune 2.8.5 Fast, portable, and opinionated build system
ocaml 4.12.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.0 Official release 4.12.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.1 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
Umm, quite bizarre, maybe a problem with envs indeed, can you try the following updated list of steps:
opam switch create test 4.12.0
eval $(opam env)
opam update
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.dev
eval $(opam env)
should not be needed. In fact, I did not do it.
Depends if you instrumented your shell or not with the opam magic [which is pretty broken on the other hand]
I have never done eval $(opam env)
, I think I do have that magic set up. But I'm testing it just in case
You could try with opam install -vv
for "verbose"
and see what is going on
in the logs
Aha. The problem was export COQ_USE_DUNE=true
. While useful for development, it broke opam
's installation
The logs show that make
was called, which showed the Welcome to Coq's Dune-based build system. Common developer targets are:
message, then the command
/home/ana/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/ana/.opam/test2/.opam-switch/build/coq.dev)
which gives the message To install Coq using dune, use 'dune build -p P && dune install P'
, and then opam
happily announces Done
oh damn, actually this is a problem deeper than Coq, env vars do affect the build of OCaml packages in an arbitrary way
for example Dune had to add a patch keeping a list of env vars that it will remove from the env for any build
otherwise the compiler may act weird
The fix IMO would be to remove the COQ_USE_DUNE
variable altogheter
https://github.com/coq/coq/issues/14469
This is still a problem for released versions of Coq, as described here: https://github.com/ocaml/opam-repository/issues/18836
That issue was recently marked as stale, and it includes the following request:
We do need a coq package maintainer to submit these fixes to the opam-repository by forcing the variable to be unset in the build rules.
I'm not sure who to tag, is there anyone who could fix this?
Hi @Ana de Almeida Borges , anyone could do this, in the form of a PR for the opam files in opam-repository.
We just need to add unset COQ_USE_DUNE
before the call to make in the opam file
Hmm ok. I guess fixing the underlying problem is a whole different issue. If it's that simple I can write the PR myself.
Emilio Jesús Gallego Arias said:
We just need to add
unset COQ_USE_DUNE
before the call to make in the opam file
IIUC, if we do this and if a person is expecting to have COQ_USE_DUNE
set, installs coq through opam, and then continues doing stuff in the same terminal session, they will now have this variable unset, which will be unexpected.
It feels itchy to mess around with the environment behind the scenes. Perhaps it would be better to store the value of the variable, unset it, and then set it back at the end of the installation, although this sounds a bit convoluted.
Changing or removing an environment variable is process-local. The effect of unset
should not be able to escape the shell session launched by Opam.
Oh, ok, great then!
https://github.com/ocaml/opam-repository/pull/19663
Thanks @Ana de Almeida Borges , note that Coq master or 8.14 should not need the patch.
Last updated: Dec 07 2023 at 09:01 UTC