diff options
| -rw-r--r-- | etc/ANNOUNCE-1.6.md | 35 | ||||
| -rw-r--r-- | etc/ChangeLog | 21 | ||||
| -rw-r--r-- | etc/INSTALL.md | 25 |
3 files changed, 46 insertions, 35 deletions
diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md index 4f5b1a4..91169ad 100644 --- a/etc/ANNOUNCE-1.6.md +++ b/etc/ANNOUNCE-1.6.md @@ -9,8 +9,10 @@ received minor fixes while the libraries received minor additions. A detailed ChangeLog is available at: https://github.com/math-comp/math-comp/blob/master/etc/ChangeLog -This document contains the list of new theorems as well as the list -of theorems that were renamed or replaced by more general variants. +This document contains in particulat the list of new theorems as well +as the list of theorems that were renamed or replaced by more +general variants. + Our development repository is now public, and mirrored on github: https://github.com/math-comp/math-comp @@ -45,30 +47,15 @@ entire component. For example the command loads all the theory files in the contained in the 'ssreflect' component. -This modularity comes at the price of an incompatibility for users of -previous version of the Mathematical Components library, due to the -change of logical/physical paths implied by the reorganization of the -library. In particular the command line - - Require Ssreflect.ssreflect. - -does not work anymore. We propose a replacement schema for such -command lines that is compatible with both versions 8.4 and 8.5 of -Coq, namely replacing the previous line with: - - Require Import mathcomp.ssreflect.ssreflect. - - From mathcomp Require Import ssrfun ssrbool ... +Note that this modularity comes at the price of a possible +incompatibility for users of previous version of the Mathematical +Components library, due to the change of logical/physical paths +implied by the reorganization of the library. See the installation +notes for more on this issue an a suggested migration scheme. -The first line loads the ssreflect plugin using its full path. -Then all other files are loaded from the mathcomp name space. -The component part (like ssreflect or algebra) is 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: hence beware of the -possible name collisions. +The tarball can be download at +http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz -The tarball can be download at 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/ diff --git a/etc/ChangeLog b/etc/ChangeLog index a603a9f..ee28d7d 100644 --- a/etc/ChangeLog +++ b/etc/ChangeLog @@ -1,26 +1,28 @@ -24/11/2015 - major reorganization of the archive - version 1.6 - * Files split into subdirectories: ssreflect, algebra, fingroup, +24/11/2015 - major reorganization of the archive - version 1.6 + * Files split into subdirectories: ssreflect, algebra, fingroup, solvable, field and character. In this way the user can decide to compile only the subset of the Mathematical Components library - that is relevant to her. + that is relevant to her. Note that this introduces a possible + incompatibility for users of the previous version. A replacement + scheme is suggested in the installation notes. * The archive is now open and based on git. Public mirror at: https://github.com/math-comp/math-comp - - * Sources of the reference manual of the Ssreflect tactic language are + + * Sources of the reference manual of the Ssreflect tactic language are also open and available at: https://github.com/math-comp/ssr-manual Pull requests improving the documentation are welcome. - + * Renamings or replacements: conjC_closed -> cfConjC_closed class_transr -> class_eqP cfclass_transl -> cfclass_transr nontrivial_ideal -> proper_ideal zchar_orthonormalP -> vchar_orthonormalP - + * Definitions that changed: - seq_sub + seq_sub * Statements that changed: orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, @@ -28,7 +30,7 @@ lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, ltr0_neq0, ltr_prod, Zisometry_of_iso - + * New definitions: adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type @@ -90,4 +92,3 @@ 18/03/2008 - ssreflect - version 1.1 * First public release - diff --git a/etc/INSTALL.md b/etc/INSTALL.md index 83b4252..0ea3c4c 100644 --- a/etc/INSTALL.md +++ b/etc/INSTALL.md @@ -6,7 +6,7 @@ Users familiar with OPAM can use such tool to install Coq and the Mathematical C This document is for users that installed Coq in another way, for example compiling it from sources. -## REQUIREMENTS +## REQUIREMENTS Coq version 8.4pl6 or 8.5 (at the time of writing, beta3) @@ -75,3 +75,26 @@ file. Coq sources have a .v extension. Opening any .v file should automatically launch ProofGeneral. +## TRANSITION FROM 1.5 to 1.6 + +The change of logical/physical paths implied by the reorganization of the +library causes an incompatibility for users of previous version of the +Mathematical Components library. For instance the command line + + Require Ssreflect.ssreflect. + +does not work anymore. We propose a replacement schema for such +command lines that is compatible with both versions 8.4 and 8.5 of +Coq, namely replacing the previous line with: + + 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 name space. +The component part (like ssreflect or algebra) is 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: hence beware of the +possible name collisions. |