# 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 4 Virtual package relying on a GMP lib system installation
coq 8.14.1 Formal proof management system
dune 3.7.0 Fast, portable, and opinionated build system
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "The CertiCoq Team"
homepage: "https://certicoq.org/"
dev-repo: "git+https://github.com/CertiCoq/certicoq"
bug-reports: "https://github.com/CertiCoq/certicoq/issues"
authors: ["Andrew Appel"
"Yannick Forster"
"Anvay Grover"
"Joomy Korkut"
"John Li"
"Zoe Paraskevopoulou"
"Matthieu Sozeau"
"Matthew Weaver"
"Abhishek Anand"
"Greg Morrisett"
"Randy Pollack"
"Olivier Savary Belanger"
]
license: "MIT"
build: [
[make "all"]
[make "plugins"]
[make "bootstrap"]
]
install: [
[make "install"]
]
depends: [
"ocaml"
"coq" {>= "8.14" & < "8.15~"}
"coq-compcert" {= "3.11"}
"coq-equations" {= "1.3+8.14"}
"coq-metacoq-erasure" {>= "1.1.1+8.14" }
"coq-ext-lib" {>= "0.11.5"}
]
synopsis: "A Verified Compiler for Gallina, Written in Gallina "
url {
src: "https://github.com/CertiCoq/certicoq/archive/refs/tags/v0.9-beta.tar.gz"
checksum: "sha512=dd5269d4666cdf7410e828472584ca59bf62729c9ac9ad47fb654da5723d7d16e5b27325aa89086f880c13890a62701af40f8719889dc7be2e522aba413b14e1"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-certicoq.0.9~beta+8.14 coq.8.14.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-certicoq.0.9~beta+8.14 coq.8.14.1# 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 4 Virtual package relying on a GMP lib system installation coq 8.14.1 Formal proof management system dune 3.7.0 Fast, portable, and opinionated build system ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers The following actions will be performed: - install coq-equations 1.3+8.14 - install menhirLib 20220210 - install conf-g++ 1.0 - install menhirSdk 20220210 - install coq-menhirlib 20220210 - install stdlib-shims 0.3.0 - install coq-ext-lib 0.11.7 - install coq-flocq 4.1.0 - install menhir 20220210 - install coq-metacoq-template 1.1.1+8.14 - install coq-compcert 3.11 - install coq-metacoq-pcuic 1.1.1+8.14 - install coq-metacoq-safechecker 1.1.1+8.14 - install coq-metacoq-erasure 1.1.1+8.14 ===== 14 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-ext-lib.0.11.7] downloaded from https://github.com/coq-community/coq-ext-lib/archive/v0.11.7.tar.gz [coq-compcert.3.11] downloaded from https://github.com/AbsInt/CompCert/archive/v3.11.tar.gz [coq-equations.1.3+8.14] downloaded from https://github.com/mattam82/Coq-Equations/archive/refs/tags/v1.3-8.14.tar.gz [coq-flocq.4.1.0] downloaded from https://flocq.gitlabpages.inria.fr/releases/flocq-4.1.0.tar.gz [coq-menhirlib.20220210] downloaded from https://gitlab.inria.fr/fpottier/menhir/-/archive/20220210/archive.tar.gz [coq-metacoq-erasure.1.1.1+8.14] downloaded from https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.14.tar.gz [coq-metacoq-pcuic.1.1.1+8.14] found in cache [coq-metacoq-safechecker.1.1.1+8.14] found in cache [coq-metacoq-template.1.1.1+8.14] found in cache [menhir.20220210] found in cache [menhirLib.20220210] found in cache [menhirSdk.20220210] found in cache [stdlib-shims.0.3.0] downloaded from cache at https://opam.ocaml.org/cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed conf-g++.1.0 -> installed coq-ext-lib.0.11.7 -> installed coq-equations.1.3+8.14 -> installed coq-menhirlib.20220210 -> installed menhirLib.20220210 -> installed menhirSdk.20220210 -> installed stdlib-shims.0.3.0 -> installed menhir.20220210 -> installed coq-flocq.4.1.0 -> installed coq-metacoq-template.1.1.1+8.14 -> installed coq-compcert.3.11 -> installed coq-metacoq-pcuic.1.1.1+8.14
trueNo files were installed.
true