Commit af9470bf authored by Tuyen Nguyen's avatar Tuyen Nguyen
parents b3f20c37 4081a8f9
......@@ -15,7 +15,7 @@
** extraction of Ocaml code
** logic symbols used in programs
* Jessie3
* A true Jessie3 front-end ?
* traceability: Partially done
(Claude)
......@@ -47,14 +47,24 @@
=== Roadmap for next release ========================
* fix support for newer Z3, CVC3 and Alt-Ergo, allow several version
of them at the same time. Allow why3config --detect to find e.g z3
under names like z3-3.2 (how ? command-line option ? e.g. -p z3 /usr/local/bin/z3-3.2)
* move Session module and its dependencies into the Why3 library
* document new tools why3stats or others
* Ensure that we kill a prover after some time (ressurect %T ? with a
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
* update the BTS
* API for programs
* reject global "val"s in typing environment for logic decls.
* move session.ml and its dependencies into the Why3 lib
* Coq plugin
* Coq realization of theories
......
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