diff options
| -rw-r--r-- | etc/INSTALL | 50 | ||||
| -rw-r--r-- | etc/INSTALL.md | 78 |
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. + |