Skip to content

Latest commit

 

History

History
116 lines (99 loc) · 3.75 KB

INSTALL.md

File metadata and controls

116 lines (99 loc) · 3.75 KB

Installing

Requirements

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.

Short Instructions

  • 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

From scratch instructions

How to install as a package

  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.15.0
  1. Everytime you want to work in this same context, you need to type
$ export OPAMROOT=~/.opam_mathcomp_analysis 
$ eval `opam config env`

How to edit and test the source code

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

Break-down of phase 3 of the installation procedure step by step

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

How to clean your computer

  • 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