Commit 9d4e5566 authored by François Bobot's avatar François Bobot

session_ro : Fix provers handling

- add the provers list which can be found in the session.
- remove Detected/Undetected since we use only the information
provided by the session, not which provers are currently available
on the current computer.
parent 02536d53
...@@ -154,9 +154,7 @@ let run_file (context : context) print_session f = ...@@ -154,9 +154,7 @@ let run_file (context : context) print_session f =
module Simple = module Simple =
struct struct
let print_prover fmt = function let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
| Detected_prover pd -> fprintf fmt "%s" pd.prover_name
| Undetected_prover s -> fprintf fmt "%s" s
let print_proof_status fmt = function let print_proof_status fmt = function
| Undone -> fprintf fmt "Undone" | Undone -> fprintf fmt "Undone"
...@@ -196,7 +194,7 @@ struct ...@@ -196,7 +194,7 @@ struct
let print_session _name fmt s = let print_session _name fmt s =
fprintf fmt "<ul>%a</ul>" fprintf fmt "<ul>%a</ul>"
(Pp.print_list Pp.newline print_file) s (Pp.print_list Pp.newline print_file) s.files
let context : context = "<!DOCTYPE html let context : context = "<!DOCTYPE html
...@@ -225,9 +223,7 @@ struct ...@@ -225,9 +223,7 @@ struct
then fprintf fmt "class='verified'" then fprintf fmt "class='verified'"
else fprintf fmt "class='notverified'" else fprintf fmt "class='notverified'"
let print_prover fmt = function let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
| Detected_prover pd -> fprintf fmt "%s" pd.prover_name
| Undetected_prover s -> fprintf fmt "%s" s
let print_proof_status fmt = function let print_proof_status fmt = function
| Undone -> fprintf fmt "<span class='notverified'>Undone</span>" | Undone -> fprintf fmt "<span class='notverified'>Undone</span>"
...@@ -325,7 +321,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]" ...@@ -325,7 +321,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
let print_session_aux name fmt s = let print_session_aux name fmt s =
fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]" fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
name name
(Pp.print_list Pp.newline print_file) s (Pp.print_list Pp.newline print_file) s.files
let print_session name fmt s = let print_session name fmt s =
......
...@@ -1487,13 +1487,16 @@ available on this computer@." ...@@ -1487,13 +1487,16 @@ available on this computer@."
eprintf "[Warning] Session.load_file: unexpected element '%s'@." s; eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
old_provers old_provers
let old_provers = ref Util.Mstr.empty
let get_old_provers () = !old_provers
let load_session ~env xml = let load_session ~env xml =
let cont = xml.Xml.content in let cont = xml.Xml.content in
match cont.Xml.name with match cont.Xml.name with
| "why3session" -> | "why3session" ->
let _old_provers = (** just to keep the old_provers somewhere *)
old_provers :=
List.fold_left (load_file ~env) Util.Mstr.empty cont.Xml.elements List.fold_left (load_file ~env) Util.Mstr.empty cont.Xml.elements
in ()
| s -> | s ->
eprintf "[Warning] Session.load_session: unexpected element '%s'@." s eprintf "[Warning] Session.load_session: unexpected element '%s'@." s
......
...@@ -210,6 +210,10 @@ module Make(O: OBSERVER) : sig ...@@ -210,6 +210,10 @@ module Make(O: OBSERVER) : sig
*) *)
val get_provers : unit -> prover_data Util.Mstr.t val get_provers : unit -> prover_data Util.Mstr.t
(** The provers on this computer *)
val get_old_provers : unit -> (string * string) Util.Mstr.t
(** The provers in this session (name * version ) *)
val maximum_running_proofs : int ref val maximum_running_proofs : int ref
......
...@@ -25,7 +25,9 @@ open Util ...@@ -25,7 +25,9 @@ open Util
type session = file list type session =
{ files : file list;
provers : prover_data Mstr.t}
and file = and file =
{ file_name : string; { file_name : string;
...@@ -53,21 +55,17 @@ and transf = ...@@ -53,21 +55,17 @@ and transf =
and prover_data = and prover_data =
{ prover_name : string; { prover_name : string;
prover_version : string; prover_version : string;
prover_interactive : bool; (** will be added again when session records it *)
(* prover_interactive : bool; *)
} }
and prover_option =
| Detected_prover of prover_data
| Undetected_prover of string
and proof_attempt_status = and proof_attempt_status =
| Undone | Undone
| Done of Call_provers.prover_result (** external proof done *) | Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *) | InternalFailure of exn (** external proof aborted by internal error *)
and proof_attempt = and proof_attempt =
{ prover : prover_option; { prover : prover_data;
proof_state : proof_attempt_status; proof_state : proof_attempt_status;
timelimit : int; timelimit : int;
proof_obsolete : bool; proof_obsolete : bool;
...@@ -86,6 +84,16 @@ let read_config ?(includes=[]) conf_path_opt = ...@@ -86,6 +84,16 @@ let read_config ?(includes=[]) conf_path_opt =
{env = env; config = config} {env = env; config = config}
let get_provers env =
let provers = Whyconf.get_provers env.config in
let get_prover_data pr =
{ prover_name = pr.Whyconf.name;
prover_version = pr.Whyconf.version;
(* prover_interactive = pr.Whyconf.interactive; *)
}
in
Mstr.map get_prover_data provers
module Observer_dumb : Session.OBSERVER = module Observer_dumb : Session.OBSERVER =
struct struct
type key = unit type key = unit
...@@ -103,13 +111,16 @@ module Read_project (O : Session.OBSERVER) ...@@ -103,13 +111,16 @@ module Read_project (O : Session.OBSERVER)
struct struct
module M = Session.Make(Observer_dumb) module M = Session.Make(Observer_dumb)
let read_prover_option = function let old_provers = ref Mstr.empty
| M.Detected_prover pd -> Detected_prover
{ prover_name = pd.Session.prover_name; let get_prover_by_id pid =
prover_version = pd.Session.prover_version; try Mstr.find pid !old_provers
prover_interactive = pd.Session.interactive; with Not_found -> assert false (** the provers must be an old_provers *)
}
| M.Undetected_prover s -> Undetected_prover s let read_prover_option po =
get_prover_by_id (match po with
| M.Detected_prover pd -> pd.Session.prover_id
| M.Undetected_prover s -> s)
let read_attempt_status = function let read_attempt_status = function
| Session.Undone | Session.Scheduled | Session.Interrupted | Session.Undone | Session.Scheduled | Session.Interrupted
...@@ -167,7 +178,12 @@ struct ...@@ -167,7 +178,12 @@ struct
let _found_obs = M.open_session ~allow_obsolete let _found_obs = M.open_session ~allow_obsolete
~env:env.env ~config:env.config ~init ~notify P.project_dir ~env:env.env ~config:env.config ~init ~notify P.project_dir
in in
List.map read_file (M.get_all_files ()) let prover_data (name,version) =
{ prover_name = name; prover_version = version} in
let op = Mstr.map prover_data (M.get_old_provers ()) in
old_provers := op;
{files = List.map read_file (M.get_all_files ());
provers = op}
end end
......
...@@ -23,7 +23,9 @@ ...@@ -23,7 +23,9 @@
open Why3 open Why3
open Util open Util
type session = file list type session =
{ files : file list;
provers : prover_data Mstr.t}
and file = private and file = private
{ file_name : string; { file_name : string;
...@@ -51,21 +53,17 @@ and transf = private ...@@ -51,21 +53,17 @@ and transf = private
and prover_data = private and prover_data = private
{ prover_name : string; { prover_name : string;
prover_version : string; prover_version : string;
prover_interactive : bool; (** will be added again when session records it *)
(* prover_interactive : bool; *)
} }
and prover_option = private
| Detected_prover of prover_data
| Undetected_prover of string
and proof_attempt_status = private and proof_attempt_status = private
| Undone | Undone
| Done of Call_provers.prover_result (** external proof done *) | Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *) | InternalFailure of exn (** external proof aborted by internal error *)
and proof_attempt = private and proof_attempt = private
{ prover : prover_option; { prover : prover_data;
proof_state : proof_attempt_status; proof_state : proof_attempt_status;
timelimit : int; timelimit : int;
proof_obsolete : bool; proof_obsolete : bool;
...@@ -82,6 +80,9 @@ val read_config : ?includes:string list -> string option -> env ...@@ -82,6 +80,9 @@ val read_config : ?includes:string list -> string option -> env
[conf_path] or use the default location if [conf_path] is [None]. [conf_path] or use the default location if [conf_path] is [None].
Add the directory in [includes] in the loadpath *) Add the directory in [includes] in the loadpath *)
val get_provers : env -> prover_data Util.Mstr.t
(** Get the provers on this computer *)
val read_project_dir : val read_project_dir :
allow_obsolete:bool -> allow_obsolete:bool ->
env:env -> string -> session env:env -> string -> session
......
...@@ -170,20 +170,19 @@ let stats_of_file stats file = ...@@ -170,20 +170,19 @@ let stats_of_file stats file =
let theories = file.theories in let theories = file.theories in
List.iter (stats_of_theory file stats) theories List.iter (stats_of_theory file stats) theories
let fill_prover_data stats = let fill_prover_data stats session =
let provers = Mstr.empty (* FIXME get_provers ()*) in
Mstr.iter Mstr.iter
(fun prover data -> (fun prover data ->
Hashtbl.add stats.prover_data prover Hashtbl.add stats.prover_data prover
(data.Session.prover_name ^ " " ^ data.Session.prover_version)) (data.prover_name ^ " " ^ data.prover_version))
provers session.provers
let extract_stats_from_file stats fname = let extract_stats_from_file stats fname =
let project_dir = get_project_dir fname in let project_dir = get_project_dir fname in
try try
let file_list = read_project_dir ~allow_obsolete ~env project_dir in let session = read_project_dir ~allow_obsolete ~env project_dir in
fill_prover_data stats; fill_prover_data stats session;
List.iter (stats_of_file stats) file_list List.iter (stats_of_file stats) session.files
with e when not (Debug.test_flag Debug.stack_trace) -> with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "Error while opening session with database '%s' : %a@." project_dir eprintf "Error while opening session with database '%s' : %a@." project_dir
Exn_printer.exn_printer e; Exn_printer.exn_printer e;
...@@ -198,7 +197,7 @@ let finalize_stats stats = ...@@ -198,7 +197,7 @@ let finalize_stats stats =
stats.prover_avg_time stats.prover_avg_time
let print_stats stats = let print_stats stats =
printf "== Provers used ==@\n @["; printf "== Provers available ==@\n @[";
Hashtbl.iter (fun prover data -> printf "%-10s: %s@\n" prover data) Hashtbl.iter (fun prover data -> printf "%-10s: %s@\n" prover data)
stats.prover_data; stats.prover_data;
printf "@]@\n"; printf "@]@\n";
......
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