updated ROADMAP and CHANGES

parent 490e6428
* marks an incompatible change
o [WhyML] programs labels with new syntax 'L: (instead of label L:)
o [Coq output] fixed bug 12934: type def with several type params
version 0.70, July 6, 2011
==========================
New features
o [WhyML] language and VC generator
o [syntax] record types
- introduced with syntax "type t = {| a:int; b:bool |}"
actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
i.e. an algebraic with one constructor and projection functions
- a record expression is written {| a = 1; b = True |}
o new tool why3replayer: batch replay of a Why3 session created in IDE
Fixes and other changes
* [syntax] new syntax for conjunction (/\) and disjunction (\/)
("and" and "or" do not exist anymore)
* [syntax] "logic" is not a keyword anymore, use "function" and "predicate"
o [IDE] interactive detection of provers disabled because incompatible
with session. Detection must be done with why3config --detect-provers
o [WhyML] mutable record fields and type models
o why3replayer
* "parameter" keyword renamed to "val"
* new syntax for conjunction (/\) and disjunction (\/)
("and" and "or" do not exist anymore)
* "logic" is not a keyword anymore, use "function" and "predicate"
* functions to create an environment are now exported from Env
o [IDE] bug 12244 resolved by using Task.task_equal
o fixed Alt-ergo output: no triggers for "exists" quantifier
o [IDE] tool "Replay" works
o [IDE] does not use Threads anymore, thanks to Call_provers.query_call
o VC gen produces explanations in a suitable form for IDE
o [IDE] displays explanations using labels of the form "expl:..."
o fixed Coq output for polymorphic inductive predicates
o [IDE] dropped dependence on Sqlite
* calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value (of type
prover_call), which can be queried in two ways:
o [Alt-Ergo output] bugfix: no triggers for "exists" quantifier
o [Coq output] bugfix: polymorphic inductive predicates
o [Coq output] fixed bug 12934: type def with several type params
* [API] functions to create an environment are now exported from Env
* [API] calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value
(of type prover_call), which can be queried in two ways:
- blocking way with Call_provers.wait_on_call
- non-blocking way with Call_provers.query_call
So old code performing "prove_task t () ()" should be translated to
"wait_on_call (prove_task t ()) ()".
o record types
- introduced with syntax "type t = {| a:int; b:bool |}"
actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
i.e. an algebraic with one constructor and projection functions
- a record expression is written {| a = 1; b = True |}
version 0.64, Feb 16, 2011
==========================
......
......@@ -76,7 +76,7 @@
* Final preparation: put on the web page
** why3-0.70.tar.gz
** manual in PDF: TODO: check that macro \todo can be commented out
** DONE manual in PDF: check that macro \todo can be commented out
from ./macros.tex
** API doc in HTML (suggestion: http://why3.lri.fr/api/)
Note: check that URL of API doc is correct in doc/api.tex line 9.
......@@ -91,13 +91,12 @@
* DONE update why3 output of Why2, release Why 2.30
* The last commit (A):
** increment the magic number in config (DONE this morning do we really need another bump? But that cost nothing...)
** DONE increment the magic number in config
** add a tag to the git repository
** The next commit : increment de why3 version
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
(JC)
* DONE Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs (JC)
* DONE document "Make obsolete" (A+C)
......
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