diff options
| -rw-r--r-- | etc/ANNOUNCE-1.6.md | 48 | ||||
| -rw-r--r-- | etc/INSTALL.md | 9 |
2 files changed, 52 insertions, 5 deletions
diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md new file mode 100644 index 0000000..6a27d6b --- /dev/null +++ b/etc/ANNOUNCE-1.6.md @@ -0,0 +1,48 @@ +# Ssreflect/MathComp 1.6 released + +We are proud to announce the immediate availability of the +Ssreflect proof language and the Mathematical Components library +version 1.6 for Coq 8.4pl6 and 8.5beta3. + +This release adds no new theory files. The proof language +received minor fixes while the libraries received minor additions. + +The developmet is now happening in the public and is mirrored +on github. Another annoucment specific to this will follow shortly. + +A detailed ChageLog is available at: + https://github.com/math-comp/math-comp/blob/master/etc/ChangeLog +Such document contains the list of new theorems as well as the list +of theorems that were renamed or replaced by more general variants. + +The main user visible change is that the library was split into the following components: + + 1. ssreflect: the ssreflect proof language and ... + 2. fingroup: finite groups theory... + 3. algebra: .. + 4. solvable: ... + 5. field: ... + 6. character: ... + +A user not needing the entire library can build only the components she +is interested in. Each component comes with a file one can Require and Import to load, at once, the entire component. For example "Require Import all_ssreflect." loads all the theory files in the ssreflect component. + +The main incompatibility concerning users is the change of logical/phisical path implied by the reorganization of the library. In particular "Require Ssreflect.ssreflect" does not work anymore. We propose a schema +that is compatible with both Coq 8.4 and Coq 8.5, namely: + Require Import mathcomp.ssreflect.ssreflect. + From mathcomp Require Import ssrfun ssrbool ... +The first line loads the ssreflect plugin using its full path. +Then all other files are loaded from the mathcomp namespace. +The component part (like ssreflect or algebra) can be safely omitted. +All theory files in the library follow this schema. Note that the +From directive has effect only in Coq 8.5. Coq 8.4 ignores it and +searches for files in all known paths. Beware of name collisions. + +The tarball can be download at the following URL: + http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz + +The html documentation of the theory files can be browsed at: + http://ssr.msr-inria.inria.fr/doc/mathcomp-1.6/ + +-- The Mathematical Components team + diff --git a/etc/INSTALL.md b/etc/INSTALL.md index f4b4f7b..83b4252 100644 --- a/etc/INSTALL.md +++ b/etc/INSTALL.md @@ -1,7 +1,7 @@ # 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`. +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. @@ -13,15 +13,14 @@ 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. +units. On can install the entire library (compilation time is around 35 minutes) 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/ + export COQBIN=/home/user/coq/bin/ Now, to install the entire library, including the SSReflect proof language: |