diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 105 |
1 files changed, 30 insertions, 75 deletions
@@ -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) |