Stream: Coq users

Topic: Wrong version installs


view this post on Zulip Robert Rand (Oct 16 2020 at 05:57):

Hi all,

I keep trying to install Coq and it keeps showing the following message when I type coqc -v (or coqtop -v):

The Coq Proof Assistant, version 8.10.1 (October 2020)
compiled on Oct 15 2020 23:23:16 with OCaml 4.08.0

This despite the fact that opam says "installed coq.8.12.0" and I've deliberately uninstalled all versions of Coq before reinstalling (I was getting this issue before). Any ideas what might be going on?

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2020 at 07:19):

which coqc would be a good start

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2020 at 07:21):

and then opam env

view this post on Zulip Karl Palmskog (Oct 16 2020 at 07:25):

ocaml --version might help as well

view this post on Zulip Robert Rand (Oct 16 2020 at 16:12):

which coqc gives /Users/rand/.opam/default/bin/coqc.

ocaml --version is ocaml --version The OCaml toplevel, version 4.08.0.

% opam env
OPAM_SWITCH_PREFIX='/Users/rand/.opam/default'; export OPAM_SWITCH_PREFIX;
CAML_LD_LIBRARY_PATH='/Users/rand/.opam/default/lib/stublibs:/Users/rand/.opam/default/lib/ocaml/stublibs:/Users/rand/.opam/default/lib/ocaml'; export CAML_LD_LIBRARY_PATH;
OCAML_TOPLEVEL_PATH='/Users/rand/.opam/default/lib/toplevel'; export OCAML_TOPLEVEL_PATH;
PATH='/Users/rand/.opam/default/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Library/TeX/texbin'; export PATH;

view this post on Zulip Kenji Maillard (Oct 16 2020 at 16:15):

and opam info coq ?

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:10):

it’d also help to know what are the commands that you run and that did not help

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:10):

just in case, what does opam switch say?

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:12):

also to be sure, are you running all commands in the same shell and path, and do those make a difference? opam lets you have different environments (called switches) and allows selecting different switches depending on environment variables.

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 18:13):

in the past, I’ve also gotten that behavior by installing programs on the wrong machine :-P

view this post on Zulip Robert Rand (Oct 16 2020 at 21:41):

opam info coq

<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><>  🐫
name                   coq
all-installed-versions 8.12.0 [default]
all-versions           8.3  8.4pl1  8.4pl2  8.4pl4  8.4.5  8.4.6~camlp4  8.4.6
                       8.5.0~camlp4  8.5.0  8.5.1  8.5.2~camlp4  8.5.2  8.5.3
                       8.6  8.6.1  8.7.0  8.7.1  8.7.1+1  8.7.1+2  8.7.2  8.8.0
                       8.8.1  8.8.2  8.9.0  8.9.1  8.10.0  8.10.1  8.10.2
                       8.11.0  8.11.1  8.11.2  8.12.0

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version       8.12.0
repository    default
pin           https://github.com/coq/coq/archive/V8.12.0.tar.gz
url.src:      "https://github.com/coq/coq/archive/V8.12.0.tar.gz"
url.checksum: "sha512=8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240"
homepage:     "https://coq.inria.fr/"
bug-reports:  "https://github.com/coq/coq/issues"
dev-repo:     "git+https://github.com/coq/coq.git"
authors:      "The Coq development team, INRIA, CNRS, and contributors."
maintainer:   "coqdev@inria.fr"
license:      "LGPL-2.1-only"
depends:      "ocaml" {>= "4.05.0" & < "4.12"}
              "ocamlfind" {build}
              "num"
              "conf-findutils" {build}
synopsis      Formal proof management system
description
          The Coq proof assistant provides a formal language to write
          mathematical definitions, executable algorithms, and theorems,
          together
          with an environment for semi-interactive development of
          machine-checked
          proofs. Typical applications include the certification of properties
          of programming
          languages (e.g., the CompCert compiler certification project and the
          Bedrock verified low-level programming library), the formalization of
          mathematics (e.g., the full formalization of the Feit-Thompson theorem
          and homotopy type theory) and teaching.

view this post on Zulip Robert Rand (Oct 16 2020 at 21:41):

opam switch
#  switch   compiler                    description
→  default  ocaml-base-compiler.4.08.0  default

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:15):

time for $(which coqc) --version

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:15):

(and no, that’s not guaranteed to match coqc --version)

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:17):

to double-check, open a new shell, check that which coqc finds the same binary, _then_ run coqc --version

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:17):

*new shell -> new terminal, probably

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:21):

to be clear, the two options I see are (1) opam install coq has a bug (2) your shell still finds an old coq version that was not uninstalled.

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:22):

(1) seems pretty unlikely; (2) is actually far too easy to trigger.

view this post on Zulip Shea Levy (Oct 16 2020 at 22:44):

Can do hash -d coqc within a single shell too.

view this post on Zulip Karl Palmskog (Oct 16 2020 at 22:45):

I would actually try running coqc --version with an absolute path, as in /Users/rand/.opam/default/bin/coqc --version

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:52):

@Shea Levy read my mind

view this post on Zulip Robert Rand (Oct 17 2020 at 03:39):

All of these show Coq 8.10.1. Any other ideas?

view this post on Zulip Robert Rand (Oct 17 2020 at 03:40):

Except hash -d coqc which fails with no such directory. (Also when I give the full path.)

view this post on Zulip Robert Rand (Oct 17 2020 at 03:41):

(Note that this is on Mac OS.)

view this post on Zulip Robert Rand (Oct 17 2020 at 03:54):

Note that I've tried uninstalling coq, at which point which coqc indeed shows command not found. It's just that if I install coq again, I get 8.10 (even if I say / its says 8.12).

I can also do the "Roots" things here (https://coq.inria.fr/opam-using.html), getting a new ~/.opam-coq.8.12.0 directory (which seems to be an entirely different opam install?) but I can't keep coqc pinned to its version of coq. (Also, I'd prefer not to have multiple opam directories.)

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 03:59):

entirely different opam install

Precisely

Does that give you the right Coq version in that folder?

I can't keep coqc pinned to its version of coq

?

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 04:01):

Also, that sounds extremely cursed...

view this post on Zulip Robert Rand (Oct 17 2020 at 04:14):

"Does that give you the right Coq version in that folder?"

Yeah, it does, but no matter what I do to my .zshrc file, opening a new terminal/tab reverts to 8.10.

(Also, I really don't want to go with this approach.)

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 09:59):

Opening a new zsh reverts to the old PATH, right? That's probably a more fixable problem; you probably have some code in other zsh init files that is interfering. Maybe you told opam init to automatically do opam env for you.

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 10:03):

I would try to find that code either way.

view this post on Zulip Paolo Giarrusso (Oct 17 2020 at 10:05):

Eventually, one way to not have multiple opam installs is to move away the broken one (and eventually remove it), but without a diagnosis that might not solve the problem.

view this post on Zulip Robert Rand (Oct 20 2020 at 05:21):

Sometimes you just burn everything down and start over.


Last updated: Jan 29 2023 at 06:02 UTC