Skip to content

GitLab

why3
why3
Commit a46bf955 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

external proofs data read from db

parent e81b1d02
Hide whitespace changes
Inline Side-by-side
Showing with 160 additions and 86 deletions
src/ide/db.ml
View file @ a46bf955
......@@ -106,6 +106,26 @@ let step_fold db stmt iterfn =
in
fn []
(* iterate over a result set *)
let step_iter db stmt iterfn =
let stepfn () = Sqlite3.step stmt in
let rec fn () = match db_busy_retry db stepfn with
| Sqlite3.Rc.ROW -> iterfn stmt; fn ()
| Sqlite3.Rc.DONE -> ()
| x -> raise_sql_error x
in
fn ()
(* iterate over a result set *)
let step_fold_gen db stmt iterfn start =
let stepfn () = Sqlite3.step stmt in
let rec fn a = match db_busy_retry db stepfn with
| Sqlite3.Rc.ROW -> fn (iterfn stmt a)
| Sqlite3.Rc.DONE -> a
| x -> raise_sql_error x
in
fn start
(* DB/SQL helpers *)
let bind db sql l =
......@@ -121,12 +141,12 @@ let stmt_column_INT stmt i msg =
| Sqlite3.Data.INT i -> i
| _ -> failwith msg
(*
let stmt_column_FLOAT stmt i msg =
match Sqlite3.column stmt i with
| Sqlite3.Data.FLOAT i -> i
| _ -> failwith msg
(*
let stmt_column_TEXT stmt i msg =
match Sqlite3.column stmt i with
| Sqlite3.Data.TEXT i -> i
......@@ -163,16 +183,15 @@ type prover_id =
prover_name : string;
}
let prover_name _p =
assert false
(* p.prover_name *)
let prover_name p = p.prover_name
module Hprover = Hashtbl.Make
(struct
type t = prover_id
let equal _p1 _p2 = assert false (* p1.prover_id == p2.prover_id *)
let hash _p = assert false (* Hashtbl.hash p.prover_id *)
let equal p1 p2 = p1.prover_id = p2.prover_id
let hash p = Hashtbl.hash p.prover_id
end)
type transf_id =
......@@ -214,9 +233,13 @@ type proof_attempt = int64
*)
let prover _p = assert false (* p.prover *)
(*
let status _p = assert false (* p.status *)
*)
let proof_obsolete _p = assert false (* p.proof_obsolete *)
(*
let time _p = assert false (* p.result_time *)
*)
let edited_as _p = assert false (* p.edited_as *)
type transf =
......@@ -240,7 +263,9 @@ and goal = int64
let task_checksum _g = assert false
let proved _g = assert false
(*
let external_proofs _g = Hprover.create 7 (* TODO !!! *)
*)
let transformations _g = assert false
......@@ -296,16 +321,16 @@ module ProverId = struct
prover_name = name }
)
let get db name =
let from_name db name =
let sql =
"SELECT prover.prover_id, prover.prover_name FROM prover \
"SELECT prover.prover_id FROM prover \
WHERE prover.prover_name=?"
in
let stmt = bind db sql [Sqlite3.Data.TEXT name] in
(* convert statement into record *)
let of_stmt stmt =
{ prover_id = stmt_column_INT stmt 0 "ProverId.get: bad prover id";
prover_name = stmt_column_string stmt 1 "ProverId.get: bad prover name";
prover_name = name;
}
in
(* execute the SQL query *)
......@@ -314,17 +339,16 @@ module ProverId = struct
| [x] -> x
| _ -> assert false
(*
let from_id db id =
let sql =
"SELECT prover.prover_id, prover.prover_name FROM prover \
"SELECT prover.prover_name FROM prover \
WHERE prover.prover_id=?"
in
let stmt = bind db sql [Sqlite3.Data.INT id] in
(* convert statement into record *)
let of_stmt stmt =
{ prover_id = Int64.to_int id ;
prover_name = stmt_column_string stmt 1
{ prover_id = id ;
prover_name = stmt_column_string stmt 0
"ProverId.from_id: bad prover_name";
}
in
......@@ -333,14 +357,12 @@ module ProverId = struct
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
*)
end
(*
let prover_memo = Hashtbl.create 7
let get_prover_from_id id =
let prover_from_id id =
try
Hashtbl.find prover_memo id
with Not_found ->
......@@ -352,6 +374,14 @@ let get_prover_from_id id =
Hashtbl.add prover_memo id p;
p
let prover_from_name n =
let db = current () in
try ProverId.from_name db n
with Not_found -> ProverId.add db n
(*
let prover e = get_prover_from_id e.prover
let get_prover name (* ~short ~long ~command ~driver *) =
......@@ -559,8 +589,9 @@ module External_proof = struct
let sql =
(* timelimit INTEGER, memlimit INTEGER,
edited_as TEXT, obsolete INTEGER *)
"CREATE TABLE IF NOT EXISTS external_proof \
(external_proof_id INTEGER,\
"CREATE TABLE IF NOT EXISTS external_proofs \
(external_proof_id INTEGER PRIMARY KEY AUTOINCREMENT,\
goal_id INTEGER,\
prover_id INTEGER, \
status INTEGER,\
time REAL);"
......@@ -571,7 +602,7 @@ module External_proof = struct
let delete db e =
let id = e.external_proof_id in
assert (id <> 0L);
let sql = "DELETE FROM external_proof WHERE external_proof_id=?" in
let sql = "DELETE FROM external_proofs WHERE external_proof_id=?" in
let stmt = bind db sql [ Sqlite3.Data.INT id ] in
ignore(step_fold db stmt (fun _ -> ()));
e.external_proof_id <- 0L
......@@ -580,7 +611,7 @@ module External_proof = struct
let add db (g : goal) (p: prover_id) =
transaction db
(fun () ->
let sql = "INSERT INTO external_proof VALUES(?,?,0,0.0)" in
let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0.0)" in
let stmt = bind db sql [
Sqlite3.Data.INT g;
Sqlite3.Data.INT p.prover_id;
......@@ -602,22 +633,48 @@ module External_proof = struct
Sqlite3.last_insert_rowid db.raw_db)
let set_status db e stat time =
try
transaction db
(fun () ->
let sql =
"UPDATE external_proof SET status=?,time=? WHERE external_proof_id=?"
in
let stmt = bind db sql [
Sqlite3.Data.INT (int64_from_status stat);
Sqlite3.Data.FLOAT time;
Sqlite3.Data.INT e;
]
in
db_must_done db (fun () -> Sqlite3.step stmt))
with e ->
Format.eprintf "External_proof.set_status raised an exception %s@."
(Printexc.to_string e)
transaction db
(fun () ->
let sql =
"UPDATE external_proofs SET status=?,time=? WHERE external_proof_id=?"
in
let stmt = bind db sql [
Sqlite3.Data.INT (int64_from_status stat);
Sqlite3.Data.FLOAT time;
Sqlite3.Data.INT e;
]
in
db_must_done db (fun () -> Sqlite3.step stmt))
let of_goal db g =
let sql="SELECT prover_id,external_proof_id FROM external_proofs \
WHERE external_proofs.goal_id=?"
in
let stmt = bind db sql [Sqlite3.Data.INT g] in
let res = Hprover.create 7 in
let of_stmt stmt =
let pid = stmt_column_INT stmt 0 "External_proof.of_goal" in
let a = stmt_column_INT stmt 1 "External_proof.of_goal" in
Hprover.add res (prover_from_id pid) a
in
step_iter db stmt of_stmt;
res
let status_and_time db p =
let sql="SELECT status,time FROM external_proofs \
WHERE external_proofs.external_proof_id=?"
in
let stmt = bind db sql [Sqlite3.Data.INT p] in
let of_stmt stmt =
let status = stmt_column_INT stmt 0 "External_proof.status_and_time" in
let t = stmt_column_FLOAT stmt 1 "External_proof.status_and_time" in
(status_from_int64 status, t)
in
match step_fold db stmt of_stmt with
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
(*
let set_result_time db e t =
......@@ -727,7 +784,9 @@ module External_proof = struct
*)
end
let status_and_time p = External_proof.status_and_time (current()) p
let external_proofs g = External_proof.of_goal (current()) g
module Goal = struct
......@@ -1195,12 +1254,6 @@ let root_goals () =
let files () =
Main.all_files (current())
let prover_from_name n =
let db = current () in
try ProverId.get db n
with Not_found -> ProverId.add db n
let transf_from_name _n = assert false
exception AlreadyExist
......
src/ide/db.mli
View file @ a46bf955
......@@ -78,9 +78,8 @@ val prover : proof_attempt -> prover_id
(*
val proof_goal : proof_attempt -> goal
*)
val status : proof_attempt -> proof_status
val status_and_time : proof_attempt -> proof_status * float
val proof_obsolete : proof_attempt -> bool
val time : proof_attempt -> float
val edited_as : proof_attempt -> string
(** goal accessors *)
......
src/ide/gconfig.ml
View file @ a46bf955
......@@ -25,7 +25,7 @@ type t =
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
mutable provers : prover_data list;
mutable provers : prover_data Util.Mstr.t;
mutable default_editor : string;
mutable env : Env.env;
mutable config : Whyconf.config;
......@@ -69,14 +69,16 @@ let load_ide section =
let get_prover_data env id pr acc =
try
let dr = Driver.load_driver env pr.Whyconf.driver in
{ prover_id = id ;
Mstr.add id
{ prover_id = id ;
prover_name = pr.Whyconf.name;
prover_version = pr.Whyconf.version;
command = pr.Whyconf.command;
driver_name = pr.Whyconf.driver;
driver = dr;
editor = pr.Whyconf.editor;
}::acc
}
acc
with _e ->
eprintf "Failed to load driver %s for prover %s. prover disabled@."
pr.Whyconf.driver pr.Whyconf.name;
......@@ -106,7 +108,7 @@ let load_config config =
(*
provers = Mstr.fold (get_prover_data env) provers [];
*)
provers = [];
provers = Mstr.empty;
default_editor = ide.ide_default_editor;
config = config;
env = env
......@@ -118,7 +120,7 @@ let read_config () =
let save_config t =
let save_prover acc pr =
let save_prover _ pr acc =
Mstr.add pr.prover_id
{
Whyconf.name = pr.prover_name;
......@@ -143,7 +145,7 @@ let save_config t =
let ide = set_string ide "default_editor" t.default_editor in
let config = set_section config "ide" ide in
let config = set_provers config
(List.fold_left save_prover Mstr.empty t.provers) in
(Mstr.fold save_prover t.provers Mstr.empty) in
save_config config
let config =
......@@ -347,7 +349,7 @@ let run_auto_detection gconfig =
let config = Autodetection.run_auto_detection gconfig.config in
gconfig.config <- config;
let provers = get_provers config in
gconfig.provers <- Mstr.fold (get_prover_data gconfig.env) provers [];
gconfig.provers <- Mstr.fold (get_prover_data gconfig.env) provers Mstr.empty;
(*
Local Variables:
......
src/ide/gconfig.mli
View file @ a46bf955
......@@ -20,19 +20,19 @@ type t =
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
mutable provers : prover_data list;
mutable provers : prover_data Util.Mstr.t;
mutable default_editor : string;
mutable env : Why.Env.env;
mutable config : Whyconf.config;
}
val get_prover_data : Why.Env.env ->
string ->
Why.Whyconf.config_prover -> prover_data list -> prover_data list
val get_prover_data : Why.Env.env -> string ->
Why.Whyconf.config_prover ->
prover_data Why.Util.Mstr.t -> prover_data Why.Util.Mstr.t
val save_config : unit -> unit
val config : t
val config : t
val get_main : unit -> Whyconf.main
......
src/ide/gdbmain.ml
View file @ a46bf955
......@@ -84,9 +84,11 @@ let gconfig =
let loadpath = (get_main ()).loadpath @ List.rev !includes in
c.env <- Env.create_env (Lexer.retrieve loadpath);
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <- Util.Mstr.fold (Gconfig.get_prover_data c.env) provers [];
c.provers <-
Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
c
(********************)
(* opening database *)
(********************)
......@@ -372,15 +374,22 @@ module Helpers = struct
set_proved t.parent_goal;
end
let set_proof_status a s =
let set_proof_status a s time =
a.status <- s;
let row = a.proof_row in
goals_model#set ~row ~column:status_column
(image_of_result s);
goals_model#set ~row ~column:status_column (image_of_result s);
let t = if time > 0.0 then
begin
a.Model.time <- time;
Format.sprintf "%.2f" time
end
else ""
in
goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t;
if s = Scheduler.Success then set_proved a.proof_goal
let add_external_proof_row g p db_proof =
let add_external_proof_row g p db_proof status time =
let parent = g.goal_row in
let name = p.prover_name in
let row = goals_model#prepend ~parent () in
......@@ -393,16 +402,16 @@ module Helpers = struct
proof_goal = g;
proof_row = row;
proof_db = db_proof;
status = Scheduler.Scheduled;
status = status;
proof_obsolete = false;
time = 0.0;
time = time;
output = "";
edited_as = "";
}
in
goals_model#set ~row ~column:index_column
(Row_proof_attempt a);
goals_model#set ~row ~column:index_column (Row_proof_attempt a);
Hashtbl.add g.external_proofs p.prover_id a;
set_proof_status a status time;
a
......@@ -541,9 +550,28 @@ let () =
eprintf "gname = %s, taskname = %s@." gname taskname;
assert false;
end;
let _goal = Helpers.add_goal_row mth gname t db_goal in
let _external_proofs = Db.external_proofs db_goal in
()
let goal = Helpers.add_goal_row mth gname t db_goal in
let external_proofs = Db.external_proofs db_goal in
Db.Hprover.iter
(fun pid a ->
let p =
Util.Mstr.find (Db.prover_name pid) gconfig.provers
in
let s,t = Db.status_and_time a in
eprintf "time = %f@." t;
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success -> Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
in
let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row goal p a s t
in
((* TODO *))
)
external_proofs
)
goals tasks
)
......@@ -573,7 +601,7 @@ let redo_external_proof g a =
let p = a.Model.prover in
let callback result time output =
a.Model.output <- output;
Helpers.set_proof_status a result;
Helpers.set_proof_status a result time;
let db_res = match result with
| Scheduler.Scheduled | Scheduler.Running -> Db.Undone
| Scheduler.Success -> Db.Success
......@@ -581,15 +609,7 @@ let redo_external_proof g a =
| Scheduler.Timeout -> Db.Timeout
| Scheduler.HighFailure -> Db.Failure
in
let t = if time > 0.0 then
begin
Db.set_status a.Model.proof_db db_res time;
a.Model.time <- time;
Format.sprintf "%.2f" time
end
else ""
in
goals_model#set ~row:a.Model.proof_row ~column:Model.time_column t
Db.set_status a.Model.proof_db db_res time
in
callback Scheduler.Scheduled 0.0 "";
let old = if a.Model.edited_as = "" then None else
......@@ -608,7 +628,7 @@ let rec prover_on_goal p g =
with Not_found ->
let db_prover = Db.prover_from_name id in
let db_pa = Db.add_proof_attempt g.Model.goal_db db_prover in
Helpers.add_external_proof_row g p db_pa
Helpers.add_external_proof_row g p db_pa Scheduler.Scheduled 0.0
in
redo_external_proof g a;
List.iter
......@@ -923,8 +943,8 @@ let () = add_refresh_provers (fun () ->
let () =
let add_item_provers () =
List.iter
(fun p ->
Util.Mstr.iter
(fun _ p ->
let n = p.prover_name ^ " " ^ p.prover_version in
(*
let (_ : GMenu.image_menu_item) =
......@@ -1157,9 +1177,9 @@ let edit_selected_row p =
let file = Driver.file_of_task driver fname "" t in
a.Model.edited_as <- file;
let old_status = a.Model.status in
Helpers.set_proof_status a Scheduler.Running;
Helpers.set_proof_status a Scheduler.Running 0.0;
let callback () =
Helpers.set_proof_status a old_status;
Helpers.set_proof_status a old_status 0.0;
in
let editor =
match a.Model.prover.editor with
......
src/ide/gmain.ml
View file @ a46bf955
......@@ -88,7 +88,7 @@ let gconfig =
let loadpath = (get_main ()).loadpath @ List.rev !includes in
c.env <- Env.create_env (Lexer.retrieve loadpath);
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <- Util.Mstr.fold (Gconfig.get_prover_data c.env) provers [];
c.provers <- Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
c
(***********************)
......@@ -708,8 +708,8 @@ let () = add_refresh_provers (fun () ->
let () =
let add_item_provers () =
List.iter
(fun p ->
Util.Mstr.iter
(fun _ p ->
let n = p.prover_name ^ " " ^ p.prover_version in
let (_ : GMenu.image_menu_item) =
tools_factory#add_image_item ~label:(n ^ " on all unproved goals")
......
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