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
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
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
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_DUNEbefore 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!
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