Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 31 additions & 26 deletions INSTALL.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,23 +5,27 @@
- [Mathematical Components version ≥ 1.11.0](https://github.com/math-comp/math-comp)
- [Finmap library version ≥ 1.5.0](https://github.com/math-comp/finmap)

These requirements can be installed through [opam](https://opam.ocaml.org/) (the recommended way) using
- the repository https://coq.inria.fr/opam/extra-dev, if the requirements involve beta releases (as of [2020-06-05] this is the case for MathComp 1.11.0)
- or, for other versions, the repository https://coq.inria.fr/opam/released, which you can add by typing `opam repo add coq-released https://coq.inria.fr/opam/released`
or can be installed in a custom way.
These requirements can be installed in a custom way, or through
[opam](https://opam.ocaml.org/) (the recommended way) using
the repository https://coq.inria.fr/opam/released, which you can add by typing
`opam repo add coq-released https://coq.inria.fr/opam/released`.

Detailed instructions for possible installations of Mathematical Components are located [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
Detailed instructions for possible installations of Mathematical Components are located
[here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).

## Short Instructions
- Through opam:
+ For the latest version (as of [2020-06-05]), type `opam install coq-mathcomp-analysis.0.3.0` (assuming the `extra-dev` repository has been added)
+ For other versions, type `opam install coq-mathcomp-analysis`
(all the dependencies should be automatically installed, assuming `opam` has been properly configured and `coq-released` repository is added)
- Custom (assuming Coq ≥ 8.7, Mathematical Components version ≥ 1.11, and Finmap version 1.5.0 have been installed):
+ 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 (assuming Coq ≥ 8.7, Mathematical Components version ≥ 1.11.0, and Finmap version 1.5.0
have been installed):
+ Type `make` to use the provided `Makefile`.

## From scratch instructions

### How to install as a package

1. Install opam
- any linux system:
```
Expand All @@ -30,22 +34,18 @@ $ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/instal

2. Configure opam
```
$ export OPAMROOT=~/.opam_mathcomp_analysis
$ 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 coq-released https://coq.inria.fr/opam/released
```
To access beta releases:
```
$ opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
```
3. Install our package (and all its dependencies)
```
$ opam install coq-mathcomp-analysis
```
To install a precise version, type, say 0.3.0,
To install a precise version, type, say
```
$ opam install coq-mathcomp-analysis.0.3.0
$ opam install coq-mathcomp-analysis.0.3.1
```
4. Everytime you want to work in this same context, you need to type
```
Expand All @@ -54,35 +54,39 @@ $ 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

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](https://github.com/ProofGeneral/PG)
You may then browse the files using `coqide` (you might want to `opam install coqide`) or
using [proof general for emacs](https://github.com/ProofGeneral/PG)

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

With the example of Coq 8.9.1 and MathComp 1.8.0. For more recent versions, update the version numbers accordingly.
With the example of Coq 8.9.1 and MathComp 1.11.0. For more recent versions, update the
version numbers accordingly.

1. Install Coq 8.9.1
```
$ opam install coq.8.9.1
```
2. Install Mathematical Components development version
```
$ opam install coq-mathcomp-ssreflect.1.8.0
$ opam install coq-mathcomp-fingroup.1.8.0
$ opam install coq-mathcomp-algebra.1.8.0
$ opam install coq-mathcomp-solvable.1.8.0
$ opam install coq-mathcomp-field.1.8.0
$ opam install coq-mathcomp-ssreflect.1.11.0
$ opam install coq-mathcomp-fingroup.1.11.0
$ opam install coq-mathcomp-algebra.1.11.0
$ opam install coq-mathcomp-solvable.1.11.0
$ opam install coq-mathcomp-field.1.11.0
$ opam install coq-mathcomp-bigenough.1.0.0
```
3. Install Finite maps library
```
$ opam install coq-mathcomp-finmap.1.2.0
$ opam install coq-mathcomp-finmap.1.5.0
```
4. Download and compile `coq-mathcomp-analysis` without installing
```
Expand All @@ -95,7 +99,8 @@ $ make
```
$ 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:
- 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
```