diff --git a/Makefile.in b/Makefile.in
index abc65391312ad7adf518d56e110096b5a2932649..1123227472bb414379f9dc26f86e94bde7cd06f0 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -481,7 +481,7 @@ endif
ifeq (@enable_bench@,yes)
-BENCH_FILES = bench benchrc whybench
+BENCH_FILES = bench benchrc benchdb whybench
BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
diff --git a/src/bench/bench.ml b/src/bench/bench.ml
index 7e18b133042ae369843113abac319dc69a750b10..0848d288b71e8e1cb031b3f2284f7f81f01eb3f6 100644
--- a/src/bench/bench.ml
+++ b/src/bench/bench.ml
@@ -80,126 +80,104 @@ type proof_attempt_status =
open Format
-let print_prover_answer fmt = function
- | Db.Success -> fprintf fmt "Valid"
- (* | Invalid -> fprintf fmt "Invalid" *)
- | Db.Timeout -> fprintf fmt "Timeout"
- | Db.Unknown -> fprintf fmt "Unknown"
- | Db.Failure -> fprintf fmt "Failure"
- | Db.Undone -> fprintf fmt "Undone"
-
-let print_why_result fmt = function
- | InternalFailure exn ->
- Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
- | Done (pr,_) -> print_prover_answer fmt pr
-
-let print_pas fmt = function
- | Runned sp -> fprintf fmt "Runned %a" print_why_result sp
- | Cached (p,t) -> fprintf fmt "Cached (%a,%f)" print_prover_answer p t
-
type callback = tool_id -> prob_id ->
task -> int -> proof_attempt_status -> unit
-let proof_status_to_db_result pr =
- match pr with
- | {pr_answer = Valid} -> (Db.Success,pr.pr_time)
- | {pr_answer = Invalid} -> (Db.Unknown,pr.pr_time)
- (* TODO add invalid in Db *)
- | {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
- | {pr_answer = Failure _ | HighFailure} -> (Db.Failure,pr.pr_time)
- | {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
-
let debug_call = Debug.register_flag "call"
let debug = Debug.register_flag "bench_core"
-open Worker
+
+module BenchUtil =
+struct
+
+ let print_proof_status fmt = function
+ | Db.Success -> fprintf fmt "Valid"
+ (* | Invalid -> fprintf fmt "Invalid" *)
+ | Db.Timeout -> fprintf fmt "Timeout"
+ | Db.Unknown -> fprintf fmt "Unknown"
+ | Db.Failure -> fprintf fmt "Failure"
+ | Db.Undone -> fprintf fmt "Undone"
+
+ open Worker
(* number of scheduled external proofs *)
-let coef_buf = 2
-let scheduled_proofs = ref 0
-let maximum_running_proofs = ref 2
+ let coef_buf = 2
+ let scheduled_proofs = ref 0
+ let maximum_running_proofs = ref 2
(* they are protected by a lock *)
-let answers_queue = Queue.create ()
-let queue_lock = Mutex.create ()
-let queue_condition = Condition.create ()
+ let answers_queue = Queue.create ()
+ let queue_lock = Mutex.create ()
+ let queue_condition = Condition.create ()
(** Before calling this function queue_lock must be locked *)
-let treat_result () =
- let q_tmp = Queue.create () in
- while not (Queue.is_empty answers_queue) do
- Queue.transfer answers_queue q_tmp;
- Mutex.unlock queue_lock;
- let iter (result,callback) = decr scheduled_proofs; callback (result ()) in
- Queue.iter iter q_tmp;
- Queue.clear q_tmp;
- Mutex.lock queue_lock
- done
-
-let yield () =
- Thread.yield ();
- Mutex.lock queue_lock;
- treat_result ();
- Mutex.unlock queue_lock
-
-let new_external_proof =
- let run_external (call_prover,callback) =
- let r = Call_provers.wait_on_call (call_prover ()) in
+ let treat_result () =
+ let q_tmp = Queue.create () in
+ while not (Queue.is_empty answers_queue) do
+ Queue.transfer answers_queue q_tmp;
+ Mutex.unlock queue_lock;
+ let iter (result,callback) = decr scheduled_proofs; callback (result ())
+ in
+ Queue.iter iter q_tmp;
+ Queue.clear q_tmp;
+ Mutex.lock queue_lock
+ done
+
+ let yield () =
+ Thread.yield ();
+ Mutex.lock queue_lock;
+ treat_result ();
+ Mutex.unlock queue_lock
+
+ (** Wait for the last remaining tasks *)
+ let wait_remaining_task () =
Mutex.lock queue_lock;
- Queue.push (r,callback) answers_queue ;
- Condition.signal queue_condition;
- Mutex.unlock queue_lock in
- let external_workers =
- ManyWorkers.create maximum_running_proofs run_external in
- fun (call_prover,callback) ->
- ManyWorkers.add_work external_workers (call_prover,callback);
- incr scheduled_proofs;
+ while !scheduled_proofs > 0 do
+ while Queue.is_empty answers_queue do
+ Condition.wait queue_condition queue_lock
+ done;
+ treat_result ();
+ done;
+ Mutex.unlock queue_lock
+
+ let new_external_proof =
+ let run_external (call_prover,callback) =
+ let r = Call_provers.wait_on_call (call_prover ()) in
+ Mutex.lock queue_lock;
+ Queue.push (r,callback) answers_queue ;
+ Condition.signal queue_condition;
+ Mutex.unlock queue_lock in
+ let external_workers =
+ ManyWorkers.create maximum_running_proofs run_external in
+ fun (call_prover,callback) ->
+ ManyWorkers.add_work external_workers (call_prover,callback);
+ incr scheduled_proofs;
(** Stop the computation if too many external proof are scheduled *)
- while !scheduled_proofs >= !maximum_running_proofs * coef_buf do
+ while !scheduled_proofs >= !maximum_running_proofs * coef_buf do
Mutex.lock queue_lock;
while Queue.is_empty answers_queue do
Condition.wait queue_condition queue_lock
done;
treat_result ();
Mutex.unlock queue_lock;
- done
+ done
(* from Gmain *)
-let task_checksum t =
- fprintf str_formatter "%a@." Pretty.print_task t;
- let s = flush_str_formatter () in
- Digest.to_hex (Digest.string s)
-
-
-let apply_trans (task,db_goal) (trans,db_trans) =
- let task = Trans.apply trans task in
- match db_goal, db_trans with
- | Some db_goal, Some db_trans ->
- let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
- with Not_found ->
- Db.add_transformation db_goal db_trans
- in
- let md5 = task_checksum task in
- let db_goal =
- try
- Mstr.find md5 (Db.subgoals transf)
- with Not_found ->
- Db.add_subgoal transf
- (Task.task_goal task).Decl.pr_name.Ident.id_string
- md5
- in
- (task,Some db_goal)
- | _ -> ((task:task),None)
-
-let apply_transl (task,db_goal) (trans,db_trans) =
- let tasks = Trans.apply trans task in
- match db_goal, db_trans with
- | Some db_goal, Some db_trans ->
- let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
- with Not_found -> Db.add_transformation db_goal db_trans
- in
- let map task =
+ let task_checksum t =
+ fprintf str_formatter "%a@." Pretty.print_task t;
+ let s = flush_str_formatter () in
+ Digest.to_hex (Digest.string s)
+
+
+ let apply_trans (task,db_goal) (trans,db_trans) =
+ let task = Trans.apply trans task in
+ match db_goal, db_trans with
+ | Some db_goal, Some db_trans ->
+ let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
+ with Not_found ->
+ Db.add_transformation db_goal db_trans
+ in
let md5 = task_checksum task in
let db_goal =
try
@@ -209,18 +187,60 @@ let apply_transl (task,db_goal) (trans,db_trans) =
(Task.task_goal task).Decl.pr_name.Ident.id_string
md5
in
- (task,Some db_goal) in
- List.map map tasks
- | _ -> List.map (fun task -> (task:task),None) tasks
+ (task,Some db_goal)
+ | _ -> ((task:task),None)
+
+ let apply_transl (task,db_goal) (trans,db_trans) =
+ let tasks = Trans.apply trans task in
+ match db_goal, db_trans with
+ | Some db_goal, Some db_trans ->
+ let transf = try Db.Htransf.find (Db.transformations db_goal) db_trans
+ with Not_found -> Db.add_transformation db_goal db_trans
+ in
+ let map task =
+ let md5 = task_checksum task in
+ let db_goal =
+ try
+ Mstr.find md5 (Db.subgoals transf)
+ with Not_found ->
+ Db.add_subgoal transf
+ (Task.task_goal task).Decl.pr_name.Ident.id_string
+ md5
+ in
+ (task,Some db_goal) in
+ List.map map tasks
+ | _ -> List.map (fun task -> (task:task),None) tasks
+
+
+ let rec apply_transll trl acc (task,db_goal) =
+ match trl with
+ | [] -> (task,db_goal)::acc
+ | tr::trl ->
+ let tl = apply_transl (task,db_goal) tr in
+ List.fold_left (apply_transll trl) acc tl
+
+ let proof_status_to_db_result pr =
+ match pr with
+ | {pr_answer = Valid} -> (Db.Success,pr.pr_time)
+ | {pr_answer = Invalid} -> (Db.Unknown,pr.pr_time)
+ (* TODO add invalid in Db *)
+ | {pr_answer = Unknown _} -> (Db.Unknown,pr.pr_time)
+ | {pr_answer = Failure _ | HighFailure} -> (Db.Failure,pr.pr_time)
+ | {pr_answer = Timeout } -> (Db.Timeout,pr.pr_time)
+
+end
-let rec apply_transll trl acc (task,db_goal) =
- match trl with
- | [] -> (task,db_goal)::acc
- | tr::trl ->
- let tl = apply_transl (task,db_goal) tr in
- List.fold_left (apply_transll trl) acc tl
+let print_why_result fmt = function
+ | InternalFailure exn ->
+ Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
+ | Done (pr,_) -> BenchUtil.print_proof_status fmt pr
+
+let print_pas fmt = function
+ | Runned sp -> fprintf fmt "Runned %a" print_why_result sp
+ | Cached (p,t) -> fprintf fmt "Cached (%a,%f)"
+ BenchUtil.print_proof_status p t
let call callback tool prob =
(** Prove goal *)
@@ -230,7 +250,7 @@ let call callback tool prob =
let call_prover : Call_provers.pre_prover_call =
Driver.prove_task ~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
~command:(tool.tcommand) (tool.tdriver) task in
- new_external_proof (call_prover,cb)
+ BenchUtil.new_external_proof (call_prover,cb)
with e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
callback pval i task (Runned (InternalFailure e)) in
@@ -245,7 +265,7 @@ let call callback tool prob =
in
let (proof_status,time,_,_) = Db.status_and_time proof_attempt in
Debug.dprintf debug "Database has (%a,%f) for the goal@."
- print_prover_answer proof_status time;
+ BenchUtil.print_proof_status proof_status time;
begin
if proof_status = Db.Success ||
(proof_status = Db.Timeout && time > (float tool.ttime -. 0.1))
@@ -256,7 +276,7 @@ let call callback tool prob =
Debug.dprintf debug "@.time = %f %i@.@."
time tool.ttime;
let cb res =
- let (status,time) = proof_status_to_db_result res in
+ let (status,time) = BenchUtil.proof_status_to_db_result res in
callback pval i task (Runned (Done (status,time)));
Db.set_status proof_attempt status time
in
@@ -265,16 +285,18 @@ let call callback tool prob =
end
| _ ->
let cb res =
- let (status,time) = proof_status_to_db_result res in
+ let (status,time) = BenchUtil.proof_status_to_db_result res in
callback pval i task (Runned (Done (status,time))) in
new_external_proof pval i cb task
in
(** Apply trans *)
let iter_task (pval,task) =
let translist = prob.ptrans tool.tenv in
- let tasks = apply_transll translist [] (task,pval.prob_db) in
+ let tasks = BenchUtil.apply_transll translist [] (task,pval.prob_db) in
let tasks = List.map
- (fun task -> List.fold_left apply_trans task tool.ttrans) tasks in
+ (fun task -> List.fold_left BenchUtil.apply_trans task tool.ttrans)
+ tasks
+ in
let iter i task = call pval i task; succ i in
ignore (List.fold_left iter 0 (List.rev tasks)) in
(** Split *)
@@ -297,15 +319,7 @@ let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
| Cached (res,time) -> Done (res,time)
} in
call cb tool prob);
- (** Wait for the last remaining tasks *)
- Mutex.lock queue_lock;
- while !scheduled_proofs > 0 do
- while Queue.is_empty answers_queue do
- Condition.wait queue_condition queue_lock
- done;
- treat_result ();
- done;
- Mutex.unlock queue_lock
+ BenchUtil.wait_remaining_task ()
let any ?callback toolprob =
let l = ref [] in
@@ -498,7 +512,7 @@ answer output time
match r with
| Done (answer,time) ->
fprintf fmt "%a, %.3f" (*"%a, %S, %.3f"*)
- print_prover_answer answer (*r.result.pr_output*)
+ BenchUtil.print_proof_status answer (*r.result.pr_output*)
time
| InternalFailure _ -> fprintf fmt "InternalFailure, \"\""
in
diff --git a/src/bench/bench.mli b/src/bench/bench.mli
index bae52d48066051dc52407ee1c1200aa43e45e71b..8ce3d086fc8524ee3411ef87877a2221e8283a4e 100644
--- a/src/bench/bench.mli
+++ b/src/bench/bench.mli
@@ -26,11 +26,49 @@ open Driver
open Call_provers
open Scheduler
-
-val maximum_running_proofs: int ref
+module BenchUtil : sig
+ val maximum_running_proofs: int ref
(** bound on the number of prover processes running in parallel.
default is 2 *)
+ val new_external_proof :
+ Call_provers.pre_prover_call * (Call_provers.prover_result -> unit)
+ -> unit
+ (** [new_external_proof pre_prover_call callback] *)
+
+ val wait_remaining_task : unit -> unit
+ (** Wait the completion of the remaining task started by
+ new_external_proof *)
+
+ val task_checksum : Task.task -> string
+
+ val apply_trans :
+ task * Db.goal option ->
+ task trans * Db.transf_id option ->
+ task * Db.goal option
+ (** [apply_transl trans goal] *)
+
+ val apply_transl :
+ task * Db.goal option ->
+ task list trans * Db.transf_id option ->
+ (task * Db.goal option) list
+ (** [apply_transl transl goal] *)
+
+ val apply_transll :
+ (task list trans * Db.transf_id option) list ->
+ (task * Db.goal option) list ->
+ task * Db.goal option ->
+ (task * Db.goal option) list
+ (** [apply_transll transllist acc goal] *)
+
+ val proof_status_to_db_result :
+ Call_provers.prover_result -> Db.proof_status * float
+
+ val print_proof_status :
+ Format.formatter -> Db.proof_status -> unit
+
+end
+
type tool_id = {
tool_name : string;
prover_name : string;
@@ -82,8 +120,6 @@ type proof_attempt_status =
val print_pas : Format.formatter -> proof_attempt_status -> unit
-val task_checksum : Task.task -> string
-
type callback = tool_id -> prob_id ->
task -> int -> proof_attempt_status -> unit
diff --git a/src/bench/benchdb.ml b/src/bench/benchdb.ml
new file mode 100644
index 0000000000000000000000000000000000000000..356056c6906fcfa1c23f715dd00dd24b78edfaff
--- /dev/null
+++ b/src/bench/benchdb.ml
@@ -0,0 +1,141 @@
+(** run benchs from the database *)
+
+open Format
+open Why
+open Util
+module BenchUtil = Bench.BenchUtil
+
+let load_driver = Env.Wenv.memoize 2 (fun env ->
+ memo_string 10 (Driver.load_driver env))
+
+let debug = Debug.register_flag "benchdb"
+
+type path =
+ | Pgoal of string
+ | Ptrans of string
+
+let print_path fmt = function
+ | Pgoal s -> Format.fprintf fmt "the goal %s" s
+ | Ptrans s -> Format.fprintf fmt "the transformation %s" s
+
+let print_paths fmt (wf,thname,pathl) =
+ Format.fprintf fmt "%a of theory %s in file %s"
+ (Pp.print_list (fun fmt () -> fprintf fmt "@ of@ ") print_path) pathl
+ thname wf
+
+let concat_path p (wf,thname,pathl) = (wf,thname,p::pathl)
+
+let rec goal whyconf env path dbgoal wgoal =
+ (** external proof *)
+ let db_proofs = Db.external_proofs dbgoal in
+ let iter prover_id proof_attempt =
+ try
+ let (proof_status,time,obsolete,edited_as) =
+ Db.status_and_time proof_attempt in
+ if obsolete then () else
+ let prover_name = Db.prover_name prover_id in
+ let driver,command =
+ try
+ let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in
+ p.Whyconf.driver ,p.Whyconf.command
+ with
+ (* TODO add exceptions pehaps inside rc.ml in fact*)
+ | Not_found ->
+ Debug.dprintf debug "Error : Prover %s not found.@." prover_name;
+ raise Exit
+ in
+ let cb res =
+ let (res_status,_res_time) = BenchUtil.proof_status_to_db_result res in
+ if proof_status <> res_status then
+ printf "Diff : %a instead of %a in %a@."
+ BenchUtil.print_proof_status proof_status
+ BenchUtil.print_proof_status res_status
+ print_paths path
+ else
+ Debug.dprintf debug "Same : %a for %a@."
+ BenchUtil.print_proof_status proof_status
+ print_paths path
+ in
+ let old = if edited_as = "" then None else
+ begin
+ eprintf "Info: proving using edited file %s@." edited_as;
+ (Some (open_in edited_as))
+ end
+ in
+ let call_prover : Call_provers.pre_prover_call =
+ Driver.prove_task
+ ~timelimit:(truncate (ceil (time*.1.1)))
+ ~command (load_driver env driver) ?old wgoal in
+ BenchUtil.new_external_proof (call_prover,cb)
+ with Exit -> ()
+ in
+ Db.Hprover.iter iter db_proofs;
+ (** with transformations *)
+ let db_trans = Db.transformations dbgoal in
+ let iter dbtrans_id dbtrans =
+ let name = Db.transf_name dbtrans_id in
+ try
+ let wtransf = try Trans.singleton (Trans.lookup_transform name env)
+ with Trans.UnknownTrans _ -> Trans.lookup_transform_l name env
+ in
+ transf whyconf env (concat_path (Ptrans name) path) dbtrans wtransf wgoal
+ with Trans.UnknownTrans _ ->
+ Debug.dprintf debug "Error : Transformation %s not found.@." name
+ in
+ Db.Htransf.iter iter db_trans
+
+and transf whyconf env path dbtransf wtransf wgoal =
+ try
+ let wgoals = Trans.apply wtransf wgoal in
+ let dbgoals = Db.subgoals dbtransf in
+ let iter wgoal =
+ let checksum = BenchUtil.task_checksum wgoal in
+ try
+ let dbgoal = Mstr.find checksum dbgoals in
+ let gname = (Task.task_goal wgoal).Decl.pr_name.Ident.id_string in
+ goal whyconf env (concat_path (Pgoal gname) path) dbgoal wgoal
+ with Not_found ->
+ Debug.dprintf debug
+ "Error : Goal with checksum %s@ not found in@ %a.@."
+ checksum print_paths path
+ in
+ List.iter iter wgoals
+ with e ->
+ Debug.dprintf debug "Error : Execption %a@ in %a not found.@."
+ Exn_printer.exn_printer e print_paths path
+
+let theory whyconf env wf thname dbth wth =
+ let wgoals = Task.split_theory wth None None in
+ let dbgoals = Db.goals dbth in
+ let iter wgoal =
+ let gname = (Task.task_goal wgoal).Decl.pr_name.Ident.id_string in
+ try
+ let dbgoal = Mstr.find gname dbgoals in
+ goal whyconf env (wf,thname,[Pgoal gname]) dbgoal wgoal
+ with Not_found ->
+ Debug.dprintf debug
+ "Error : No sketch of proof for the goal %s of theory %s in file %s.@."
+ gname thname wf
+ in
+ List.iter iter wgoals
+
+let file whyconf env (dbf,wf) =
+ let wths = Env.read_file env
+ (Filename.concat (Filename.dirname (Db.db_name ())) wf) in
+ let dbths = Db.theories dbf in
+ let iter thname wth =
+ try
+ let dbth = Mstr.find thname dbths in
+ theory whyconf env wf thname dbth wth
+ with Not_found ->
+ Debug.dprintf debug
+ "Error : No sketch of proof for the theory %s of file %s.@."
+ thname wf
+ in
+ Theory.Mnm.iter iter wths
+
+
+let db whyconf env =
+ assert (Db.is_initialized ());
+ List.iter (file whyconf env) (Db.files ());
+ BenchUtil.wait_remaining_task ()
diff --git a/src/bench/benchdb.mli b/src/bench/benchdb.mli
new file mode 100644
index 0000000000000000000000000000000000000000..614d5e850c3b3f33761d407ad64723bef74ef90e
--- /dev/null
+++ b/src/bench/benchdb.mli
@@ -0,0 +1,5 @@
+(** run benchs from the database *)
+
+open Why
+
+val db : Whyconf.config -> Env.env -> unit
diff --git a/src/bench/benchrc.ml b/src/bench/benchrc.ml
index a510796f42fee566abfc2ffcc858e468c83f809b..708db33da0a819c88bf5024c877199845c571875 100644
--- a/src/bench/benchrc.ml
+++ b/src/bench/benchrc.ml
@@ -117,7 +117,7 @@ let apply_use_before_goal (task,goal_id) (th_use,th_use_id) =
with Not_found ->
Db.add_transformation goal_id th_use_id in
let name2 = (Task.task_goal task2).Decl.pr_name.Ident.id_string in
- let md5_2 = task_checksum task2 in
+ let md5_2 = BenchUtil.task_checksum task2 in
try Mstr.find md5_2 (Db.subgoals transf)
with Not_found ->
Db.add_subgoal transf name2 md5_2
@@ -154,7 +154,7 @@ let gen_from_file ~format ~prob_name ~file_path ~file_name env lth =
let name = (Task.task_goal task).Decl.pr_name.Ident.id_string in
try Mstr.find name (Db.goals theory_id)
with Not_found ->
- Db.add_goal theory_id name (task_checksum task)
+ Db.add_goal theory_id name (BenchUtil.task_checksum task)
) theory_id in
let (task,goal_id) = List.fold_left apply_use_before_goal
(task,goal_id) lth in
diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml
index 8db3a3df59de45dba0032f903613afd44aadee7a..2dbaa8812905189bf8ea2d7ccc18c9a1df92f534 100644
--- a/src/bench/whybench.ml
+++ b/src/bench/whybench.ml
@@ -103,6 +103,7 @@ let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_benchrc = ref []
let opt_db = ref None
+let opt_redo = ref false
let opt_print_theory = ref false
let opt_print_namespace = ref false
@@ -145,6 +146,8 @@ let option_list = Arg.align [
"<bench> Read one bench configuration file from <bench>";
"-d", Arg.String (fun s -> opt_db := Some s),
"<dir> the directory containing the database";
+ "--redo-db", Arg.Set opt_redo,
+ "Check that the proof attempts in the database (-d) give the same results";
"--prover", Arg.String (fun s -> opt_prover := s::!opt_prover),
" same as -P";
"-F", Arg.String (fun s -> opt_parser := Some s),
@@ -222,7 +225,7 @@ let () =
let main = get_main config in
Whyconf.load_plugins main;
- Bench.maximum_running_proofs := Whyconf.running_provers_max main;
+ Bench.BenchUtil.maximum_running_proofs := Whyconf.running_provers_max main;
(** listings*)
let opt_list = ref false in
@@ -318,9 +321,12 @@ let () =
Debug.dprintf debug "database loaded@."
end;
- if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue) then
+ if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue)
+ && (not !opt_redo)
+ then
begin
- eprintf "At least one bench is required or one prover and one file.@.";
+ eprintf "At least one bench is required or one prover and one file or
+ the verification of a database .@.";
Arg.usage option_list usage_msg;
exit 1
end;
@@ -337,6 +343,15 @@ let () =
!opt_metas) in
let env = Lexer.create_env !opt_loadpath in
+
+ if !opt_redo then
+ begin if not (Db.is_initialized ()) then
+ begin eprintf "--redo-db need the option -d";
+ exit 1 end;
+ Benchdb.db config env
+ end;
+
+
let map_prover s =
let prover = try Mstr.find s (get_provers config) with
| Not_found -> eprintf "Prover %s not found.@." s; exit 1
diff --git a/src/ide/db.ml b/src/ide/db.ml
index c60c7da09ab0b1e16ce800472989806b61d29ef7..0457f4cf7aa401ef596193d168068cf15f5adc5a 100644
--- a/src/ide/db.ml
+++ b/src/ide/db.ml
@@ -28,6 +28,7 @@ type handle = {
mutable in_transaction: int;
busyfn: Sqlite3.db -> unit;
mode: transaction_mode;
+ db_name : string;
}
let current_db = ref None
@@ -38,6 +39,8 @@ let current () =
| Some x -> x
let is_initialized () = !current_db <> None
+let db_name () = (current ()).db_name
+
let default_busyfn (_db:Sqlite3.db) =
prerr_endline "Db.default_busyfn WARNING: busy";
@@ -890,6 +893,7 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
in_transaction = 0;
mode = mode;
busyfn = busyfn;
+ db_name = db_name;
}
in
current_db := Some db;
@@ -934,6 +938,6 @@ let add_file f = Main.add (current()) f
(*
Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
+compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
End:
*)
diff --git a/src/ide/db.mli b/src/ide/db.mli
index c46a75fc23117d62b0ef89bcab370cee20c3a3a6..7abbd09401904e9341d3a0cb186483a72d417bc9 100644
--- a/src/ide/db.mli
+++ b/src/ide/db.mli
@@ -133,6 +133,9 @@ val is_initialized : unit -> bool
(** [is_initialized ()] is true if init_base as been called
succesively previously *)
+val db_name : unit -> string
+(** [db_name ()] return the path of the database *)
+
val files : unit -> (file * string) list
(** returns the current set of files, with their filenames *)
@@ -231,6 +234,6 @@ val add_file : string -> file
(*
Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
+compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
End:
*)
diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml
index 75ae833cc4fdd5963a03857f89b78cc832fbd949..3d53db9ffb1eb72811c8973c2e3c5100cf969c99 100644
--- a/src/ide/gmain.ml
+++ b/src/ide/gmain.ml
@@ -1331,65 +1331,6 @@ let filter_why_files () =
~name:"Why3 source files"
~patterns:[ "*.why"; "*.mlw"] ()
-(* return the absolute path of a given file name.
- this code has been designed to be architecture-independant so
- be very careful if you modify this *)
-let path_of_file f =
- let rec aux acc f =
-(*
- Format.printf "aux %s@." f;
- let _ = read_line () in
-*)
- let d = Filename.dirname f in
- if d = Filename.current_dir_name then
- (* f is relative to the current dir *)
- aux (f::acc) (Sys.getcwd ())
- else
- let b = Filename.basename f in
- if b=Filename.current_dir_name then acc else
- if f=b then b::acc else
- aux (b::acc) d
- in
- aux [] f
-
-(*
-let test x = (Filename.dirname x, Filename.basename x)
-
-let _ = test "file"
-let _ = test "/file"
-let _ = test "/"
-let _ = test "f1/f2"
-let _ = test "/f1/f2"
-
-let p1 = path_of_file "/bin/bash"
-
-let p1 = path_of_file "../src/f.why"
- *)
-
-let relativize_filename base f =
- let rec aux ab af =
- match ab,af with
- | x::rb, y::rf when x=y -> aux rb rf
- | _ ->
- let rec aux2 acc p =
- match p with
- | [] -> acc
- | _::rb -> aux2 (Filename.parent_dir_name::acc) rb
- in aux2 af ab
- in
- let rec rebuild l =
- match l with
- | [] -> ""
- | [x] -> x
- | x::l -> Filename.concat x (rebuild l)
- in
- rebuild (aux (path_of_file base) (path_of_file f))
-
-(*
-let p1 = relativize_filename "/bin/bash" "src/f.why"
-
-let p1 = relativize_filename "test" "/home/cmarche/recherche/why3/src/ide/f.why"
-*)
let select_file () =
let d = GWindow.file_chooser_dialog ~action:`OPEN
~title:"Why3: Add file in project"
@@ -1405,7 +1346,7 @@ let select_file () =
match d#filename with
| None -> ()
| Some f ->
- let f = relativize_filename project_dir f in
+ let f = Sysutil.relativize_filename project_dir f in
eprintf "Adding file '%s'@." f;
try
Helpers.add_file f
diff --git a/src/util/sysutil.ml b/src/util/sysutil.ml
index ba366d88a32c3f84b96b5b30c355fed6a5ab6e7e..153d2f6c5a734e3eba65559a8fbe162d0090c087 100644
--- a/src/util/sysutil.ml
+++ b/src/util/sysutil.ml
@@ -119,3 +119,63 @@ let copy_file from to_ =
while n := input cin buff 0 1024; !n <> 0 do
output cout buff 0 !n
done
+
+(* return the absolute path of a given file name.
+ this code has been designed to be architecture-independant so
+ be very careful if you modify this *)
+let path_of_file f =
+ let rec aux acc f =
+(*
+ Format.printf "aux %s@." f;
+ let _ = read_line () in
+*)
+ let d = Filename.dirname f in
+ if d = Filename.current_dir_name then
+ (* f is relative to the current dir *)
+ aux (f::acc) (Sys.getcwd ())
+ else
+ let b = Filename.basename f in
+ if b=Filename.current_dir_name then acc else
+ if f=b then b::acc else
+ aux (b::acc) d
+ in
+ aux [] f
+
+(*
+let test x = (Filename.dirname x, Filename.basename x)
+
+let _ = test "file"
+let _ = test "/file"
+let _ = test "/"
+let _ = test "f1/f2"
+let _ = test "/f1/f2"
+
+let p1 = path_of_file "/bin/bash"
+
+let p1 = path_of_file "../src/f.why"
+ *)
+
+let relativize_filename base f =
+ let rec aux ab af =
+ match ab,af with
+ | x::rb, y::rf when x=y -> aux rb rf
+ | _ ->
+ let rec aux2 acc p =
+ match p with
+ | [] -> acc
+ | _::rb -> aux2 (Filename.parent_dir_name::acc) rb
+ in aux2 af ab
+ in
+ let rec rebuild l =
+ match l with
+ | [] -> ""
+ | [x] -> x
+ | x::l -> Filename.concat x (rebuild l)
+ in
+ rebuild (aux (path_of_file base) (path_of_file f))
+
+(*
+let p1 = relativize_filename "/bin/bash" "src/f.why"
+
+let p1 = relativize_filename "test" "/home/cmarche/recherche/why3/src/ide/f.why"
+*)
diff --git a/src/util/sysutil.mli b/src/util/sysutil.mli
index a52b5eaa08924569b08e70c2b75a8b8f2fec8eff..8e3e93c95a405148972e14412f6a5baa7a3220be 100644
--- a/src/util/sysutil.mli
+++ b/src/util/sysutil.mli
@@ -61,3 +61,10 @@ val call_asynchronous : (unit -> 'a) -> (unit -> 'a)
val copy_file : string -> string -> unit
(** [copy_file from to] copy the file from [from] to [to] *)
+
+val path_of_file : string -> string list
+(** [path_of_file filename] return the absolute path of [filename] *)
+
+val relativize_filename : string -> string -> string
+(** [relativize_filename base filename] relativize the filename
+ [filename] according to [base] *)
diff --git a/src/util/util.ml b/src/util/util.ml
index d1a76b0a4fd12c0ac2e3cbae84b72866273e37bd..9adb7e7c179e48b2284239098939f2a3067aa664 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -224,3 +224,5 @@ let memo_int size f =
fun x -> try Hashtbl.find h x
with Not_found -> let y = f x in Hashtbl.add h x y; y
+let memo_string = memo_int
+
diff --git a/src/util/util.mli b/src/util/util.mli
index d5375bf0e1ded3305ab930289240272121b6a5be..206a01eff128ddb671928de592b61a2fc683c9e8 100644
--- a/src/util/util.mli
+++ b/src/util/util.mli
@@ -126,6 +126,7 @@ module Mstr : Map.S with type key = string
module Sstr : Mstr.Set
val memo_int : int -> (int -> 'a) -> int -> 'a
+val memo_string : int -> (string -> 'a) -> string -> 'a
(* Set, Map, Hashtbl on structures with a unique tag *)