• The Rocq Prover version ≥ 9.0
• Mathematical Components version ≥ 2.5.0
• Finmap library version ≥ 2.1.0
• Hierarchy builder version ≥ 1.8.0
• bigenough ≥ 1.0.0

These requirements can be installed in a custom way, or through opam (the recommended way) using the repository https://rocq-prover.org/opam/released, which you can add by typing opam repo add rocq-released https://rocq-prover.org/opam/released.

Detailed instructions for possible installations of Mathematical Components are located here.

• Through opam:
  • type opam install coq-mathcomp-analysis.X.Y.Z where X.Y.Z is the version number (all the dependencies should be automatically installed, assuming opam has been properly configured and coq-released repository is added)
• Custom:
  • first, install the required dependencies, for example with opam type opam install --deps-only coq-mathcomp-analysis.X.Y.Z
  • assuming the requirements are met, type make to use the provided Makefile

1. Install opam

• any linux system:

$ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

1. Configure opam

$ export OPAMROOT=~/.opam_mathcomp_analysis # opam configuration, metadata, logs, temporary directories and caches
$ opam init -j4 # adapt to the number of cores you have
$ eval `opam config env`
$ opam repo add rocq-released https://rocq-prover.org/opam/released

1. Install our package (and all its dependencies)

$ opam install coq-mathcomp-analysis

To install a precise version, type, say

$ opam install coq-mathcomp-analysis.1.16.0

1. Everytime you want to work in this same context, you need to type

$ export OPAMROOT=~/.opam_mathcomp_analysis 
$ eval `opam config env`

If you would rather edit and test the files than intalling them, we suggest that you replace opam install coq-mathcomp-analysis command with the following

$ opam install coq-mathcomp-analysis --deps-only
$ git clone https://github.com/math-comp/analysis
$ cd analysis
$ make

You may then browse the files using coqide (you might want to opam install coqide) or using proof general for emacs

With the example of Coq 9.1.1 and MathComp 2.5.0. For other versions, update the version numbers accordingly.

1. Install Rocq 9.1.1

$ opam install rocq-core.9.1.1

1. Install the Mathematical Components

$ opam install rocq-mathcomp-ssreflect.2.5.0
$ opam install rocq-mathcomp-fingroup.2.5.0
$ opam install rocq-mathcomp-algebra.2.5.0
$ opam install rocq-mathcomp-solvable.2.5.0
$ opam install rocq-mathcomp-field.2.5.0

1. Install the Finite maps library

$ opam install rocq-mathcomp-finmap.2.2.0

1. Install the Hierarchy Builder

$ opam install rocq-hierarchy-builder.1.10.2

1. Download and compile coq-mathcomp-analysis without installing

$ git clone https://github.com/math-comp/analysis
$ cd analysis
$ make

• If you installed the package coq-mathcomp-analysis and wish to get rid of it, just type

$ opam remove coq-mathcomp-analysis

• However if you wish to clean the entire installation (including coq and mathcomp dependencies) you should remove the opam root we created for this purpose:

$ rm -rf ~/.opam_mathcomp_analysis