Commit 705916dd authored by MARCHE Claude's avatar MARCHE Claude

roadmap

parent feaaff6d
......@@ -2,6 +2,10 @@
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
* calls to prover can now be asynchronous
Driver.prove_task now returns some intermediate value (of type
......
......@@ -8,7 +8,7 @@
** ghost code
** extraction of Ocaml code
* Jessie3
* traceability
* traceability: Partially done
(Claude)
* Coq plugin
* Coq realization of theories
......@@ -19,8 +19,7 @@
* IDE: edition, navigation
(?)
* HOL
* IDE: no more threads
(qui ?)
* IDE: custom model
(JC + ?)
* why3bench sur examples/ dans make bench
......@@ -52,8 +51,11 @@
=== Roadmap for third release =================================================
* (DONE) IDE: no more threads
* proof replay
** in IDE: replay all obsolete but previously successful proofs
** (DONE) IDE: replay all obsolete but previously successful proofs
** in whybench
** add replay of existing proofs in "make bench" to detect regression
** add automatic recompilation, install and bench every night on moloch
......@@ -61,7 +63,7 @@
* IDE: implement "inline" (use transformation inline_goal)
** partially done
** problem 1: detect that transformation did nothing
** problem 2: reimport form db does apply inline correctly
** (DONE) problem 2: reimport from db does apply inline correctly
* IDE: debug "hide proved goals" feature
** suggested solution: replace model + filter_model by a custom model
......
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