Merge pull request #165 from ejgallego/readme_pass

[doc] Attempt to tweak README based on the discussion.

2 files changed, 111 insertions, 75 deletions

diff --git a/INSTALL.md b/INSTALL.md
new file mode 100644
index 0000000..9752f0f
--- /dev/null
+++ b/INSTALL.md
@@ -0,0 +1,81 @@
+# Layout and compilation of the library
+
+The library is divided into packages which group together related
+files. Each package defines a distribution and compilation unit.
+
+Packages can be compiled using the traditional `make` utility or
+the more recent `OPAM` one. The released and current dev version are
+also available as opam packages.
+
+## Compilation and installation of released and current dev version with OPAM
+If you just installed opam you may have to do the following. You may also want
+to read opam user manual first https://opam.ocaml.org/doc/Usage.html
+```
+opam init
+eval `opam config env`
+```
+Once your opam envionement is configure you can install any math-comp package via
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam pin add -n coq -k version 8.7.0
+opam install coq -j3
+opam install coq-mathcomp-ssreflect.1.6.4 -j3
+```
+Replace `ssreflect` here by the package you want, dependencies will be
+installed automatically. You can replace `1.6.4` by `dev` to get the last
+development version. We recommand to pin a particular version of Coq
+(here `8.7.0`).
+
+## Compilation and installation with make
+
+The instructions assume you are in the `mathcomp` directory and that
+you have a supported version of Coq.
+The list of Coq versions that are known to work can be obtained with:
+```
+ls ssreflect/plugin/
+```
+Alternatively, if you are familiar with the `OPAM` slang:
+```
+grep depends: ssreflect/opam
+```
+
+If `coqc` is in your `PATH`, then you are good to go.  Alternatively you
+can export the `COQBIN` variable to tell make where the `coqc` binary is:
+```
+export COQBIN=/home/gares/COQ/coq/bin/
+```
+
+To compile the entire library just type `make`. If you have parallel
+hardware then `make -j 3` is probably a faster option. 
+
+The files can be edited using CoqIDE or Proof General, or any
+other editor that understands the `_CoqProject` file, with no
+further configuration from the `mathcomp` directory.
+```
+coqide ssreflect/div.v
+```
+Note that you may need to enable `_CoqProject` processing in your
+editor (e.g. the default for CoqIDE is to ignore it).
+
+To install the compiled library, just execute `make install`.
+
+## Compilation and installation of a custom version using OPAM
+
+The instructions assume you are in the `mathcomp` directory
+and that you have `OPAM` installed and configured with the
+standard Coq repositories.
+
+For each package, pin the `opam` file:
+```
+opam pin -n add ssreflect
+```
+This can be achieved in one go as follows:
+```
+for P in */opam; do opam pin -n add ${P%%/opam}; done
+```
+
+Then you can use `opam install` to compile and install any package.
+For example:
+```
+opam install coq.8.7.0 coq-mathcomp-ssreflect
+```
diff --git a/README.md b/README.md
index 9bb2645..b45ce9d 100644
--- a/README.md
+++ b/README.md
@@ -2,90 +2,45 @@
 
 # The Mathematical Components repository
 
-This repository holds the Mathematical Components Library for the Coq system:
-an extensive body of mathematics formalized in the Coq/SSReflect language.
+The Mathematical Components Library is an extensive body of
+mathematics formalized in the Coq/SSReflect language.
 
-It also contains the proof of the Odd Order Theorem, that builds on top
-of the Mathematical Components Library.
+This repository also contains a
+[mechanization](https://hal.archives-ouvertes.fr/hal-00816699/) of the
+[Odd Order
+Theorem](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem),
+which utilizes the library extensively.
 
-# Layout and compilation of the library
+## Installation
 
-The library is divided into packages which group together related
-files. Each package defines a distribution and compilation unit.
+If you already have OPAM installed:
 
-Packages can be compiled using the traditional `make` utility or
-the more recent `OPAM` one. The released and current dev version are
-also available as opam packages.
-
-## Compilation and installation of released and current dev version with OPAM
-If you just installed opam you may have to do the following. You may also want
-to read opam user manual first https://opam.ocaml.org/doc/Usage.html
-```
-opam init
-eval `opam config env`
-```
-Once your opam envionement is configure you can install any math-comp package via
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam pin add -n coq -k version 8.7.0
-opam install coq -j3
-opam install coq-mathcomp-ssreflect.1.6.4 -j3
-```
-Replace `ssreflect` here by the package you want, dependencies will be
-installed automatically. You can replace `1.6.4` by `dev` to get the last
-development version. We recommand to pin a particular version of Coq
-(here `8.7.0`).
-
-## Compilation and installation with make
-
-The instructions assume you are in the `mathcomp` directory and that
-you have a supported version of Coq.
-The list of Coq versions that are known to work can be obtained with:
-```
-ls ssreflect/plugin/
-```
-Alternatively, if you are familiar with the `OPAM` slang:
-```
-grep depends: ssreflect/opam
-```
-
-If `coqc` is in your `PATH`, then you are good to go.  Alternatively you
-can export the `COQBIN` variable to tell make where the `coqc` binary is:
+opam install coq-mathcomp-ssreflect
 ```
-export COQBIN=/home/gares/COQ/coq/bin/
-```
-
-To compile the entire library just type `make`. If you have parallel
-hardware then `make -j 3` is probably a faster option. 
 
-The files can be edited using CoqIDE or Proof General, or any
-other editor that understands the `_CoqProject` file, with no
-further configuration from the `mathcomp` directory.
-```
-coqide ssreflect/div.v
-```
-Note that you may need to enable `_CoqProject` processing in your
-editor (e.g. the default for CoqIDE is to ignore it).
+Additional packages go by the name of `coq-mathcomp-algebra`,
+`coq-mathcomp-field`, etc... See [INSTALL](INSTALL.md) for detailed
+installation instructions in other scenarios.
 
-To install the compiled library, just execute `make install`.
+## How to get help
 
-## Compilation and installation of a custom version using OPAM
+- The [ssreflect mailing
+  list](https://sympa.inria.fr/sympa/info/ssreflect) is the primary
+  venue for help and questions about the library.
+- The [MathComp wiki](https://github.com/math-comp/math-comp/wiki)
+  contains many useful information, including including a list of
+  [tutorials](https://github.com/math-comp/math-comp/wiki/tutorials)
+- The [Mathematical Components Book](https://math-comp.github.io/mcb/)
+  provides a comprehensive introduction to the library.
+- Experienced users hang around at
+  [StackOverflow](https://stackoverflow.com/questions/tagged/ssreflect)
+  listening to the `ssreflect` and `coq` tags.
 
-The instructions assume you are in the `mathcomp` directory
-and that you have `OPAM` installed and configured with the
-standard Coq repositories.
+## Publications and Tools using MathComp
 
-For each package, pin the `opam` file:
-```
-opam pin -n add ssreflect
-```
-This can be achieved in one go as follows:
-```
-for P in */opam; do opam pin -n add ${P%%/opam}; done
-```
-
-Then you can use `opam install` to compile and install any package.
-For example:
-```
-opam install coq.8.7.0 coq-mathcomp-ssreflect
-```
+[Papers](https://github.com/math-comp/math-comp/wiki/Publications) and
+[Software](https://github.com/math-comp/math-comp/wiki/Software) built
+using the Mathematical Components library can be found at the
+[wiki](https://github.com/math-comp/math-comp/wiki)