Commit 2fe5755e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

comments

parent 120fd044
......@@ -120,8 +120,14 @@ let string_of_status = function
let print_status fmt s = Format.fprintf fmt "%s" (string_of_status s)
type prover =
{ prover_id : int64;
{ prover_id : db_ident;
prover_name : string;
(*
prover_short : string;
prover_long : string;
prover_command : string;
prover_driver_checksum : string;
*)
}
let prover_name p = p.prover_name
......@@ -300,11 +306,14 @@ let get_prover_from_id id =
let prover e = get_prover_from_id e.prover
let get_prover n =
let get_prover name (* ~short ~long ~command ~driver *) =
let db = current () in
try Prover.get db n
(*
let checksum = Digest.file driver in
*)
try Prover.get db name (* ~short ~long ~command ~checksum *)
with Not_found ->
Prover.add db n
Prover.add db name (* ~short ~long ~command ~checksum *)
......@@ -591,6 +600,20 @@ module External_proof = struct
(fun () -> Sqlite3.bind stmt 2 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt))
let set_result_time db e t =
transaction db
(fun () ->
let id = e.external_proof_id in
let sql =
"UPDATE external_proof SET result_time=? WHERE external_proof_id=?"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.FLOAT t));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt))
let from_id db id =
let sql="SELECT external_proof.prover, external_proof.timelimit, external_proof.memlimit, external_proof.status, external_proof.result_time, external_proof.trace, external_proof.obsolete FROM external_proof WHERE external_proof.external_proof_id=?"
in
......@@ -967,6 +990,21 @@ module Goal = struct
e
let set_proved db g b =
transaction db
(fun () ->
let id = g.goal_id in
let sql =
"UPDATE goal SET proved=? WHERE goal_id=?"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.INT (int64_from_bool b)));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt))
(* TODO make specific update functions for each field ! *)
(*
let update db (g : goal) =
......@@ -1546,28 +1584,37 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
| Why.Driver.Error e ->
Format.eprintf "Db.try_prover: prove_task reports %a@."
Why.Driver.report e;
raise Exit
fun () -> raise Exit
| e ->
try
Printexc.print (fun () -> raise e) ()
with _ -> raise Exit
with _ -> fun () -> raise Exit
in
fun () ->
if debug then Format.printf "setting attempt status to Running@.";
External_proof.set_status db attempt Running;
let r = callback () in
if debug then Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
match r.Why.Call_provers.pr_answer with
| Why.Call_provers.Valid ->
External_proof.set_status db attempt Success;
(* TODO: update "proved" status of goal and its parents *)
()
| Why.Call_provers.Timeout ->
External_proof.set_status db attempt Timeout
| Why.Call_provers.Invalid | Why.Call_provers.Unknown _ ->
External_proof.set_status db attempt Unknown
| Why.Call_provers.Failure _ | Why.Call_provers.HighFailure ->
External_proof.set_status db attempt HighFailure
try
let r = callback () in
if debug then Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
External_proof.set_result_time db attempt r.Why.Call_provers.pr_time;
match r.Why.Call_provers.pr_answer with
| Why.Call_provers.Valid ->
External_proof.set_status db attempt Success;
g.proved <- true;
Goal.set_proved db g true;
(* TODO: update "proved" status of goal parents if any *)
()
| Why.Call_provers.Timeout ->
External_proof.set_status db attempt Timeout
| Why.Call_provers.Invalid | Why.Call_provers.Unknown _ ->
External_proof.set_status db attempt Unknown
| Why.Call_provers.Failure _ | Why.Call_provers.HighFailure ->
External_proof.set_status db attempt HighFailure
with Exit ->
if debug then Format.eprintf "prover callback aborted because of an exception raised during elaboration@.";
External_proof.set_status db attempt HighFailure
let add_transformation (_g : goal) (_t : transf) : unit =
......@@ -1579,7 +1626,7 @@ let add_or_replace_task (name : Why.Decl.prsymbol) (t : Why.Task.task) : goal =
goal_id = 0L;
goal_origin = Goal name;
task = t;
task_checksum = ""; (* TODO: md5sum (marshall ?) *)
task_checksum = Digest.string (Marshal.to_string t []);
proved = false;
observers = [];
}
......
......@@ -3,6 +3,10 @@ open Format
open Why
open Whyconf
(******************************)
(* loading user configuration *)
(******************************)
(*
let autodetection () =
let alt_ergo = {
......@@ -58,6 +62,15 @@ let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.l
let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
let timelimit =
match config.timelimit with
| None -> 2
| Some n -> n
(********************)
(* opening database *)
(********************)
let fname = "tests/test-claude"
let () = Db.init_base (fname ^ ".db")
......@@ -73,7 +86,7 @@ type prover_data =
}
let provers_data =
printf "Provers: ";
printf "===============================@\nProvers: ";
let l =
Util.Mstr.fold
(fun id conf acc ->
......@@ -84,19 +97,17 @@ let provers_data =
driver = get_driver id; } :: acc
) config.provers []
in
printf "@.";
l
printf "@\n===============================@.";
l
let timelimit =
match config.timelimit with
| None -> 2
| Some n -> n
let () =
printf "previously known goals:@\n";
List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
printf "@."
(***********************)
(* Parsing input file *)
(***********************)
let rec report fmt = function
| Lexer.Error e ->
......@@ -129,7 +140,10 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
eprintf "%a@." report e;
exit 1
(***************************)
(* Process input theories *)
(* add corresponding tasks *)
(***************************)
let add_task (tname : string) (task : Why.Task.task) acc =
match task with
......@@ -146,61 +160,25 @@ let add_task (tname : string) (task : Why.Task.task) acc =
Db.add_or_replace_task name task :: acc
let do_theory tname th glist =
(*
let add acc (x,l) =
let pr = try Why.Theory.ns_find_pr th.Why.Theory.th_export l with Not_found ->
Format.eprintf "Goal '%s' not found in theory '%s'.@." x tname;
exit 1
in
Why.Decl.Spr.add pr acc
in
*)
(*
let prs = Some (Queue.fold add Why.Decl.Spr.empty glist) in
let prs = if Queue.is_empty glist then None else prs in
*)
let tasks = Why.Task.split_theory th None in
List.fold_right (add_task tname) tasks glist
(*
if !opt_prove then begin
let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in
printf "%s %s %s : %a@." fname tname
((task_goal task).Decl.pr_name).Ident.id_long
Call_provers.print_prover_result res
end else match !opt_output with
| None ->
printf "@[%a@]@?" (Driver.print_task drv) task
| Some dir ->
let file =
let file = Filename.basename fname in
try Filename.chop_extension file
with Invalid_argument _ -> file
in
let tname = th.th_name.Ident.id_short in
let dest = Driver.filename_of_goal drv file tname task in
(* Uniquify the filename before the extension if it exists*)
let i = try String.rindex dest '.' with _ -> String.length dest in
let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
let fmt = formatter_of_out_channel cout in
fprintf fmt "@[%a@]@?" (Driver.print_task drv) task;
close_out cout
*)
(***********************************)
(* back to the eighties: *)
(* A good-old text-based interface *)
(***********************************)
let goal_menu g =
try
while true do
printf "Menu:@.";
printf "Choose a prover:@.";
let _,menu = List.fold_left
(fun (i,acc) p ->
let i = succ i in
printf "%2d: try %s@." i (Db.prover_name p.prover);
(i,(i,p)::acc)) (0,[]) provers_data
in
printf "Select a choice:@.";
let s = read_line () in
(try
let i = try int_of_string s with Failure _ -> raise Not_found in
......@@ -223,7 +201,7 @@ let goal_menu g =
let main_loop goals =
try
while true do
printf "Menu:@.";
printf "======================@\nMenu:@.";
printf " 0: exit@.";
let _,menu = List.fold_left
(fun (i,acc) g ->
......@@ -232,12 +210,14 @@ let main_loop goals =
let e = Db.external_proofs g in
List.iter (fun e ->
let p = Db.prover e in
printf " external proof: prover=%s, result=%a@."
(Db.prover_name p) Db.print_status (Db.status e))
printf " external proof: prover=%s, obsolete=%b, result=%a, time=%f@."
(Db.prover_name p) (Db.proof_obsolete e)
Db.print_status (Db.status e)
(Db.result_time e))
e;
(i,(i,g)::acc)) (0,[]) goals
in
printf "Select a choice:@.";
let s = read_line () in
(try
let i = int_of_string s in
......@@ -248,11 +228,13 @@ let main_loop goals =
done
with Exit -> ()
(****************)
(* Main program *)
(****************)
let () =
eprintf "looking for goals@.";
(*
let glist = Queue.create () in
*)
let add_th t th mi =
eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi
......
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