First stab at INSTALL

2 files changed, 78 insertions, 50 deletions

diff --git a/etc/INSTALL b/etc/INSTALL
deleted file mode 100644
index c468b6f..0000000
--- a/etc/INSTALL
+++ /dev/null
@@ -1,50 +0,0 @@
-INSTALLATION PROCEDURE FOR THE MATHEMATICAL COMPONENTS LIBRARY
---------------------------------------------------------------
-
-LINUX AND MAC
-=============
-
-0. Install opam.  Instructions at
-
-     http://opam.ocaml.org/doc/Install.html
-
-1. Be sure to have the Coq stable repository added to opam by typing
-
-     opam repo list
-
-   If it is not the case, type
-
-     opam repo add coq-stable https://github.com/coq/repo-stable.git
-
-2. To find all Mathematical Components libraries type
-
-     opam search coq:mathcomp
-
-3. To get more info about a package type (for example)
-
-     opam show coq:mathcomp:discrete
-
-4. To install the ones you need, type (for example)
-
-     opam install coq:mathcomp:discrete
-
-   To take advantage of parallel hardware one can add
-   the flag -j to specify how many concurrent jobs are
-   run, for example type
-
-     opam install -j2 coq:mathcomp:discrete
-
-5. To remove a package, type (for example)
-
-     opam remove coq:mathcomp:discrete
-
-WINDOWS
-=======
-
-0. Install Coq using the official Windows installer from
-
-    ...
-
-1. Download and install the all in one bundle
-
-    ...
diff --git a/etc/INSTALL.md b/etc/INSTALL.md
new file mode 100644
index 0000000..f4b4f7b
--- /dev/null
+++ b/etc/INSTALL.md
@@ -0,0 +1,78 @@
+# INSTALLATION PROCEDURE
+
+Users familiar with OPAM can use such tool to install Coq and the Mathematical
+Components library with commands like `opam coq-mathcomp-fingroup`.
+
+This document is for users that installed Coq in another way, for example
+compiling it from sources.
+
+## REQUIREMENTS 
+
+Coq version 8.4pl6 or 8.5 (at the time of writing, beta3)
+
+## BUILDING
+
+The Mathematical Components library is divided into various installation
+units.  On can install the entire library (compilation time is XX) or only
+some of its units.
+
+In both cases, if Coq is not installed such that its binaries like `coqc`
+and `coq_makefile` are in the PATH, then the COQBIN environment variable
+must be set to point to the directory containing such binaries.
+For example:
+
+    export COQBIN=/home/gares/coq/bin/
+
+Now, to install the entire library, including the SSReflect proof language:
+
+    cd mathcomp-1.6/mathcomp
+    make -j2 && make install
+
+If one wants to only install a few modules he should instead run make
+inside the modules he wants to install *in the following order*:
+
+  1. ssreflect
+  2. fingroup
+  3. algebra
+  4. solvable
+  5. field
+  6. character
+
+This means that one cannot install, say, algebra without having already
+installed fingroup. An example:
+
+    cd mathcomp-1.6/mathcomp
+    cd ssreflect && make -j2 && make install
+    cd ../fingroup && make -j2 && make install
+
+## CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE
+
+The `mathcomp/ssreflect/` directory comes with a small configuration file
+`pg-ssr.el` to extend ProofGeneral (PG), a generic interface for
+proof assistants based on the customizable text editor Emacs, to the
+syntax of ssreflect.
+
+The >= 3.7 versions of ProofGeneral support this extension.
+
+- Following the installation instructions, unpack the sources of PG in
+a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add
+the following line to your .emacs file.
+Under Unix/MacOS:
+
+    (load-file
+      "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
+    (load-file "<my-pgssr-location>/pg-ssr.el")
+
+Under Windows+Cygwin:
+
+    (load-file
+      "C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el")
+    (load-file "<my-pgssr-location>\\pg-ssr.el")
+
+Where <my-pg-location> is the location of your own ProofGeneral
+directory, and where <my-pgssr-location> is the location of your pg-ssr.el
+file.
+
+Coq sources have a .v extension. Opening any .v file should
+automatically launch ProofGeneral.
+