Commit 2e9d50af authored by MARCHE Claude's avatar MARCHE Claude

roadmap updated

parent 6c7c5d2c
......@@ -9,12 +9,31 @@
** extraction of Ocaml code
* Jessie3
* traceability
(Claude)
* Coq plugin
* Coq realization of theories
(Andrei)
* more libraries (theories and modules)
* IDE: reload
(claude)
* IDE: edition, navigation
(?)
* HOL
* IDE: no more threads
(qui ?)
* IDE: custom model
(JC + ?)
* why3bench sur examples/ dans make bench
(Francois)
* checkout frais, compilation (local ou non) et make bench chaque nuit sur moloch
(?)
* BD : se passer de sqlite3
(Claude)
* IDE: avoir des transformations non codees en dur
(Claude d'abord)
* Bug des md5
(Claude. pas reproductible ? Pb de duplication des buts ?)
* Papers to write
......
......@@ -501,9 +501,16 @@ let task_checksum t =
fprintf str_formatter "%a@." Pretty.print_task t;
let s = flush_str_formatter () in
(*
eprintf "task = %s@." s;
let tmp = Filename.temp_file "task" "out" in
let c = open_out tmp in
output_string c s;
close_out c;
*)
Digest.to_hex (Digest.string s)
let sum = Digest.to_hex (Digest.string s) in
(*
eprintf "task %s, sum = %s@." tmp sum;
*)
sum
let info_window ?(callback=(fun () -> ())) mt s =
......
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