Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Project Filelist for Why3

File Release Notes and Changelog

Release Name: 0.84

Release Notes
A major visible change in this release is the way Why3 commands are
invoked: instead of several executables why3, why3config, why3ide,
why3replay, why3session, etc., there is only one Why3 executable
called why3, and the former executables are available as commands given
as first argument, e.g. "why3 config", "why3 ide", etc.

Another quite visible change is that session files are split in two
parts, as detailed below in the detailed changes.
Change Log
  * 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
  o 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.

  * 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.).

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

  o new transformation "compute_in_goal" that simplifies the goal, by
    computation, as much as possible