Robert Rand (Oct 16 2020 at 05:57): 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?
Pierre-Marie Pédrot (Oct 16 2020 at 07:19):which coqc would be a good start
Pierre-Marie Pédrot (Oct 16 2020 at 07:21):and then opam env
Karl Palmskog (Oct 16 2020 at 07:25):ocaml --version might help as well
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;
and opam info coq ?
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
Paolo Giarrusso (Oct 16 2020 at 18:10):just in case, what does opam switch say?
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.
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
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.
opam switch
# switch compiler description
→ default ocaml-base-compiler.4.08.0 default
time for $(which coqc) --version
Paolo Giarrusso (Oct 16 2020 at 22:15):(and no, that’s not guaranteed to match coqc --version)
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
Paolo Giarrusso (Oct 16 2020 at 22:17):*new shell -> new terminal, probably
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.
Paolo Giarrusso (Oct 16 2020 at 22:22):(1) seems pretty unlikely; (2) is actually far too easy to trigger.
Shea Levy (Oct 16 2020 at 22:44):Can do hash -d coqc within a single shell too.
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
Paolo Giarrusso (Oct 16 2020 at 22:52):@Shea Levy read my mind
Robert Rand (Oct 17 2020 at 03:39):All of these show Coq 8.10.1. Any other ideas?
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.)
Robert Rand (Oct 17 2020 at 03:41):(Note that this is on Mac OS.)
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.)
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
?
Paolo Giarrusso (Oct 17 2020 at 04:01):Also, that sounds extremely cursed...
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.)
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.
Paolo Giarrusso (Oct 17 2020 at 10:03):I would try to find that code either way.
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.
Robert Rand (Oct 20 2020 at 05:21):Sometimes you just burn everything down and start over.
Last updated: Oct 13 2024 at 01:02 UTC