From 64d8345e4ede21260d24d413fee51d49357b96a5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 6 Jun 2020 00:31:19 +0900 Subject: [PATCH] update to last version --- INSTALL.md | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index d7f33ae1c7..7da6538df7 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,21 +1,24 @@ # Installing ## Requirements -- [The Coq Proof Assistant version ≥ 8.8](https://coq.inria.fr) -- [Mathematical Components version ≥ 1.8.0](https://github.com/math-comp/math-comp) -- [Bigenough version 1.0.0](https://github.com/math-comp/bigenough) -- [Finmap library version 1.2.0](https://github.com/math-comp/finmap) +- [The Coq Proof Assistant version ≥ 8.7](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 [opam 2](https://opam.ocaml.org/) 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`. +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. Detailed instructions for possible installations of Mathematical Components are located [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md). ## Short Instructions -- Custom (assuming Coq ≥ 8.8, Mathematical Components version ≥ 1.8.0, Bigenough version 1.0.0 and Finmap version 1.2.0 have been installed): - + Type `make` to use the provided `Makefile`. - Through opam: - + Type `opam install coq-mathcomp-analysis` + + 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 `make` to use the provided `Makefile`. ## From scratch instructions ### How to install as a package @@ -32,10 +35,18 @@ $ 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, +``` +$ opam install coq-mathcomp-analysis.0.3.0 +``` 4. Everytime you want to work in this same context, you need to type ``` $ export OPAMROOT=~/.opam_mathcomp_analysis @@ -53,6 +64,9 @@ $ 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) ## 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. + 1. Install Coq 8.9.1 ``` $ opam install coq.8.9.1