diff options
| author | Enrico Tassi | 2015-12-04 14:27:51 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-04 14:27:51 +0100 |
| commit | 0b02d109c93af8bf50626d47c680ebc9f4ee820e (patch) | |
| tree | 5560d8dfdb3e9f866deeb7818dcf85ab1db6aabb /etc/ANNOUNCE-1.6.md | |
| parent | cfb80117f9e947e83b56d0b07eccafdc057f2c8d (diff) | |
better wording and package description in the ANNOUNCE for 1.6
Diffstat (limited to 'etc/ANNOUNCE-1.6.md')
| -rw-r--r-- | etc/ANNOUNCE-1.6.md | 51 |
1 files changed, 31 insertions, 20 deletions
diff --git a/etc/ANNOUNCE-1.6.md b/etc/ANNOUNCE-1.6.md index 6a27d6b..a5ad8cb 100644 --- a/etc/ANNOUNCE-1.6.md +++ b/etc/ANNOUNCE-1.6.md @@ -7,36 +7,47 @@ 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: ... +The development is now taking place in the public and is mirrored +on github. Another announcement specific to this will follow shortly. -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 user visible change is that the library was split into the following components: -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: + 1. ssreflect: Ssreflect proof language, lists, boolean predicates, natural + numbers, types with a decidable equality, finite types, finite sets, finite + functions, finite graphs, basic arithmetics and prime numbers, big operators + 2. fingroup: finite groups, group quotients, group morphisms, group + presentation, group action + 3. algebra: discrete algebraic structures as ring, fields, ordered fields, + real fields, modules, algebras, vector spaces and integers, rational + numbers, polynomials, matrices, vector spaces + 4. solvable: more definitions and theorems about finite groups + 5. field: field extensions, Galois theory, algebraic numbers, cyclotomic + polynomials + 6. character: group representations, characters and class functions + +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/physical +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. +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. 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 |
