Skip to content

Commit

Permalink
update of install instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Dec 12, 2020
1 parent 00e6783 commit 06a8c38
Showing 1 changed file with 17 additions and 10 deletions.
27 changes: 17 additions & 10 deletions INSTALL.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
# Installing

## Requirements
- [The Coq Proof Assistant version ≥ 8.10](https://coq.inria.fr)
- [Mathematical Components version ≥ 1.11.0](https://github.com/math-comp/math-comp)

- [The Coq Proof Assistant version ≥ 8.11](https://coq.inria.fr)
- [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 in a custom way, or through
Expand All @@ -14,13 +15,14 @@ Detailed instructions for possible installations of Mathematical Components are
[here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).

## 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 (assuming Coq ≥ 8.10, Mathematical Components version 1.11.0, and Finmap version ≥ 1.5.0
have been installed):
+ Type `make` to use the provided `Makefile`.
- Custom (assuming Coq ≥ 8.11, Mathematical Components version = 1.11.0, Finmap version ≥ 1.5.0,
and Hierarchy Builder ≥ 0.10.0 have been installed):
+ type `make` to use the provided `Makefile`

## From scratch instructions

Expand All @@ -45,7 +47,7 @@ $ opam install coq-mathcomp-analysis
```
To install a precise version, type, say
```
$ opam install coq-mathcomp-analysis.0.3.3
$ opam install coq-mathcomp-analysis.0.3.4
```
4. Everytime you want to work in this same context, you need to type
```
Expand Down Expand Up @@ -75,26 +77,31 @@ version numbers accordingly.
```
$ opam install coq.8.12.0
```
2. Install Mathematical Components development version
2. Install the Mathematical Components
```
$ 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
3. Install the Finite maps library
```
$ opam install coq-mathcomp-finmap.1.5.0
```
4. Download and compile `coq-mathcomp-analysis` without installing
4. Install the Hierarchy Builder
```
$ opam install coq-hierarchy-builder.0.10.0
```
5. 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
Expand Down

0 comments on commit 06a8c38

Please sign in to comment.