~# opam repo --all
[WARNING] Running as root is not recommended
# Repository # Url                              # Switches(rank)
coq-released https://coq.inria.fr/opam/released <default>(1) Hott+metacoq(1) with-metacoq-test-2(1)
                                                with-metacoq-test(1) with-coq(1)
default      https://opam.ocaml.org             <default>(2) Hott+metacoq(2) with-metacoq-test-2(2)
                                                with-metacoq-test(2) with-coq(2)




~# opam switch set with-metacoq-test
[WARNING] Running as root is not recommended
# Run eval $(opam env) to update the current shell environment
~t# opam list
[WARNING] Running as root is not recommended
# Packages matching: installed
# Name                   # Installed    # Synopsis
base-bigarray            base
base-threads             base
base-unix                base
cairo2                   0.6.2          Binding to Cairo, a 2D Vector Graphics Library
conf-adwaita-icon-theme  1              Virtual package relying on adwaita-icon-theme
conf-cairo               1              Virtual package relying on a Cairo system installation
conf-findutils           1              Virtual package relying on findutils
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-pkg-config          2              Check if pkg-config is installed and create an opam switch local pkgconfig folde
coq                      8.13.2         Formal proof management system
coq-equations            1.2.4+8.13     A function definition package for Coq
coq-metacoq-pcuic        1.0~beta2+8.13 A type system equivalent to Coq's and its metatheory
coq-metacoq-template     1.0~beta2+8.13 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.0~beta2+8.13 Translations built on top of MetaCoq
coqide                   8.13.2         IDE of the Coq formal proof management system
csexp                    1.5.1          Parsing and printing of S-expressions in Canonical form
dune                     2.8.5          Fast, portable, and opinionated build system
dune-configurator        2.8.5          Helper library for gathering system configuration
lablgtk3                 3.1.1          OCaml interface to GTK+3
lablgtk3-sourceview3     3.1.1          OCaml interface to GTK+ gtksourceview library
num                      1.4            The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                    4.12.0         The OCaml compiler (virtual package)
ocaml-base-compiler      4.12.0         Official release 4.12.0
ocaml-config             2              OCaml Switch Configuration
ocaml-options-vanilla    1              Ensure that OCaml is compiled with no special options enabled
ocamlfind                1.9.1          A library manager for OCaml
result                   1.5            Compatibility Result module
zarith                   1.12           Implements arithmetic and logical operations over arbitrary-precision integers



~# opam switch set with-metacoq-test-2
[WARNING] Running as root is not recommended
# Run eval $(opam env) to update the current shell environment
~# opam list
[WARNING] Running as root is not recommended
# Packages matching: installed
# Name                   # Installed    # Synopsis
base-bigarray            base
base-threads             base
base-unix                base
cairo2                   0.6.2          Binding to Cairo, a 2D Vector Graphics Library
conf-adwaita-icon-theme  1              Virtual package relying on adwaita-icon-theme
conf-cairo               1              Virtual package relying on a Cairo system installation
conf-findutils           1              Virtual package relying on findutils
conf-gtk3                18             Virtual package relying on GTK+ 3
conf-gtksourceview3      0+2            Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config          2              Check if pkg-config is installed and create an opam switch local pkgconfig folde
conf-python-3            1.0.0          Virtual package relying on Python-3 installation
conf-time                1              Virtual package relying on the "time" command
conf-which               1              Virtual package relying on which
coq                      8.12.2         Formal proof management system
coq-bignums              8.12.0         Bignums, the Coq library of arbitrary large numbers
coq-equations            1.2.3+8.12     A function definition package for Coq
coq-metacoq              1.0~beta1+8.12 A meta-programming framework for Coq
coq-metacoq-checker      1.0~beta1+8.12 Specification of Coq's type theory and reference checker implementation
coq-metacoq-erasure      1.0~beta1+8.12 Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic        1.0~beta1+8.12 A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker  1.0~beta1+8.12 Implementation and verification of safe conversion and typechecking algorithms f
coq-metacoq-template     1.0~beta1+8.12 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.0~beta1+8.12 Translations built on top of MetaCoq
coqide                   8.12.2         IDE of the Coq formal proof management system
csexp                    1.5.1          Parsing and printing of S-expressions in Canonical form
dune                     2.8.5          Fast, portable, and opinionated build system
dune-configurator        2.8.5          Helper library for gathering system configuration
lablgtk3                 3.1.1          OCaml interface to GTK+3
lablgtk3-sourceview3     3.1.1          OCaml interface to GTK+ gtksourceview library
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-config             1              OCaml Switch Configuration
ocamlfind                1.9.1          A library manager for OCaml
result                   1.5            Compatibility Result module




~# opam switch set Hott+metacoq
[WARNING] Running as root is not recommended
# Run eval $(opam env) to update the current shell environment
~# opam list
[WARNING] Running as root is not recommended
# Packages matching: installed
# Name                   # Installed    # Synopsis
base-bigarray            base
base-threads             base
base-unix                base
cairo2                   0.6.2          Binding to Cairo, a 2D Vector Graphics Library
conf-adwaita-icon-theme  1              Virtual package relying on adwaita-icon-theme
conf-autoconf            0.1            Virtual package relying on autoconf installation
conf-cairo               1              Virtual package relying on a Cairo system installation
conf-findutils           1              Virtual package relying on findutils
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-pkg-config          2              Check if pkg-config is installed and create an opam switch local pkgconfig folde
conf-python-3            1.0.0          Virtual package relying on Python-3 installation
conf-time                1              Virtual package relying on the "time" command
conf-which               1              Virtual package relying on which
coq                      8.11.2         Formal proof management system
coq-equations            1.2.4+8.11     A function definition package for Coq
coq-hott                 8.11           The Homotopy Type Theory library
coq-metacoq              1.0~beta1+8.11 A meta-programming framework for Coq
coq-metacoq-checker      1.0~beta1+8.11 Specification of Coq's type theory and reference checker implementation
coq-metacoq-erasure      1.0~beta1+8.11 Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic        1.0~beta1+8.11 A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker  1.0~beta1+8.11 Implementation and verification of safe conversion and typechecking algorithms f
coq-metacoq-template     1.0~beta1+8.11 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.0~beta1+8.11 Translations built on top of MetaCoq
coqide                   8.11.2         IDE of the Coq formal proof management system
csexp                    1.5.1          Parsing and printing of S-expressions in Canonical form
dune                     2.8.5          Fast, portable, and opinionated build system
dune-configurator        2.8.5          Helper library for gathering system configuration
lablgtk3                 3.1.1          OCaml interface to GTK+3
lablgtk3-sourceview3     3.1.1          OCaml interface to GTK+ gtksourceview library
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-config             1              OCaml Switch Configuration
ocamlfind                1.9.1          A library manager for OCaml
result                   1.5            Compatibility Result module
zarith                   1.12           Implements arithmetic and logical operations over arbitrary-precision integers