Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit ed7b1e27 authored by François Bobot's avatar François Bobot
Browse files

whybench : More integration but the -d is still doing nothing

parent 4922dbf0
......@@ -134,13 +134,41 @@ let new_external_proof =
done
let apply_trans (task,_db_goal) (trans,_db_trans) =
let task = Trans.apply trans task in
((task:task),None)
(* from Gmain *)
let task_checksum t =
Format.fprintf Format.str_formatter "%a@." Pretty.print_task t;
let s = Format.flush_str_formatter () in
Digest.to_hex (Digest.string s)
let apply_transl (task,_db_goal) (trans,_db_trans) =
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.add_transformation db_goal db_trans
with Db.AlreadyExist ->
Db.Htransf.find (Db.transformations db_goal) db_trans in
let db_goal = Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
(task_checksum task) in
(task,Some db_goal)
| _ -> ((task:task),None)
let apply_transl (task,db_goal) (trans,db_trans) =
let tasks = Trans.apply trans task in
List.map (fun task -> (task:task),None) tasks
match db_goal, db_trans with
| Some db_goal, Some db_trans ->
let transf = try Db.add_transformation db_goal db_trans
with Db.AlreadyExist ->
Db.Htransf.find (Db.transformations db_goal) db_trans in
let map task =
let db_goal = Db.add_subgoal transf
(Task.task_goal task).Decl.pr_name.Ident.id_string
(task_checksum task) 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
......@@ -152,16 +180,42 @@ let rec apply_transll trl acc (task,db_goal) =
let call callback tool prob =
(** Prove goal *)
let call pval i task =
let cb res = callback pval i task (Done res) in
try
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)
with e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
callback pval i task (InternalFailure e)
let db_tool = tool.tval.tool_db in
let new_external_proof pval i cb task =
try
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)
with e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
callback pval i task (InternalFailure e) in
let call pval i (task,db_goal) =
match db_goal,db_tool with
| Some db_goal, Some db_tool ->
let proof_attempt =
try
Db.add_proof_attempt db_goal db_tool
with Db.AlreadyExist ->
Db.Hprover.find (Db.external_proofs db_goal) db_tool in
let (proof_status,_,_,_) = Db.status_and_time proof_attempt in
begin match proof_status with
| Db.Success -> () (*TODO something else, must use the callback *)
| Db.Timeout | Db.Unknown | Db.Failure | Db.Undone ->
let cb res = callback pval i task (Done res);
let status = match res.pr_answer with
| Valid -> Db.Success
| Timeout -> Db.Timeout
| Unknown _ -> Db.Unknown
| Failure _ | HighFailure -> Db.Failure
| Invalid -> Db.Failure (* Todo change that one day *) in
Db.set_status proof_attempt status res.pr_time
in
new_external_proof pval i cb task
end
| _ ->
let cb res = callback pval i task (Done res) in
new_external_proof pval i cb task
in
(** Apply trans *)
let iter_task (pval,task) =
......@@ -169,7 +223,7 @@ let call callback tool prob =
let tasks = apply_transll translist [] (task,pval.prob_db) in
let tasks = List.map
(fun task -> List.fold_left apply_trans task tool.ttrans) tasks in
let iter i (task,_db_goal) = call pval i task; succ i in
let iter i task = call pval i task; succ i in
ignore (List.fold_left iter 0 (List.rev tasks)) in
(** Split *)
let ths = prob.ptask tool.tenv tool.tuse in
......
......@@ -103,6 +103,7 @@ let opt_timelimit = ref None
let opt_memlimit = ref None
let opt_task = ref None
let opt_benchrc = ref []
let opt_db = ref None
let opt_print_theory = ref false
let opt_print_namespace = ref false
......@@ -143,6 +144,8 @@ let option_list = Arg.align [
"<prover> Add <prover> in the bench";
"-B", Arg.String (fun s -> opt_benchrc := s::!opt_benchrc),
"<bench> Read one bench configuration file from <bench>";
"-d", Arg.String (fun s -> opt_db := Some s),
"<dir> the directory containing the database";
"--prover", Arg.String (fun s -> opt_prover := s::!opt_prover),
" same as -P";
"-F", Arg.String (fun s -> opt_parser := Some s),
......@@ -289,6 +292,29 @@ let () =
(* exit 1 *)
(* end; *)
begin match !opt_db with
| None -> ()
| Some db ->
if Sys.file_exists db then
begin if not (Sys.is_directory db) then
eprintf "-d %s; the given database should be a directory" db;
exit 1
end
else
begin
eprintf "Info: '%s' does not exists. Creating directory of that \
name for the project@." db;
Unix.mkdir db 0o777
end;
let dbfname = Filename.concat db "project.db" in
try
Db.init_base dbfname
with e ->
eprintf "Error while opening database '%s'@." dbfname;
eprintf "Aborting...@.";
raise e
end;
if !opt_benchrc = [] && (!opt_prover = [] || Queue.is_empty opt_queue) then
begin
eprintf "At least one bench is required or one prover and one file.@.";
......
......@@ -37,6 +37,7 @@ let current () =
| None -> failwith "Db.current: database not yet initialized"
| Some x -> x
let is_initialized () = !current_db <> None
let default_busyfn (_db:Sqlite3.db) =
prerr_endline "Db.default_busyfn WARNING: busy";
......
......@@ -127,6 +127,10 @@ val theories : file -> theory Util.Mstr.t
val init_base : string -> unit
(** opens or creates the current database, from given file name *)
val is_initialized : unit -> bool
(** [is_initialized ()] is true if init_base as been called
succesively previously *)
val files : unit -> (file * string) list
(** returns the current set of files, with their filenames *)
......
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