Commit cefa4a01 authored by MARCHE Claude's avatar MARCHE Claude

external proofs in db

parent 50dbba85
......@@ -2,7 +2,7 @@
printer "coq"
filename "%f_%t_%g.v"
valid "Success"
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
......
......@@ -170,8 +170,10 @@ type goal = {
*)
mutable observers: (bool -> unit) list;
(** observers that wants to be notified by any changes of the proved status *)
(*
mutable external_proofs : external_proof list;
mutable transformations : transf list;
*)
}
and transf = {
......@@ -184,8 +186,6 @@ and transf = {
let goal_task g = g.task
let goal_task_checksum g = g.task_checksum
let external_proofs g = g.external_proofs
let transformations g = g.transformations
let goal_proved g = g.proved
let transf_data t = t.transf_data
......@@ -529,13 +529,13 @@ let status_from_int64 i =
module External_proof = struct
let init db =
let sql = "CREATE TABLE IF NOT EXISTS external_proof (id INTEGER PRIMARY KEY AUTOINCREMENT,prover INTEGER,timelimit INTEGER,memlimit INTEGER,status INTEGER,result_time REAL,trace TEXT,obsolete INTEGER);" in
let sql = "CREATE TABLE IF NOT EXISTS external_proof (external_proof_id INTEGER PRIMARY KEY AUTOINCREMENT,prover INTEGER,timelimit INTEGER,memlimit INTEGER,status INTEGER,result_time REAL,trace TEXT,obsolete INTEGER);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
let delete db e =
let id = e.external_proof_id in
assert (id <> 0L);
let sql = "DELETE FROM external_proof WHERE id=?" in
let sql = "DELETE FROM external_proof 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.INT id));
ignore(step_fold db stmt (fun _ -> ()));
......@@ -581,7 +581,7 @@ module External_proof = struct
(fun () ->
let id = e.external_proof_id in
let sql =
"UPDATE external_proof SET status=? WHERE id=?"
"UPDATE external_proof SET status=? WHERE external_proof_id=?"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
......@@ -592,7 +592,7 @@ module External_proof = struct
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.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
let stmt=Sqlite3.prepare db.raw_db sql in
db_must_ok db (fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.INT id));
......@@ -602,31 +602,31 @@ module External_proof = struct
prover =
(match Sqlite3.column stmt 0 with
| Sqlite3.Data.INT i -> i
| _ -> failwith "External_Proof.fromid: bad prover id");
| _ -> failwith "External_Proof.from_id: bad prover id");
timelimit =
(match Sqlite3.column stmt 1 with
| Sqlite3.Data.INT i -> Int64.to_int i
| _ -> failwith "External_Proof.fromid: bad timelimit");
| _ -> failwith "External_Proof.from_id: bad timelimit");
memlimit =
(match Sqlite3.column stmt 2 with
| Sqlite3.Data.INT i -> Int64.to_int i
| _ -> failwith "External_Proof.fromid: bad memlimit");
| _ -> failwith "External_Proof.from_id: bad memlimit");
status =
(match Sqlite3.column stmt 3 with
| Sqlite3.Data.INT i -> status_from_int64 i
| _ -> failwith "External_Proof.fromid: bad status");
| _ -> failwith "External_Proof.from_id: bad status");
result_time =
(match Sqlite3.column stmt 4 with
| Sqlite3.Data.FLOAT f -> f
| _ -> failwith "External_Proof.fromid: bad result_time");
| _ -> failwith "External_Proof.from_id: bad result_time");
trace =
(match Sqlite3.column stmt 5 with
| Sqlite3.Data.TEXT t -> t
| _ -> failwith "External_Proof.fromid: bad trace");
| _ -> failwith "External_Proof.from_id: bad trace");
proof_obsolete =
(match Sqlite3.column stmt 6 with
| Sqlite3.Data.INT i -> bool_from_int64 i
| _ -> failwith "External_Proof.fromid: bad proof_obsolete");
| _ -> failwith "External_Proof.from_id: bad proof_obsolete");
})
in
match l with
......@@ -635,6 +635,59 @@ module External_proof = struct
| _ -> assert false
let from_ids db idl =
let len = List.length idl in
if len = 0 then [] else
let sql = ref ")" in
for i=1 to len-1 do sql := ",?" ^ !sql done;
let sql="SELECT external_proof.external_proof_id,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 (?" ^ !sql
in
let stmt=Sqlite3.prepare db.raw_db sql in
let _ =
List.fold_left
(fun i id ->
db_must_ok db
(fun () -> Sqlite3.bind stmt i (Sqlite3.Data.INT id));
succ i)
1 idl
in
step_fold db stmt
(fun stmt ->
{ external_proof_id =
(match Sqlite3.column stmt 0 with
| Sqlite3.Data.INT i -> i
| _ -> failwith "External_Proof.from_ids: bad external_proof_id");
prover =
(match Sqlite3.column stmt 1 with
| Sqlite3.Data.INT i -> i
| _ -> failwith "External_Proof.fromids: bad prover id");
timelimit =
(match Sqlite3.column stmt 2 with
| Sqlite3.Data.INT i -> Int64.to_int i
| _ -> failwith "External_Proof.fromids: bad timelimit");
memlimit =
(match Sqlite3.column stmt 3 with
| Sqlite3.Data.INT i -> Int64.to_int i
| _ -> failwith "External_Proof.fromids: bad memlimit");
status =
(match Sqlite3.column stmt 4 with
| Sqlite3.Data.INT i -> status_from_int64 i
| _ -> failwith "External_Proof.fromids: bad status");
result_time =
(match Sqlite3.column stmt 5 with
| Sqlite3.Data.FLOAT f -> f
| _ -> failwith "External_Proof.fromids: bad result_time");
trace =
(match Sqlite3.column stmt 6 with
| Sqlite3.Data.TEXT t -> t
| _ -> failwith "External_Proof.fromids: bad trace");
proof_obsolete =
(match Sqlite3.column stmt 7 with
| Sqlite3.Data.INT i -> bool_from_int64 i
| _ -> failwith "External_Proof.fromids: bad proof_obsolete");
})
(* TODO: update functions for each field
let update db (e : external_proof) =
transaction db
......@@ -833,8 +886,6 @@ module Goal = struct
transaction db
(fun () ->
assert (g.goal_id = 0L);
assert (g.external_proofs = []);
assert (g.transformations = []);
let sql =
"INSERT INTO goal VALUES(NULL,?,?)"
in
......@@ -852,6 +903,19 @@ module Goal = struct
g.goal_id <- new_id)
let get_all_external_proofs db g =
let sql="SELECT map_goal_prover_external_proof.external_proof_id FROM map_goal_prover_external_proof 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 g.goal_id));
let l =
step_fold db stmt
(fun stmt ->
match Sqlite3.column stmt 0 with
| Sqlite3.Data.INT i -> i
| _ -> failwith "Db.get_all_external_proofs")
in External_proof.from_ids db l
let get_external_proof db ~prover g =
let sql="SELECT map_goal_prover_external_proof.external_proof_id FROM map_goal_prover_external_proof WHERE goal_id=? AND prover_id=?" in
let stmt = Sqlite3.prepare db.raw_db sql in
......@@ -1221,6 +1285,12 @@ module Goal = struct
end
let external_proofs g =
Goal.get_all_external_proofs (current ()) g
let transformations _g = assert false
module Transf = struct
......@@ -1466,9 +1536,11 @@ let try_prover ~debug ~timelimit ~memlimit ~prover ~command ~driver
if debug then Format.printf "setting attempt status to Scheduled@.";
External_proof.set_status db attempt Scheduled;
if debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
if debug then Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) g.task;
let callback =
try
if debug then
Format.eprintf "Task for prover: %a@."
(Why.Driver.print_task driver) g.task;
Why.Driver.prove_task ~debug ~command ~timelimit ~memlimit driver g.task
with
| Why.Driver.Error e ->
......@@ -1510,8 +1582,6 @@ let add_or_replace_task (name : Why.Decl.prsymbol) (t : Why.Task.task) : goal =
task_checksum = ""; (* TODO: md5sum (marshall ?) *)
proved = false;
observers = [];
external_proofs = [];
transformations = [];
}
in
Goal.add (current()) g;
......
......@@ -2,64 +2,19 @@
(** {1 Proof manager database} *)
(*
type handle
(** Database handle which can be used to create and retrieve objects *)
type transaction_mode = | Deferred | Immediate | Exclusive
val create :
?busyfn:(Sqlite3.db -> unit) -> ?mode:transaction_mode ->
string -> handle
(** [create db_name] opens a Sqlite3 database with filename
[db_name] and create any tables if they are missing.
@return a
database handle which can be used to create and retrieve objects in
the database. @raise Sql_error if a database error is
encountered *)
(*
val raw: handle -> Sqlite3.db
(** [raw db] @return the underlying Sqlite3 database for the
connection, for advanced queries. *)
*)
*)
(* {2 proof attempts and transformations} *)
(** {2 Current proof state} *)
(*
type db_ident (* = int64 *)
(** hidden type for record unique identifiers *)
*)
(*
type loc_record
*)
(*= private
{ mutable id : db_ident option;
(** when None, the record has never been stored in database yet *)
mutable file : string;
mutable line : int;
mutable start : int;
mutable stop : int;
}
*)
(** prover data *)
type prover
(** abstract type for the set of provers of the database *)
val prover_name : prover -> string
(** name of a prover *)
val get_prover : string -> prover
(** retrieves prover from its unique name. creates a new prover if
needed. *)
(** status of an external proof attempt *)
type proof_attempt_status =
......@@ -70,30 +25,37 @@ type proof_attempt_status =
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
val print_status : Format.formatter -> proof_attempt_status -> unit
type external_proof
(** abstract type for a proof attempt with an external prover *)
val prover : external_proof -> prover
(** the prover used for this attempt *)
val timelimit : external_proof -> int
(** the time limit chosen for this attempt *)
val memlimit : external_proof -> int
(** the memory limit chosen for this attempt *)
val status : external_proof -> proof_attempt_status
(** the current status for this attempt *)
val result_time : external_proof -> float
(** the time taken for this attempt. Only meaningfull for attempts
that are not Scheduled or Running. *)
val trace : external_proof -> string
val proof_obsolete : external_proof -> bool
(** a trace of execution of this attempt. Not used yet. *)
(*
type goal_origin =
| Goal of Decl.prsymbol
(*
| VCfun of loc * explain * ...
| Subgoal of goal
*)
*)
val proof_obsolete : external_proof -> bool
(** this attempt became obsolete because goal has changed. *)
type goal
(** abstract type for goals *)
val goal_proved : goal -> bool
val goal_name : goal -> string
(** module Goal to allow use of goals in Hashtables or Map or Set *)
module Goal : sig
type t = goal
......@@ -115,20 +77,29 @@ type transf
(** goal accessors *)
val goal_task : goal -> Why.Task.task
val goal_task_checksum: goal -> string
val goal_name : goal -> string
(** returns a goal's name, if any *)
(*
val parent : goal -> transf option
*)
(*
val goal_task : goal -> Why.Task.task
*)
val goal_task_checksum: goal -> string
val external_proofs : goal -> external_proof list
(** returns the set of external proof attempt for that goal *)
val transformations : goal -> transf list
val goal_proved : goal -> bool
(** [goal_proved g] returns true iff either
exists proof p in [external_proofs g] s.t.
(** tells if the goal is proved valid or not.
It returns true iff either
<li>exists proof p in [external_proofs g] s.t.
proof_obsolete p == false and status p = Valid
or
exists transf t in [transformations g] s.t.
<li>exists transf t in [transformations g] s.t.
transf_obsolete t == false and
forall g in [subgoals t], [goal_proved g]
*)
......
......@@ -229,6 +229,12 @@ let main_loop goals =
(fun (i,acc) g ->
let i = succ i in
printf "%2d: name='%s', proved=%b@." i (Db.goal_name g) (Db.goal_proved g);
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))
e;
(i,(i,g)::acc)) (0,[]) goals
in
printf "Select a choice:@.";
......
......@@ -9,7 +9,7 @@ driver = "drivers/alt_ergo.drv"
[prover coq]
name = "Coq"
command = "coqc %f && echo Success"
command = "coqc %f"
driver = "drivers/coq.drv"
[prover cvc3]
......
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