See for changes in coq 8.16.0.

Changes in flocq 4.0.0:

  • made Coq 8.12 the minimal version and removed the IEEE754.SpecFloatCompat layer
  • removed automatic export of ZArith and Reals from Core.Raux and Core.Core
  • proved a close/far-path adder in Calc.Plus
  • made IEEE754.Binary a wrapper around IEEE754.BinarySingleNaN

Changes in flocq 4.1.0:

  • added Bnearbyint and Btrunc in IEEE754
  • ensured compatibility from Coq 8.12 to 8.16

Changes in why3 1.5.1:

  • Numerous bug fixes
  • Documentation
    • documented most options of why3 prove and why3 execute
  • Python language
    • added construct e1 if e2 else e3
    • added support for tuples and multiple assignments
    • added #@ axiom and #@ lemma
    • global variables annotated with #@ constant are available in the logic
    • pure functions (i.e., limited to return e) annotated with #@ function are available in the logic
    • logical functions can be given a variant with variant {term}
  • Provers
    • support for Z3 4.9.0 and 4.9.1 (released July 6, 2022)
    • support for Z3 4.10.0, 4.10.1 and 4.10.2 (released July 30, 2022)
    • support for Z3 4.11.0 (released August 18, 2022)
    • support for Coq 8.16.0 (release September 5, 2022)
    • support for Gappa 1.4.0 (released April 16, 2022)

The frama-c, gappalib-coq, ocaml-menhir, and zenon builds are simple rebuilds due to the above changes.

This update's test gating status has been changed to 'waiting'.

3 months ago

This update's test gating status has been changed to 'ignored'.

3 months ago

This update has been submitted for stable by bodhi

3 months ago

Please login to add feedback.

Content Type
Test Gating
Unstable by Karma
Stable by Karma
Stable by Time
0 days
3 months ago
in testing
3 months ago
in stable
3 months ago

Automated Test Results