aboutsummaryrefslogtreecommitdiff
path: root/etc/ANNOUNCE-1.6.md
diff options
context:
space:
mode:
authorEnrico Tassi2015-12-04 14:27:51 +0100
committerEnrico Tassi2015-12-04 14:27:51 +0100
commit0b02d109c93af8bf50626d47c680ebc9f4ee820e (patch)
tree5560d8dfdb3e9f866deeb7818dcf85ab1db6aabb /etc/ANNOUNCE-1.6.md
parentcfb80117f9e947e83b56d0b07eccafdc057f2c8d (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.md51
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