From e112153a07ac7aa2605c99f8137e248b2b55ea3f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond <guillaume.melquiond@inria.fr> Date: Mon, 25 Jun 2018 10:10:54 +0200 Subject: [PATCH] New release. --- CHANGES.md | 19 +++++++++++-------- ROADMAP | 1 - Version | 2 +- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d3cde36af..d4b65724d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,28 +1,31 @@ :x: marks a potential source of incompatibility +Version 1.0.0, June 25, 2018 +---------------------------- + Core * improved support of counter-examples + * attribute `[@vc:sp]` on an expression switches from traditional WP + to Flanagan-Saxe-like VC generation + * type invariants now produce logical axioms; + a type with an invariant must be proved to be inhabited :x: + * logical symbols can no longer be used in non-ghost code; + in particular, there is no polymorphic equality in programs any more, + so equality functions must be declared/defined on a per-type basis + (already done for type `int` in the standard library) :x: Language * numerous changes to syntax, see documentation appendix :x: * `let function`, `let predicate`, `val function`, and `val predicate` introduce symbols in both logic and programs - * logical symbols can no longer be used in non-ghost code; - in particular, there is no polymorphic equality in programs any more, - so equality functions must be declared/defined on a per-type basis - (already done for type `int` in the standard library) :x: * added overloading of program symbols * new contract clause `alias { <term> with <term>, ... }` :x: * support for parallel assignment `<term>,... <- <term>,...` - * type invariants now produce logical axioms; - a type with an invariant must be proved to be inhabited :x: * support for local exceptions using `exception ... in ...` * added `break`, `continue`, and `return` statements * support for `exception` branches in `match` constructs * support for `for` loops on range types (including machine integers from the standard library) - * attribute `[@vc:sp]` on an expression switches from traditional WP - to Flanagan-Saxe-like VC generation * support for type coercions in logic using `meta coercion` * keyword `theory` is deprecated; use `module` instead * term on the left of sequence `;` must be of type `unit` :x: diff --git a/ROADMAP b/ROADMAP index 6b4a9a843..98eba54cb 100644 --- a/ROADMAP +++ b/ROADMAP @@ -112,7 +112,6 @@ ============ Making a release ============ * check the BTS -* do "make update-coq" and "make", fix Coq realizations if needed * check that nightly bench is OK * check that "make xml-validate-local" is OK (see below : copy the dtd on the web) diff --git a/Version b/Version index a9450123e..624badec2 100644 --- a/Version +++ b/Version @@ -1 +1 @@ -VERSION=1.00+git +VERSION=1.0.0 -- GitLab