Commit b55f6bd6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Updated Roadmap. We could make a new release soon, say in June

parent eecfc98c
...@@ -18,12 +18,16 @@ ...@@ -18,12 +18,16 @@
* Coq realization of theories * Coq realization of theories
(Andrei) (Andrei)
* more libraries (theories and modules) * more libraries (theories and modules)
* IDE: edition, navigation * IDE: edition, navigation
(partially done) (partially done)
* HOL * HOL
* IDE: custom model * IDE: reimplement "hide proved goals" feature
** suggested solution: replace model + filter_model by a custom model
(JC + ?) (JC + ?)
* why3bench sur examples/ dans make bench * why3bench sur examples/ dans make bench
(Francois) (Francois)
...@@ -45,6 +49,11 @@ ...@@ -45,6 +49,11 @@
* Check if doc is up-to-date * Check if doc is up-to-date
* Add as many examples as possible in the regression tests
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
* DONE checkout frais, compilation (local ou non) et make bench chaque nuit sur moloch * DONE checkout frais, compilation (local ou non) et make bench chaque nuit sur moloch
(?) (?)
...@@ -74,14 +83,10 @@ ...@@ -74,14 +83,10 @@
** DONE add replay of existing proofs in "make bench" to detect regression ** DONE add replay of existing proofs in "make bench" to detect regression
** DONE add automatic recompilation, install and bench every night on moloch ** DONE add automatic recompilation, install and bench every night on moloch
* IDE: implement "inline" (use transformation inline_goal) * DONE IDE: implement "inline" (use transformation inline_goal)
** partially done
** problem 1: detect that transformation did nothing ** problem 1: detect that transformation did nothing
** (DONE) problem 2: reimport from 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
* DONE IDE: debug "remove" et "clean" qui provoquent des segfaults !! * DONE IDE: debug "remove" et "clean" qui provoquent des segfaults !!
* IDE: ajouter "invalid" comme cas de resultats de preuve * IDE: ajouter "invalid" comme cas de resultats de preuve
......
...@@ -1434,7 +1434,9 @@ let transformation_on_goal g tr = ...@@ -1434,7 +1434,9 @@ let transformation_on_goal g tr =
eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task); eprintf "addresses: %x %x@." (Obj.magic g.task) (Obj.magic task);
*) *)
s1 <> s2 s1 <> s2
(* task != g.task *) (*
task != (get_task g)
*)
| _ -> true | _ -> true
in in
if b then if b then
......
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