We are happy to announce a new release of Why3, version 1.1.0, available
from the Web page http://why3.lri.fr/
Note to Opam users: Recently released packages (be it Why3 or other
software) are only available to Opam 2.0 users. Opam 1.2 users need to
resort to abstruse incantations, e.g., opam pin add why3.1.1.0
https://gitlab.inria.fr/why3/why3.git#1.1.0
Changes between 1.0.0 and 1.1.0 are as follows:
(":x:" marks a potential source of incompatibility)
Core
* variants can now be inferred on some lemma functions
* coercions are now supported for `if` and `match` branches
* `interrupt` command should now properly interrupt running provers.
* clearer typing error messages thanks to printing qualified names
* fixed handling of prover upgrades, resurrected the policy
"duplicate" and added a policy "remove"
API
* added `Call_provers.interrupt_call` to interrupt a running prover
(contribution by Pierre-Yves Strub)
Language
* program functions can now be marked `partial` to prevent them from
being used in ghost context; the annotation does not have to be
explicitly put on their callers
* `use` now accepts several module names separated by commas
* symbolic operators can be used in identifiers like `(+)_ident` or
`([])'ident`
* range types have now a default ordering to be used in `variant`
clause
Standard library
* library `ieee_float`: floating-point operations can now be used in
programs
Transformations
* `split_vc` behaves slightly differently :x:
Provers
* support for Alt-Ergo 2.1.0 (released Mar 14, 2018)
* support for Alt-Ergo 2.2.0 (released Apr 26, 2018)
* support for Coq 8.8.1 (released Jun 29, 2018)
* support for Coq 8.8.2 (released Sep 26, 2018)
* support for CVC4 1.6 (released Jun 25, 2018)
* support for Z3 4.7.1 (released May 23, 2018)
* support for Isabelle 2018 (released Aug 2018)
(contribution by Stefan Berghofer)
* dropped support for Isabelle 2016 (2017 still supported) :x:
* dropped support for Alt-Ergo versions < 2.0.0 :x:
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
