# 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.

It also contains the proof of the Odd Order Theorem, that builds on top
of the Mathematical Components Library.

# 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.

We provide a convenience root Makefile in order to compile all packages
at once using `make`.  This is the simplest option.

We also provide `opam` files to compile each package using `OPAM`.
Note that the `OPAM` packages for the Mathematical Components library
are available in the standard Coq `OPAM` repositories,
under the `coq-mathcomp-` name space.  If you are only interested
in installing a Mathematical Components package via `OPAM`, follow
the standard instructions available on the Coq website.

## 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 with 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.5.dev coq-mathcomp-ssreflect
```