Commit 92d99e5e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Version 0.88.0

parent 903d9f69
...@@ -20,6 +20,7 @@ Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)> ...@@ -20,6 +20,7 @@ Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)> Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)> Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr> Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr> Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local> Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
......
* marks an incompatible change * marks an incompatible change
Version 0.88.0, October 6, 2017
===============================
Language Language
o two new forms of type declarations: integer range types and o two new forms of type declarations: integer range types and
floating-point types. To denote constants in such types, integer floating-point types. To denote constants in such types, integer
constants and real constants can be cast to such types. This constants and real constants can be cast to such types. This
support is exploited in drivers for provers that support bitvector support is exploited in drivers for provers that support bitvector
theories (CVC4, Z3) and floating-point theory (Z3). theories (CVC4, Z3) and floating-point theory (Z3).
More details in the manual, section 7.2.4 "Theories" More details in the manual, section 7.2.4 "Theories".
* a quote character (') inside an identifier must either be at the * a quote character (') inside an identifier must either be at the
end, or be followed by either a digit, the underscore character end, or be followed by either a digit, the underscore character
(_) or another quote. Identifiers with a quote followed by a (_) or another quote. Identifiers with a quote followed by a
...@@ -15,19 +18,18 @@ Language ...@@ -15,19 +18,18 @@ Language
Standard library Standard library
o new theory ieee_float formalizing floating-point arithmetic, o new theory ieee_float formalizing floating-point arithmetic,
conformant to IEEE-754, mapped to SMT-LIB FP theory. compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features User features
o proof strategies: why3 config now generates default proof strategies o proof strategies: why3 config now generates default proof strategies
using the installed provers. These are available under name "Auto using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide. More level 0", "Auto level 1" and "Auto level 2" in why3 ide.
details in the manual, section 10.6 "Proof Strategies" More details in the manual, section 10.6 "Proof Strategies".
o counterexamples: better support for array o counterexamples: better support for array values, support for
values, support for floating-point values, support for Z3 in floating-point values, support for Z3 in addition to CVC4.
addition to CVC4. More details in the manual, section 6.3.5 "Displaying Counterexamples".
More details in the manual, section 6.3.5 "Displaying Counterexamples"
Provers
Prover support
o support for Isabelle 2017 o support for Isabelle 2017
* discarded support for Isabelle 2016 (2016-1 still supported) * discarded support for Isabelle 2016 (2016-1 still supported)
o support for Coq 8.6.1 (released Jul 25, 2017) o support for Coq 8.6.1 (released Jul 25, 2017)
...@@ -40,11 +42,11 @@ Prover support ...@@ -40,11 +42,11 @@ Prover support
Version 0.87.3, January 12, 2017 Version 0.87.3, January 12, 2017
================================ ================================
bug fixes Bug fixes
o fixed OCaml extraction with respect to ghost parameters o fixed OCaml extraction with respect to ghost parameters
o assorted bug fixes o assorted bug fixes
provers Provers
o support for Alt-Ergo 1.30 (released Nov 21, 2016) o support for Alt-Ergo 1.30 (released Nov 21, 2016)
o support for Coq 8.6 (released Dec 8, 2016) o support for Coq 8.6 (released Dec 8, 2016)
o support for Gappa 1.3 (released Jul 20, 2016) o support for Gappa 1.3 (released Jul 20, 2016)
...@@ -55,14 +57,14 @@ provers ...@@ -55,14 +57,14 @@ provers
Version 0.87.2, September 1, 2016 Version 0.87.2, September 1, 2016
================================= =================================
bug fixes Bug fixes
o improved well-formedness of extracted OCaml code o improved well-formedness of extracted OCaml code
o assorted bug fixes o assorted bug fixes
Version 0.87.1, May 27, 2016 Version 0.87.1, May 27, 2016
============================ ============================
bug fixes Bug fixes
o assorted bug fixes o assorted bug fixes
Version 0.87.0, March 15, 2016 Version 0.87.0, March 15, 2016
......
# Why version # Why version
VERSION=0.87+git VERSION=0.88.0
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
%BEGIN LATEX %BEGIN LATEX
\begin{LARGE} \begin{LARGE}
%END LATEX %END LATEX
Version \whyversion{}, January 2017 Version \whyversion{}, October 2017
%BEGIN LATEX %BEGIN LATEX
\end{LARGE} \end{LARGE}
%END LATEX %END LATEX
......
...@@ -534,7 +534,7 @@ let show_legend_window () = ...@@ -534,7 +534,7 @@ let show_legend_window () =
let show_about_window () = let show_about_window () =
let about_dialog = let about_dialog =
GWindow.about_dialog GWindow.about_dialog
~name:"The Why3 Verification Platform " ~name:"The Why3 Verification Platform"
~authors:["François Bobot"; ~authors:["François Bobot";
"Jean-Christophe Filliâtre"; "Jean-Christophe Filliâtre";
"Claude Marché"; "Claude Marché";
...@@ -548,6 +548,7 @@ let show_about_window () = ...@@ -548,6 +548,7 @@ let show_about_window () =
"Martin Clochard"; "Martin Clochard";
"Simon Cruanes"; "Simon Cruanes";
"Sylvain Dailler"; "Sylvain Dailler";
"Jacques-Pascal Deplaix";
"Clément Fumex"; "Clément Fumex";
"Leon Gondelman"; "Leon Gondelman";
"David Hauzar"; "David Hauzar";
...@@ -556,6 +557,7 @@ let show_about_window () = ...@@ -556,6 +557,7 @@ let show_about_window () =
"Mikhail Mandrykin"; "Mikhail Mandrykin";
"David Mentré"; "David Mentré";
"Benjamin Monate"; "Benjamin Monate";
"Kim Nguyễn";
"Thi-Minh-Tuyen Nguyen"; "Thi-Minh-Tuyen Nguyen";
"Simão Melo de Sousa"; "Simão Melo de Sousa";
"Asma Tafat"; "Asma Tafat";
...@@ -564,9 +566,11 @@ let show_about_window () = ...@@ -564,9 +566,11 @@ let show_about_window () =
] ]
~copyright:"Copyright 2010-2017 Inria, CNRS, Paris-Sud University" ~copyright:"Copyright 2010-2017 Inria, CNRS, Paris-Sud University"
~license:("See file " ^ Filename.concat Config.datadir "LICENSE") ~license:("See file " ^ Filename.concat Config.datadir "LICENSE")
~website:"http://why3.lri.fr" ~website:"http://why3.lri.fr/"
~website_label:"http://why3.lri.fr" ~website_label:"http://why3.lri.fr/"
~version:Config.version ~version:Config.version
~icon:!why_icon
~logo:!why_icon
() ()
in in
let ( _ : GWindow.Buttons.about) = about_dialog#run () in let ( _ : GWindow.Buttons.about) = about_dialog#run () in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment