Changes in flocq 3.4.1:

  • ensured compatibility from Coq 8.7 to 8.14

Changes in flocq 3.4.2:

  • restored compatibility with Coq 8.11

Changes in frama-c 23.0 Vanadium:

Changes in why3 1.4.0, where :x: marks a backwards incompatibility

  • WhyML

    • sub-namespaces are now allowed in for each loops; see Section 7.4.7 of the manual
    • function literals are now supported; see Sections 7.3.2 and 7.4.9 of the manual
  • Standard library

    • added lemma permut_sub_trans to array.ArrayPermut
    • added function inter (intersection) to bag.Bag
    • added a new theory option.Map
    • added a precondition to string.OCaml.([])
    • added functions set, init, sub to mach.array.ArrayInt63
    • moved OCaml exception Invalid_argument to ocaml.Exceptions :x:
    • added function length in mach.c.String
    • added functions sdiv and srem to bv
    • added signed operations to mach.bv
    • added missing module for double-precision floats to mach.floats
  • Tools

    • command-line options now follow the getopt standard; in particular, long options start with -- :x:
    • binaries why3config, why3prove, etc, no longer exist; they are now plugins that can be loaded only using the main why3 binary, e.g., why3 config :x:
    • why3 config now uses subcommands instead of options; in particular, prover detection is performed using why3 config detect and manual prover addition is performed using why3 config add-prover; see Section 6.1 of the manual :x:
    • why3 execute now provides runtime assertion checking; see Section 6.8.1 of the manual
    • runtime assertion checking is also used to validate counterexamples in why3 prove
    • loop invariants can now be inferred automatically; see Section 8.5 of the manual
    • JSON output of counterexamples was modified :x:
  • IDE

    • native keyboard modifiers are now used on macOS
    • why3 ide in the Docker image can now be used through a web browser instead of an X server; see Section 5.1.2 of the manual
  • Input Formats

    • a new front-end named MLCFG was added; it supports unstructured program codes, including goto statements; see Section 9.3 of the manual
    • translation of <> and not have been fixed for micro-C and Python
  • Extraction

    • allowed transitive inclusion (export) of interfaces and preludes
    • added remove module for drivers to exclude modules
    • added C extraction of strings
    • improved handling of C header files
    • added support of blacklist to C extraction
    • fixed extraction of partially applied functions
    • fixed OCaml extraction of nested tuples
    • fixed OCaml extraction of OneTime integers
  • Web interface TryWhy3

    • ?lang=foo can now be used to select an input format other than WhyML; the input format can also be changed dynamically using a combobox
    • ?code=foo can now be used to fill the editor with some code; the encoded string can be retrieved by clicking the "Copy URL" button
    • examples are no longer embedded; only files mentioned in examples/index.txt are considered :x:
    • Alt-Ergo workers can now be stopped without losing the session
  • Provers

    • support for PVS 7.1 (released Apr 30, 2020)
    • support for Z3 4.8.7 (released Nov 19, 2019)
    • support for Z3 4.8.8 (released May 9, 2020)
    • support for Z3 4.8.9 (released Sep 11, 2020)
    • support for Z3 4.8.10 (released Jan 20, 2021)
    • support for AltErgo 2.3.3 (released Aug 19, 2020)
    • support for AltErgo 2.4.0 (released Jan 22, 2021)
    • support for Coq 8.13.0 (released Jan 7, 2021)
    • support for CVC4 1.8 (released Jun 19, 2020)
  • Documentation

    • Why3 modes for editors (Section 5.3)
    • Why3-specific configuration for shells (Section 5.4)
    • detailed explanations on semantics of various WhyML statements (Section 7.4)
    • detailed explanations on WhyML module system (Section 7.5)
    • explanations on how users can customize drivers (Section 12.5)
  • API

    • helpers were added to ease production of parse trees; see Section 4.9 of the manual
    • generation of counterexamples was changed; see Section 4.10 of the manual :x:
  • Additional bug fixes

    • fixed why3 prove when called on a DIMACS file
    • improved detection of out-of-range values in why3 execute
    • fixed micro-Python parser when there is no newline at end of file
    • fixed SMT translation of negative floating-point literals
    • fixed set of reserved symbols for SMT solvers
    • restored hypothesis_selection transformation
    • fixed unsoundness of transformations case and destruct in presence of polymorphic formulas

The gappalib-coq build is a simple rebuild due to the flocq update.

How to install

sudo dnf upgrade --advisory=FEDORA-2021-9f6c4fa5e7

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

4 months ago

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

4 months ago

This update has been submitted for stable by bodhi

4 months 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
3
Stable by Time
0 days
Dates
submitted
4 months ago
in testing
4 months ago
in stable
4 months ago

Automated Test Results