How do I have opam show me the version to download a package?

I tried:

(iit_synthesis) brando9/afs/cs.stanford.edu/u/brando9/software_foundations_solution/book $ opam search coq
# Packages matching: match(*coq*)
# Name           # Installed # Synopsis
archsat          --          A first-order theorem prover with formal proof output
coq              --          Formal proof management system
coq-lsp          --          Language Server Protocol native server for Coq
coq-native       --          Package flag enabling coq's native-compiler flag
coq-of-ocaml     --          Compile a subset of OCaml to Coq
coq-serapi       --          Serialization library and protocol for machine interaction with the Coq proof assistant
coq-shell        --          Simplified OPAM shell for Coq
coqide           --          IDE of the Coq formal proof management system
farith           --          Floating point numbers library extracted from the Flocq Coq Library
lambdapi         --          Proof assistant for the λΠ-calculus modulo rewriting
lem              --          Lem is a tool for lightweight executable mathematics
ott              --          A tool for writing definitions of programming languages and calculi
sail_coq_backend --          Sail to Coq translation
sibylfs-lem      --          SibylFS fork of Lightweight Executable Mathematics for large-scale semantics
space-search     --          SpaceSearch is a library that turns Coq into a solver-aided host language. Many
why3-coq         --          Why3 environment for deductive program verification
zenon            --          An Extensible Automated Theorem Prover Producing Checkable Proofs

but it doesn’t show me the version of coq available. I want to know why this fails but what is available

(iit_synthesis) brando9/afs/cs.stanford.edu/u/brando9/software_foundations_solution/book $ opam pin add -y coq 8.14pl6
[ERROR] Package coq has no known version 8.14pl6 in the repositories

opam show coq
should work.

1 Like

how do I see which compiler does it need?

When you do opam show coq you get a bunch of versions at the top of the output. You can then show one of those versions, viz.

$ opam show coq.8.16.1

<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><><><>
name         coq
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  8.12.1  8.12.2  8.13.0  8.13.1  8.13.2  8.14.0  8.14.1  8.15.0  8.15.1  8.15.2  8.16.0  8.16.1

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><><><>
version      8.16.1
repository   default
url.src      "https://github.com/coq/coq/archive/refs/tags/V8.16.1.tar.gz"
url.checksum "sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b"
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.09.0"}
             "ocamlfind" {>= "1.8.1"}
             "dune" {>= "2.5.1"}
             "conf-findutils" {build}
             "zarith" {>= "1.11"}
depopts      "coq-native"
conflicts    "base-nnp" "ocaml-option-nnpchecker"
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.

and if you look at the “depends” line, you’ll what compiler-version that version of Coq needs. But typically, opam will resolve all that for you automatically. Also, since you can only install within a switch, you should already have a compiler installed, right? So opam will choose a version of coq that is compatible with your installed-in-switch compiler, not the other way around.

2 Likes