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 49385a25 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

reimporting goals

parent ee1c1d38
......@@ -246,8 +246,6 @@ let subgoals t = t.subgoals
type theory = int64
let goals _ = assert false
let verified _ = assert false
type file = int64
......@@ -770,6 +768,30 @@ module Goal = struct
db_must_done db (fun () -> Sqlite3.step stmt);
Sqlite3.last_insert_rowid db.raw_db)
let name db g =
let sql="SELECT goal_name FROM goals \
WHERE goals.goal_id=?"
in
let stmt = bind db sql [Sqlite3.Data.INT g] in
let of_stmt stmt =
(stmt_column_string stmt 0 "Goal.name")
in
match step_fold db stmt of_stmt with
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
let of_theory db th =
let sql="SELECT goal_id FROM goals \
WHERE goals.goal_theory=?"
in
let stmt = bind db sql [Sqlite3.Data.INT th] in
let of_stmt stmt =
(stmt_column_INT stmt 0 "Goal.of_theory")
in
List.rev (step_fold db stmt of_stmt)
(*
let get_all_external_proofs db g =
let sql="SELECT map_goal_prover_external_proof.external_proof_id \
......@@ -858,6 +880,11 @@ module Goal = struct
end
let goal_name g = Goal.name (current()) g
let goals th = Goal.of_theory (current()) th
(*
let external_proofs g =
......@@ -1074,6 +1101,8 @@ end
let theory_name th = Theory.name (current()) th
let verified _ = assert false
let theories f = Theory.of_file (current()) f
module Main = struct
......
......@@ -86,6 +86,7 @@ val edited_as : proof_attempt -> string
(*
val parent : goal -> goal_parent
*)
val goal_name : goal -> string
val task_checksum : goal -> string (** checksum *)
val proved : goal -> bool
val external_proofs: goal -> proof_attempt Hprover.t
......
......@@ -378,6 +378,24 @@ module Helpers = struct
(image_of_result s);
if s = Scheduler.Success then set_proved a.proof_goal
let add_goal_row mth name t db_goal =
let parent = mth.theory_row in
let row = goals_model#append ~parent () in
let goal = { parent = Theory mth;
task = t ;
goal_row = row;
goal_db = db_goal;
external_proofs = Hashtbl.create 7;
transformations = [];
proved = false;
}
in
goals_model#set ~row ~column:name_column name;
goals_model#set ~row ~column:icon_column !image_file;
goals_model#set ~row ~column:index_column (Row_goal goal);
goals_model#set ~row ~column:visible_column true;
goal
let add_theory_row mfile th db_theory =
let tname = th.Theory.th_name.Ident.id_string in
let parent = mfile.file_row in
......@@ -400,28 +418,14 @@ module Helpers = struct
let tname = th.Theory.th_name.Ident.id_string in
let db_theory = Db.add_theory mfile.file_db tname in
let mth = add_theory_row mfile th db_theory in
let row = mth.theory_row in
let goals =
List.fold_left
(fun acc t ->
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let row = goals_model#append ~parent:row () in
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let sum = task_checksum t in
let db_goal = Db.add_goal db_theory name sum in
let goal = { parent = Theory mth;
task = t ;
goal_row = row;
goal_db = db_goal;
external_proofs = Hashtbl.create 7;
transformations = [];
proved = false;
}
in
goals_model#set ~row ~column:name_column name;
goals_model#set ~row ~column:icon_column !image_file;
goals_model#set ~row ~column:index_column (Row_goal goal);
goals_model#set ~row ~column:visible_column true;
let goal = add_goal_row mth name t db_goal in
goal :: acc
)
[]
......@@ -490,8 +494,26 @@ let () =
let tname = Db.theory_name db_th in
eprintf "Reimporting theory '%s'@."tname;
let th = Theory.Mnm.find tname theories in
let (_mth : Model.theory) = Helpers.add_theory_row mfile th db_th in
( (* TODO *) )
let mth = Helpers.add_theory_row mfile th db_th in
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
List.iter2
(fun db_goal t ->
let gname = Db.goal_name db_goal in
let taskname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
if gname <> taskname then
begin
eprintf "gname = %s, taskname = %s@." gname taskname;
assert false;
end;
let (_mg : Model.goal) =
Helpers.add_goal_row mth gname t db_goal
in
()
)
goals tasks
)
ths
)
......
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