Commit 69a8b5e8 authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap after strange conflict

parent 76617da9
......@@ -8,13 +8,6 @@
* more libraries (theories and modules)
* WhyML
** regions : strong update
** clone module
** ghost code
** extraction of Ocaml code
** logic symbols used in programs
* A true Jessie3 front-end ?
* traceability: Partially done
......@@ -61,6 +54,10 @@
le bon typage, et clone sera en premier lieu un de ces constructors
** cas d'utilisation: range d'entiers de Jessie, Flottants -> double ou single
containeurs pour Adacore et Claire
NON PRIORITAIRE ?
** regions : strong update
** ghost code
** logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI, besoin pour cours aux JFLA en janvier 2012
......@@ -98,9 +95,18 @@
* DELAYED Coq plugin
* Coq realization of theories
** corriger l'incoherence
** corriger l'incoherence, comprendre si on veut vraiment accepter
function x : 'a
(cf: en caml cela ne marche pas)
** make it really usable
** understand problems when trying to realize set.why.
Status of equality, relation with clone module feature
* DOC:
** document new tools why3stats and others if any
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
......@@ -110,6 +116,7 @@
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
* do not save if no change was made
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
......
[ATP alt-ergo-0.93.1]
name = "Alt-Ergo"
exec = "alt-ergo-0.93.1"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_trunk.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.93.1"
version_ok = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
......@@ -47,9 +31,9 @@ version_old = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3-2.4]
[ATP cvc3]
name = "CVC3"
exec = "cvc3-2.4.1"
exec = "cvc3"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.4.1"
......@@ -157,9 +141,9 @@ command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/verit.drv"
[ATP z3-3]
[ATP z3]
name = "Z3"
exec = "z3-3.2"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "3.2"
......@@ -181,7 +165,7 @@ name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.19"
version_old = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
......
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