Commit 0b05b7a7 authored by MARCHE Claude's avatar MARCHE Claude

session files compressed further by factorizing timelimit,memlimit

parent 40109e4f
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -6,6 +6,8 @@
<!ATTLIST prover version CDATA #REQUIRED>
<!ATTLIST prover alternative CDATA #IMPLIED>
<!ATTLIST prover timelimit CDATA #IMPLIED>
<!ATTLIST prover memlimit CDATA #IMPLIED>
<!ELEMENT file (theory*)>
......@@ -449,11 +449,37 @@ let get_session_proof_attempt pa = get_session_goal pa.proof_parent
let get_used_provers session =
let sprover = ref Sprover.empty in
(fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
let get_used_provers_with_stats session =
let prover_table = PHprover.create 5 in
(fun pa ->
(* record mostly used pa.proof_timelimit pa.proof_memlimit *)
let prover = pa.proof_prover in
let timelimits,memlimits =
try PHprover.find prover_table prover
with Not_found ->
let x = (Hashtbl.create 5,Hashtbl.create 5) in
PHprover.add prover_table prover x;
let tf =
try Hashtbl.find timelimits pa.proof_timelimit
with Not_found -> 0
let mf =
try Hashtbl.find memlimits pa.proof_timelimit
with Not_found -> 0
Hashtbl.replace timelimits pa.proof_timelimit (tf+1);
Hashtbl.replace memlimits pa.proof_memlimit (mf+1))
exception NoTask
let goal_task g = Opt.get_exn NoTask g.goal_task
......@@ -482,7 +508,7 @@ let save_string fmt s =
let save_result fmt r =
fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
fprintf fmt "@\n<result@ status=\"%s\"@ time=\"%.2f\"/>"
(match r.Call_provers.pr_answer with
| Call_provers.Valid -> "valid"
| Call_provers.Failure _ -> "failure"
......@@ -500,7 +526,7 @@ let save_status fmt s =
| Scheduled | Running | Interrupted | JustEdited ->
fprintf fmt "@\n<undone/>"
| InternalFailure msg ->
fprintf fmt "@\n<internalfailure reason=\"%a\"/>"
fprintf fmt "@\n<internalfailure@ reason=\"%a\"/>"
save_string (Printexc.to_string msg)
| Done r -> save_result fmt r
......@@ -508,15 +534,20 @@ let save_status fmt s =
let save_bool_def name def fmt b =
if b <> def then fprintf fmt "@ %s=\"%b\"" name b
let save_int_def name def fmt n =
if n <> def then fprintf fmt "@ %s=\"%d\"" name n
let opt lab fmt = function
| None -> ()
| Some s -> fprintf fmt "@ %s=\"%a\"" lab save_string s
let save_proof_attempt fmt (id,a) =
let save_proof_attempt fmt ((id,tl,ml),a) =
fprintf fmt
"@\n@[<hov 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ memlimit=\"%d\"%a%a%a>"
id a.proof_timelimit a.proof_memlimit
(opt "edited") a.proof_edited_as
"@\n@[<hov 1><proof@ prover=\"%i\"%a%a%a%a%a>"
(save_int_def "timelimit" tl) a.proof_timelimit
(save_int_def "memlimit" ml) a.proof_memlimit
(opt "edited") a.proof_edited_as
(save_bool_def "obsolete" false) a.proof_obsolete
(save_bool_def "archived" false) a.proof_archived;
save_status fmt a.proof_state;
......@@ -524,6 +555,8 @@ let save_proof_attempt fmt (id,a) =
let save_ident fmt id =
fprintf fmt "name=\"%a\"" save_string id.Ident.id_string;
(* location info is useless, and takes a lot of place *)
match id.Ident.id_loc with
| None -> ()
| Some loc ->
......@@ -532,6 +565,8 @@ let save_ident fmt id =
fprintf fmt
"@ locfile=\"%a\"@ loclnum=\"%i\" loccnumb=\"%i\" loccnume=\"%i\""
save_string file lnum cnumb cnume
let save_label fmt s =
fprintf fmt "@\n@[<hov 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string
......@@ -549,7 +584,7 @@ let rec save_goal provers fmt g =
let l = PHprover.fold
(fun _ a acc -> (Mprover.find a.proof_prover provers, a) :: acc)
g.goal_external_proofs [] in
let l = List.sort (fun (i1,_) (i2,_) -> compare i1 i2) l in
let l = List.sort (fun ((i1,_,_),_) ((i2,_,_),_) -> compare i1 i2) l in
List.iter (save_proof_attempt fmt) l;
let l = PHstr.fold (fun _ t acc -> t :: acc) g.goal_transformations [] in
let l = List.sort (fun t1 t2 -> compare t1.transf_name t2.transf_name) l in
......@@ -559,14 +594,14 @@ let rec save_goal provers fmt g =
and save_trans provers fmt t =
fprintf fmt "@\n@[<hov 1><transf@ name=\"%a\"@ proved=\"%b\"%a>"
save_string t.transf_name t.transf_verified
save_string t.transf_name t.transf_verified
(save_bool_def "expanded" false) t.transf_expanded;
List.iter (save_goal provers fmt) t.transf_goals;
fprintf fmt "@]@\n</transf>"
and save_metas provers fmt _ m =
fprintf fmt "@\n@[<hov 1><metas@ proved=\"%b\"%a>"
(save_bool_def "expanded" false) m.metas_expanded;
let save_pos fmt pos =
fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
......@@ -632,7 +667,7 @@ let save_theory provers fmt t =
fprintf fmt
"@\n@[<hov 1><theory@ %a@ verified=\"%b\"%a>"
save_ident t.theory_name
(save_bool_def "expanded" false) t.theory_expanded;
Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
List.iter (save_goal provers fmt) t.theory_goals;
......@@ -646,20 +681,33 @@ let save_file provers fmt _ f =
List.iter (save_theory provers fmt) f.file_theories;
fprintf fmt "@]@\n</file>"
let save_prover fmt p (provers,id) =
fprintf fmt "@\n@[<hov 1><prover@ id=\"%i\"@ \
name=\"%a\"@ version=\"%a\"%a/>@]"
let save_prover fmt p (timelimits,memlimits) (provers,id) =
let mostfrequent_timelimit,_ =
(fun t f ((_,f') as t') -> if f > f' then (t,f) else t')
let mostfrequent_memlimit,_ =
(fun m f ((_,f') as m') -> if f > f' then (m,f) else m')
fprintf fmt "@\n@[<hov 1><prover@ id=\"%i\"@ name=\"%a\"@ \
version=\"%a\"%a@ timelimit=\"%d\"@ memlimit=\"%d\"/>@]"
id save_string p.C.prover_name save_string p.C.prover_version
(fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
save_string s)
Mprover.add p id provers, id+1
mostfrequent_timelimit mostfrequent_memlimit;
Mprover.add p (id,mostfrequent_timelimit,mostfrequent_memlimit) provers, id+1
let save fname _config session =
let ch = open_out fname in
let fmt = formatter_of_out_channel ch in
fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v2//EN\" \"\">@\n";
fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"\">@\n";
let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
......@@ -667,7 +715,7 @@ let save fname _config session =
fprintf fmt "@[<hov 1><why3session shape_version=\"%d\">"
let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session)
let provers,_ = PHprover.fold (save_prover fmt) (get_used_provers_with_stats session)
(Mprover.empty,0) in
PHstr.iter (save_file provers fmt) session.session_files;
fprintf fmt "@]@\n</why3session>";
......@@ -1066,10 +1114,8 @@ and load_proof_or_transf ~old_provers mg a =
match with
| "proof" ->
let prover = string_attribute "prover" a in
let p =
let p = Mstr.find prover old_provers in
let (p,timelimit,memlimit) =
try Mstr.find prover old_provers
with Not_found ->
eprintf "[Error] prover not listing in header '%s'@." prover;
raise (LoadError (a,"prover not listing in header"))
......@@ -1086,8 +1132,8 @@ and load_proof_or_transf ~old_provers mg a =
let edit = match edit with None | Some "" -> None | _ -> edit in
let obsolete = bool_attribute "obsolete" a false in
let archived = bool_attribute "archived" a false in
let timelimit = int_attribute_def "timelimit" a 2 in
let memlimit = int_attribute_def "memlimit" a 0 in
let timelimit = int_attribute_def "timelimit" a timelimit in
let memlimit = int_attribute_def "memlimit" a memlimit in
if timelimit < 0 then begin
eprintf "[Error] incorrect or unspecified timelimit '%i'@."
......@@ -1273,10 +1319,12 @@ let load_file session old_provers f =
let name = string_attribute "name" f in
let version = string_attribute "version" f in
let altern = string_attribute_def "alternative" f "" in
let timelimit = int_attribute_def "timelimit" f 5 in
let memlimit = int_attribute_def "memlimit" f 1000 in
let p = {C.prover_name = name;
prover_version = version;
prover_altern = altern} in
Mstr.add id p old_provers
Mstr.add id (p,timelimit,memlimit) old_provers
| s ->
eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
......@@ -51,10 +51,10 @@ let goal_expl_task ~root task =
(* Shapes *)
type shape = string
let print_shape = Format.pp_print_string
let string_of_shape x = x
let shape_of_string x = x
let equal_shape (x:string) y = x = y
let print_shape fmt s = Format.pp_print_string fmt (string_of_shape s)
let debug = Debug.register_info_flag "session_pairing"
~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
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