Fedora 21 Update: gappalib-coq-1.0.0-12.fc21

[updates at fedoraproject.org]

--------------------------------------------------------------------------------
Fedora Update Notification
FEDORA-2014-10505
2014-09-10 01:58:20
--------------------------------------------------------------------------------

Name        : gappalib-coq
Product     : Fedora 21
Version     : 1.0.0
Release     : 12.fc21
URL         : http://gappa.gforge.inria.fr/
Summary     : Coq support library for gappa
Description :
This support library provides vernacular files so that the certificates
Gappa generates can be imported by the Coq proof assistant.  It also
provides a "gappa" tactic that calls Gappa on the current Coq goal.

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques --
automatic proof generation of arithmetic properties) is a tool intended
to help verifying and formally proving properties on numerical programs
dealing with floating-point or fixed-point arithmetic.

--------------------------------------------------------------------------------
Update Information:

This update removes an obsolete ExcludeArch tag from ocaml-zip.  Besides ocaml-zip, flocq and why3, the other updates are just rebuilds due to the updated packages.

Changes in flocq 2.4.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
- added theorems about double rounding being innocuous (Fappli_double_round.v)
- improved a bit the efficiency of IEEE-754 arithmetic

Changes in why3 0.84:

Tools:
- file generated by "why3session html f.mlw" is now "f/why3session.html" and not "f/f.html"
- the default behavior of why3 has been moved to the "prove" subcommand
- options --exec, --extract, and --realize, have been moved to subcommands: execute, extract, and realize
- why3replayer has been moved to the "replay" subcommand
- other tools have been moved to why3 subcommands too: config, doc, ide, session, wc; for local usage, the old commands are still available

Proof sessions:
- session files are split in two parts: "why3session.xml" and "why3shapes". The latter file contains the checksums and the shapes for the goals. That second file is not strictly needed for replaying a proof session, it is only useful when input programs are modified, to track obsolete goals. If Why3 is compiled with compression support (provided by ocamlzip library) then files for shapes are compressed into why3shapes.gz.

Library:
- renamed array.ArraySorted -> array.IntArraySorted. array.ArraySorted is now generic, with type and order relation parameters
- reduced amount of "use export" in the standard library: theories now only export the symbols they define. Users may need to insert more "use import" in their theories (typically int.Int, option.Option, list.List, etc.).

Provers:
- fixed Coq printer (former Coq proofs may have to be updated, by removing non-emptiness constraints from polymorphic type applications)
- support for Coq8.4pl4
- support for Isabelle2014
- support for CVC4 1.4
- updated support for TPTP TFA syntax (used by provers Beagle and Princess)

Transformations:
- new transformation "compute_in_goal" that simplifies the goal, by computation, as much as possible

Changes in why3 0.85:

Language:
- fix a soundness bug in the detection of aliases when calling a WhyML function: some alias could have been forgotten when a type variable was substituted with a mutable type

Sessions:
- use the full path of identifiers when the user introduces namespaces (BTS #17181)

Transformations:
- fix a soundness bug in "compute_in_goal" regarding the handling of logical implication.
- several improvements to "compute_in_goal":
    - left-hand side of rewrite rules can be any symbols, not only non-interpreted ones.
    - perform beta-reduction when possible
    - the maximal number of reduction steps can be increased using meta "compute_max_steps"
    - the transformation is documented in details in the manual
- new transformation "compute_specified":
    - less aggressive variant of "compute_in_goal"
    - Unfolding of definitions is controlled using meta "rewrite_def"
- fixed a bug in "eliminate_if" when applied on inductive definitions

Provers:
- fixed wrong warning when detecting Isabelle2014

--------------------------------------------------------------------------------

This update can be installed with the "yum" update program.  Use
su -c 'yum update gappalib-coq' at the command line.
For more information, refer to "Managing Software with yum",
available at http://docs.fedoraproject.org/yum/.

All packages are signed with the Fedora Project GPG key.  More details on the
GPG keys used by the Fedora Project can be found at
https://fedoraproject.org/keys
--------------------------------------------------------------------------------