From 4177146f004539d684976678dae008d4f2223cb9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 10 Jun 2020 22:33:24 +0900 Subject: [PATCH 1/3] update INSTALL.md now that 1.11.0 has been released --- INSTALL.md | 36 +++++++++++++++++++++++------------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 7da6538df7..3c1c0be70c 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -5,19 +5,24 @@ - [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 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` +- or the repository https://coq.inria.fr/opam/extra-dev, if the requirements involve beta releases + (this has been the case with MathComp 1.11+beta1) -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): + + For the latest version (as of [2020-06-05]), type `opam install coq-mathcomp-analysis.0.3.0` + + For other versions, type `opam install coq-mathcomp-analysis.X.Y.Z` + (all the dependencies should be automatically installed, assuming `opam` has been properly configured + and `coq-released` repository is added---possibly `extra-dev` if necessary, see above) +- 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 @@ -54,18 +59,22 @@ $ 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.8.0. For more recent versions, update the +version numbers accordingly. 1. Install Coq 8.9.1 ``` @@ -95,7 +104,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 ``` From 4f39f26a3cd794521d91fc5e993d5ea22f4c5e9d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 11 Jun 2020 00:01:44 +0900 Subject: [PATCH 2/3] remove technical explanations about betas --- INSTALL.md | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 3c1c0be70c..64c961a6b9 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -5,28 +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 can be installed in a custom way or through +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` -- or the repository https://coq.inria.fr/opam/extra-dev, if the requirements involve beta releases - (this has been the case with MathComp 1.11+beta1) +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). ## Short Instructions - Through opam: - + For the latest version (as of [2020-06-05]), type `opam install coq-mathcomp-analysis.0.3.0` - + For other versions, type `opam install coq-mathcomp-analysis.X.Y.Z` - (all the dependencies should be automatically installed, assuming `opam` has been properly configured - and `coq-released` repository is added---possibly `extra-dev` if necessary, see above) + + 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, 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: ``` @@ -35,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.X.Y.Z ``` 4. Everytime you want to work in this same context, you need to type ``` From 5c11fdc9a513c40733d5bf8b11216c08d780a3d0 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 11 Jun 2020 05:04:14 +0200 Subject: [PATCH 3/3] Update INSTALL.md --- INSTALL.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 64c961a6b9..98e5958b80 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -18,7 +18,7 @@ Detailed instructions for possible installations of Mathematical Components are + 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, and Finmap version 1.5.0 +- 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`. @@ -45,7 +45,7 @@ $ opam install coq-mathcomp-analysis ``` To install a precise version, type, say ``` -$ opam install coq-mathcomp-analysis.X.Y.Z +$ opam install coq-mathcomp-analysis.0.3.1 ``` 4. Everytime you want to work in this same context, you need to type ``` @@ -68,7 +68,7 @@ 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 +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 @@ -77,16 +77,16 @@ $ 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 ```