~$ 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 ~$