Changes in flocq 2.6.0:

  • ensured compatibility from Coq 8.4 to 8.7
  • removed some hypotheses on some lemmas of Fcore_ulp
  • added lemmas to Fprop_plus_error
  • improved examples

Changes in why3 0.88.0:

  • two new forms of type declarations: integer range types and floating-point types. To denote constants in such types, integer constants and real constants can be cast to such types. This support is exploited in drivers for provers that support bitvector theories (CVC4, Z3) and floating-point theory (Z3). More details in the manual, section 7.2.4 "Theories".
  • a quote character (') inside an identifier must either be at the end, or be followed by either a digit, the underscore character (_) or another quote. Identifiers with a quote followed by a letter are reserved.
  • new theory ieee_float formalizing floating-point arithmetic, compliant to IEEE-754, mapped to SMT-LIB FP theory.
  • proof strategies: why3 config now generates default proof strategies using the installed provers. These are available under name "Auto level 0", "Auto level 1", and "Auto level 2" in why3 ide. More details in the manual, section 10.6 "Proof Strategies".
  • counterexamples: better support for array values, support for floating-point values, support for Z3 in addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples".
  • support for Isabelle 2017
  • discarded support for Isabelle 2016 (2016-1 still supported)
  • support for Coq 8.6.1 (released Jul 25, 2017)
  • tentative support for Coq 8.7
  • discarded tactic support for Coq 8.4 (proofs still supported)
  • support for CVC4 1.5 (released Jul 10, 2017)
  • support for E 2.0 (released Jul 4, 2017)
  • support for E 1.9.1 (release Aug 31, 2016)

The gappalib-coq, frama-c, and why builds are just rebuilds due to the new versions of flocq and why3.

How to install

sudo dnf upgrade --advisory=FEDORA-2017-93d7fb97b0

This update has been submitted for testing by jjames.

4 years ago

This update has been pushed to testing.

4 years ago

jjames edited this update.

New build(s):

  • why-2.39-2.fc27
  • frama-c-15.0-3.fc27
  • why3-0.88.0-1.fc27

Removed build(s):

  • why3-0.87.3-12.fc27

Karma has been reset.

4 years ago

This update has been submitted for testing by jjames.

4 years ago

This update has been pushed to testing.

4 years ago

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

4 years ago

This update has been submitted for stable by jjames.

4 years ago

This update has been pushed to stable.

4 years ago

Please login to add feedback.

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

Automated Test Results