Stream: Coq devs & plugin devs

Topic: Installing coq.dev through opam, missing binaries

Ana de Almeida Borges (Jun 08 2021 at 15:05):

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?

Guillaume Melquiond (Jun 08 2021 at 15:32):

I do not see anything wrong. It should have worked.

Guillaume Melquiond (Jun 08 2021 at 15:34):

I don't think whereis would return anything, if the switch is not part of your PATH, but at least ls should have succeeded.

Guillaume Melquiond (Jun 08 2021 at 15:49):

I just tried it and it worked for me.

Ana de Almeida Borges (Jun 08 2021 at 16:14):

Thanks for checking. If it's working for you then it's not as worrying, but I have no idea how to troubleshoot it.

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:35):

@Ana de Almeida Borges what does opam list say?

Ana de Almeida Borges (Jun 08 2021 at 16:37):

# 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

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:41):

Umm, quite bizarre, maybe a problem with envs indeed, can you try the following updated list of steps:

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:41):

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

Guillaume Melquiond (Jun 08 2021 at 16:43):

eval $(opam env) should not be needed. In fact, I did not do it.

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:44):

Depends if you instrumented your shell or not with the opam magic [which is pretty broken on the other hand]

Ana de Almeida Borges (Jun 08 2021 at 16:46):

I have never done eval $(opam env), I think I do have that magic set up. But I'm testing it just in case

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:51):

You could try with opam install -vv for "verbose"

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:51):

and see what is going on

Emilio Jesús Gallego Arias (Jun 08 2021 at 16:52):

in the logs

Ana de Almeida Borges (Jun 08 2021 at 17:14):

Aha. The problem was export COQ_USE_DUNE=true. While useful for development, it broke opam's installation

Ana de Almeida Borges (Jun 08 2021 at 17:17):

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

Emilio Jesús Gallego Arias (Jun 08 2021 at 19:06):

oh damn, actually this is a problem deeper than Coq, env vars do affect the build of OCaml packages in an arbitrary way

Emilio Jesús Gallego Arias (Jun 08 2021 at 19:07):

for example Dune had to add a patch keeping a list of env vars that it will remove from the env for any build

Emilio Jesús Gallego Arias (Jun 08 2021 at 19:07):

otherwise the compiler may act weird

Emilio Jesús Gallego Arias (Jun 08 2021 at 19:08):

The fix IMO would be to remove the COQ_USE_DUNE variable altogheter

Ana de Almeida Borges (Jun 09 2021 at 11:14):

https://github.com/coq/coq/issues/14469

Ana de Almeida Borges (Sep 28 2021 at 14:59):

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?

Emilio Jesús Gallego Arias (Sep 28 2021 at 15:05):

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

Ana de Almeida Borges (Sep 28 2021 at 15:12):

Hmm ok. I guess fixing the underlying problem is a whole different issue. If it's that simple I can write the PR myself.

Ana de Almeida Borges (Sep 28 2021 at 16:10):

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.

Ana de Almeida Borges (Sep 28 2021 at 16:12):

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.

Guillaume Melquiond (Sep 28 2021 at 16:12):

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.

Ana de Almeida Borges (Sep 28 2021 at 16:14):

Oh, ok, great then!

Ana de Almeida Borges (Sep 28 2021 at 16:31):

https://github.com/ocaml/opam-repository/pull/19663

Emilio Jesús Gallego Arias (Sep 28 2021 at 18:15):

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