stable

flocq-2.4.0-1.fc21, frama-c-1.10-18.fc21, & 4 more

FEDORA-2014-10505 created by jjames 10 years ago for Fedora 21

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

How to install

Updates may require up to 24 hours to propagate to mirrors. If the following command doesn't work, please retry later:

sudo dnf upgrade --refresh --advisory=FEDORA-2014-10505

This update has been submitted for testing by jjames.

10 years ago

AutoQA: depcheck test PASSED on i386. Result log: http://autoqa.fedoraproject.org/report/1fy5h (results are informative only)

AutoQA: depcheck test PASSED on x86_64. Result log: http://autoqa.fedoraproject.org/report/1fy5q (results are informative only)

This update is currently being pushed to the Fedora 21 testing updates repository.

10 years ago

This update has been pushed to testing

10 years ago

This update has reached 3 days in testing and can be pushed to stable now if the maintainer wishes

10 years ago

This update has been submitted for stable by jjames.

10 years ago

AutoQA: upgradepath test PASSED on noarch. Result log: http://autoqa.fedoraproject.org/report/1gerg (results are informative only)

jjames has edited this update. New build(s): frama-c-1.10-18.fc21, why-2.34-10.fc21, why3-0.85-2.fc21. Removed build(s): frama-c-1.10-16.fc21, why-2.34-9.fc21, why3-0.84-1.fc21.

10 years ago

This update has been submitted for testing by jjames.

10 years ago

AutoQA: depcheck test PASSED on i386. Result log: http://autoqa.fedoraproject.org/report/1gs9u (results are informative only)

AutoQA: depcheck test PASSED on x86_64. Result log: http://autoqa.fedoraproject.org/report/1gs9w (results are informative only)

This update is currently being pushed to the Fedora 21 testing updates repository.

10 years ago

This update has been pushed to testing

10 years ago

This update has been submitted for stable by jjames.

10 years ago

AutoQA: upgradepath test PASSED on noarch. Result log: http://autoqa.fedoraproject.org/report/1h729 (results are informative only)

This update is currently being pushed to the Fedora 21 stable updates repository.

10 years ago

This update is currently being pushed to the Fedora 21 stable updates repository.

10 years ago

This update has been pushed to stable

10 years ago

Please login to add feedback.

Metadata
Type
enhancement
Karma
0
Signed
Content Type
RPM
Test Gating
Settings
Unstable by Karma
-3
Stable by Karma
disabled
Stable by Time
disabled
Dates
submitted
10 years ago
in testing
10 years ago
in stable
10 years ago
modified
10 years ago

Automated Test Results