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