Skip to content

Commit

Permalink
better wording and package description in the ANNOUNCE for 1.6
Browse files Browse the repository at this point in the history
  • Loading branch information
Enrico Tassi committed Dec 4, 2015
1 parent cfb8011 commit 0b02d10
Showing 1 changed file with 31 additions and 20 deletions.
51 changes: 31 additions & 20 deletions etc/ANNOUNCE-1.6.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 0b02d10

Please sign in to comment.