Project Filelist for Why3
File Release Notes and Changelog
Release Name: 0.84
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.
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 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. 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) 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) transformations o new transformation "compute_in_goal" that simplifies the goal, by computation, as much as possible