~$ opam install coq-metacoq
The following actions will be performed:
- remove coq-hott 8.13 [conflicts with coq]
- install conf-time 1 [required by coq-metacoq-translations]
- install conf-python-3 1.0.0 [required by coq-metacoq-translations]
- downgrade coq 8.13.2 to 8.12.2 [required by coq-metacoq]
- install coq-metacoq-template 1.0~beta1+8.12 [required by coq-metacoq]
- upgrade coq-elpi 1.8.1 to 1.8.3~8.12 [uses coq]
- recompile coq-menhirlib 20200624 [uses coq]
- recompile coq-mathcomp-ssreflect 1.12.0 [uses coq]
- recompile coq-flocq 3.3.1 [uses coq]
- recompile coq-ext-lib 0.11.3 [uses coq]
- downgrade coqide 8.13.2 to 8.12.2 [uses coq]
- downgrade coq-unicoq 1.5+8.13 to 1.5+8.12 [uses coq]
- downgrade coq-equations 1.2.3+8.13 to 1.2.3+8.12 [uses coq]
- downgrade coq-bignums 8.13.0 to 8.12.0 [uses coq]
- downgrade coq-aac-tactics 8.13.0 to 8.12.0 [uses coq]
- recompile coq-hierarchy-builder 1.0.0 [uses coq-elpi]
- recompile coq-mathcomp-fingroup 1.12.0 [uses coq-mathcomp-ssreflect]
- recompile coq-mathcomp-bigenough 1.0.0 [uses coq-mathcomp-ssreflect]
- recompile coq-coquelicot 3.1.0 [uses coq]
- recompile coq-gappa 1.4.6 [uses coq]
- recompile coq-compcert 3.8 [uses coq]
- recompile coq-simple-io 1.5.0 [uses coq]
- downgrade coq-mtac2 1.4+8.13 to 1.3+8.12 [uses coq]
- install coq-metacoq-checker 1.0~beta1+8.12 [required by coq-metacoq]
- recompile coq-mathcomp-algebra 1.12.0 [uses coq-mathcomp-fingroup]
- recompile coq-mathcomp-finmap 1.5.1 [uses coq]
- recompile coq-interval 4.1.1 [uses coq]
- recompile coq-vst 2.7.1 [uses coq]
- downgrade coq-quickchick 1.5.0 to 1.4.0 [uses coq]
- install coq-metacoq-translations 1.0~beta1+8.12 [required by coq-metacoq]
- install coq-metacoq-pcuic 1.0~beta1+8.12 [required by coq-metacoq]
- recompile coq-mathcomp-solvable 1.12.0 [uses coq-mathcomp-algebra]
- install coq-metacoq-safechecker 1.0~beta1+8.12 [required by coq-metacoq]
- recompile coq-mathcomp-field 1.12.0 [uses coq-mathcomp-solvable]
- install coq-metacoq-erasure 1.0~beta1+8.12 [required by coq-metacoq]
- recompile coq-mathcomp-real-closed 1.1.2 [uses coq]
- recompile coq-mathcomp-character 1.12.0 [uses coq-mathcomp-field]
- install coq-metacoq 1.0~beta1+8.12
===== 9 to install | 19 to recompile | 1 to upgrade | 8 to downgrade | 1 to remove =====
Do you want to continue? [Y/n] n
~$ opam list
# Packages matching: installed
# Name # Installed # Synopsis
base v0.14.1 Full standard library replacement for OCaml
base-bigarray base
base-threads base
base-unix base
cairo2 0.6.2 Binding to Cairo, a 2D Vector Graphics Library
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-adwaita-icon-theme 1 Virtual package relying on adwaita-icon-theme
conf-autoconf 0.1 Virtual package relying on autoconf installation
conf-automake 1 Virtual package relying on GNU automake
conf-bison 2 Virtual package relying on GNU bison
conf-boost 1 Virtual package relying on boost
conf-cairo 1 Virtual package relying on a Cairo system installation
conf-findutils 1 Virtual package relying on findutils
conf-flex 2 Virtual package relying on GNU flex
conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++)
conf-gmp 3 Virtual package relying on a GMP lib system installation
conf-gtk3 18 Virtual package relying on GTK+ 3
conf-gtksourceview3 0+2 Virtual package relying on a GtkSourceView-3 system installation
conf-mpfr 2 Virtual package relying on library MPFR installation
conf-perl 1 Virtual package relying on perl
conf-pkg-config 2 Check if pkg-config is installed and create an opam switch local pkgconfig folder
conf-which 1 Virtual package relying on which
coq 8.13.2 Formal proof management system
coq-aac-tactics 8.13.0 Coq plugin providing tactics for rewriting universally quantified equations, modul
coq-bignums 8.13.0 Bignums, the Coq library of arbitrary large numbers
coq-compcert 3.8 The CompCert C compiler (64 bit)
coq-coquelicot 3.1.0 A Coq formalization of real analysis compatible with the standard library
coq-elpi 1.8.1 Elpi extension language for Coq
coq-equations 1.2.3+8.13 A function definition package for Coq
coq-ext-lib 0.11.3 A library of Coq definitions, theorems, and tactics
coq-flocq 3.3.1 A formalization of floating-point arithmetic for the Coq system
coq-gappa 1.4.6 A Coq tactic for discharging goals about floating-point arithmetic and round-off e
coq-hierarchy-builder 1.0.0 High level commands to declare and evolve a hierarchy based on packed classes
coq-hott 8.13 The Homotopy Type Theory library
coq-interval 4.1.1 A Coq tactic for proving bounds on real-valued expressions automatically
coq-mathcomp-algebra 1.12.0 Mathematical Components Library on Algebra
coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning
coq-mathcomp-character 1.12.0 Mathematical Components Library on character theory
coq-mathcomp-field 1.12.0 Mathematical Components Library on Fields
coq-mathcomp-fingroup 1.12.0 Mathematical Components Library on finite groups
coq-mathcomp-finmap 1.5.1 Finite sets, finite maps, finitely supported functions
coq-mathcomp-real-closed 1.1.2 Mathematical Components Library on real closed fields
coq-mathcomp-solvable 1.12.0 Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect 1.12.0 Small Scale Reflection
coq-menhirlib 20200624 A support library for verified Coq parsers produced by Menhir
coq-mtac2 1.4+8.13 Mtac2: Typed Tactics for Coq
coq-quickchick 1.5.0 Randomized Property-Based Testing Plugin for Coq
coq-simple-io 1.5.0 IO monad for Coq
coq-unicoq 1.5+8.13 An enhanced unification algorithm for Coq
coq-vst 2.7.1 Verified Software Toolchain
coqide 8.13.2 IDE of the Coq formal proof management system
cppo 1.6.7 Code preprocessor like cpp for OCaml
csexp 1.5.1 Parsing and printing of S-expressions in Canonical form
depext transition opam-depext transition package
dune 2.8.5 Fast, portable, and opinionated build system
dune-configurator 2.8.5 Helper library for gathering system configuration
elpi 1.12.0 ELPI - Embeddable λProlog Interpreter
gappa 1.3.5 Tool intended for formally proving properties on numerical programs dealing with f
lablgtk3 3.1.1 OCaml interface to GTK+3
lablgtk3-sourceview3 3.1.1 OCaml interface to GTK+ gtksourceview library
menhir 20200624 An LR(1) parser generator
menhirLib 20200624 Runtime support library for parsers generated by Menhir
menhirSdk 20200624 Compile-time library for auxiliary tools related to Menhir
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.10.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.0 Official release 4.10.0
ocaml-compiler-libs v0.12.3 OCaml compiler libraries repackaged
ocaml-config 1 OCaml Switch Configuration
ocaml-migrate-parsetree 1.8.0 Convert OCaml parsetrees between different versions
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml project
ocamlfind 1.9.1 A library manager for OCaml
opam-depext 1.1.5 install OS distribution packages
ppx_derivers 1.2.1 Shared [@@deriving] plugin registry
ppx_deriving 5.1 Type-driven code generation for OCaml
ppxlib 0.14.0 Base library and tools for ppx rewriters
re 1.9.0 RE is a regular expression library for OCaml
result 1.5 Compatibility Result module
seq base Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converters
stdio v0.14.0 Standard IO library for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
~$ opam repo
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
<><> Repository configuration for switch __coq-platform.2021.02.1 <><><><><><><>
1 __coq-platform.2021.02.1.patch_coq-released file:///Users/msoegtrop/CoqPlatform/coq-platform-test/opam/opam-coq-archive/released
2 __coq-platform.2021.02.1.patch_ocaml file:///Users/msoegtrop/CoqPlatform/coq-platform-test/opam/opam-repository
3 coq-released https://coq.inria.fr/opam/released
4 default https://opam.ocaml.org
~$