~$ opam install coq-metacoq The following actions will be performed: - install coq-metacoq-template 1.0~beta2+8.13 [required by coq-metacoq] - install coq-metacoq-translations 1.0~beta2+8.13 [required by coq-metacoq] - install coq-metacoq-pcuic 1.0~beta2+8.13 [required by coq-metacoq] - install coq-metacoq-safechecker 1.0~beta2+8.13 [required by coq-metacoq] - install coq-metacoq-erasure 1.0~beta2+8.13 [required by coq-metacoq] - install coq-metacoq 1.0~beta2+8.13 ===== 6 to install ===== Do you want to continue? [Y/n] n ~$ opam list # Packages matching: installed # Name # Installed # Synopsis base v0.14.0 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-m4 1 Virtual package relying on m4 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.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 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 ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml project ocamlfind 1.8.1 A library manager for OCaml ocamlfind-secondary 1.8.1 ocamlfind support for ocaml-secondary-compiler 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 patch_coq-platform_.2021.02.1 file:///Users/msoegtrop/CoqPlatform/coq-platform-2021.02/opam 2 coq-released https://coq.inria.fr/opam/released 3 default https://opam.ocaml.org ~$