From 9d4e5566302f2b01b2dedff03f26101c384d4c10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 2 Nov 2011 17:43:45 +0100 Subject: [PATCH] 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. --- src/ide/html_session.ml | 12 ++++------- src/ide/session.ml | 7 ++++-- src/ide/session.mli | 4 ++++ src/ide/session_ro.ml | 48 +++++++++++++++++++++++++++-------------- src/ide/session_ro.mli | 17 ++++++++------- src/ide/stats.ml | 15 ++++++------- 6 files changed, 61 insertions(+), 42 deletions(-) diff --git a/src/ide/html_session.ml b/src/ide/html_session.ml index 672577f0c..3adf2275a 100644 --- a/src/ide/html_session.ml +++ b/src/ide/html_session.ml @@ -154,9 +154,7 @@ let run_file (context : context) print_session f = module Simple = struct - let print_prover fmt = function - | Detected_prover pd -> fprintf fmt "%s" pd.prover_name - | Undetected_prover s -> fprintf fmt "%s" s + let print_prover fmt pd = fprintf fmt "%s" pd.prover_name let print_proof_status fmt = function | Undone -> fprintf fmt "Undone" @@ -196,7 +194,7 @@ struct let print_session _name fmt s = fprintf fmt "" - (Pp.print_list Pp.newline print_file) s + (Pp.print_list Pp.newline print_file) s.files let context : context = " fprintf fmt "%s" pd.prover_name - | Undetected_prover s -> fprintf fmt "%s" s + let print_prover fmt pd = fprintf fmt "%s" pd.prover_name let print_proof_status fmt = function | Undone -> fprintf fmt "Undone" @@ -325,7 +321,7 @@ onclick=\"showedited('%s'); return false;\">%a : %a@]" let print_session_aux name fmt s = fprintf fmt "@[@]" name - (Pp.print_list Pp.newline print_file) s + (Pp.print_list Pp.newline print_file) s.files let print_session name fmt s = diff --git a/src/ide/session.ml b/src/ide/session.ml index 59095b986..0dcbab64e 100644 --- a/src/ide/session.ml +++ b/src/ide/session.ml @@ -1487,13 +1487,16 @@ available on this computer@." eprintf "[Warning] Session.load_file: unexpected element '%s'@." s; old_provers +let old_provers = ref Util.Mstr.empty +let get_old_provers () = !old_provers + let load_session ~env xml = let cont = xml.Xml.content in match cont.Xml.name with | "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 - in () | s -> eprintf "[Warning] Session.load_session: unexpected element '%s'@." s diff --git a/src/ide/session.mli b/src/ide/session.mli index a839fb8ee..5414a7ea9 100644 --- a/src/ide/session.mli +++ b/src/ide/session.mli @@ -210,6 +210,10 @@ module Make(O: OBSERVER) : sig *) 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 diff --git a/src/ide/session_ro.ml b/src/ide/session_ro.ml index 1c676abb0..2a46b01bb 100644 --- a/src/ide/session_ro.ml +++ b/src/ide/session_ro.ml @@ -25,7 +25,9 @@ open Util -type session = file list +type session = + { files : file list; + provers : prover_data Mstr.t} and file = { file_name : string; @@ -53,21 +55,17 @@ and transf = and prover_data = { prover_name : 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 = | Undone | Done of Call_provers.prover_result (** external proof done *) | InternalFailure of exn (** external proof aborted by internal error *) and proof_attempt = - { prover : prover_option; + { prover : prover_data; proof_state : proof_attempt_status; timelimit : int; proof_obsolete : bool; @@ -86,6 +84,16 @@ let read_config ?(includes=[]) conf_path_opt = {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 = struct type key = unit @@ -103,13 +111,16 @@ module Read_project (O : Session.OBSERVER) struct module M = Session.Make(Observer_dumb) - let read_prover_option = function - | M.Detected_prover pd -> Detected_prover - { prover_name = pd.Session.prover_name; - prover_version = pd.Session.prover_version; - prover_interactive = pd.Session.interactive; - } - | M.Undetected_prover s -> Undetected_prover s + let old_provers = ref Mstr.empty + + let get_prover_by_id pid = + try Mstr.find pid !old_provers + with Not_found -> assert false (** the provers must be an old_provers *) + + 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 | Session.Undone | Session.Scheduled | Session.Interrupted @@ -167,7 +178,12 @@ struct let _found_obs = M.open_session ~allow_obsolete ~env:env.env ~config:env.config ~init ~notify P.project_dir 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 diff --git a/src/ide/session_ro.mli b/src/ide/session_ro.mli index dd9355036..d7185f3e4 100644 --- a/src/ide/session_ro.mli +++ b/src/ide/session_ro.mli @@ -23,7 +23,9 @@ open Why3 open Util -type session = file list +type session = + { files : file list; + provers : prover_data Mstr.t} and file = private { file_name : string; @@ -51,21 +53,17 @@ and transf = private and prover_data = private { prover_name : 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 | Undone | Done of Call_provers.prover_result (** external proof done *) | InternalFailure of exn (** external proof aborted by internal error *) and proof_attempt = private - { prover : prover_option; + { prover : prover_data; proof_state : proof_attempt_status; timelimit : int; proof_obsolete : bool; @@ -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]. 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 : allow_obsolete:bool -> env:env -> string -> session diff --git a/src/ide/stats.ml b/src/ide/stats.ml index 5e270cc21..fda17e767 100644 --- a/src/ide/stats.ml +++ b/src/ide/stats.ml @@ -170,20 +170,19 @@ let stats_of_file stats file = let theories = file.theories in List.iter (stats_of_theory file stats) theories -let fill_prover_data stats = - let provers = Mstr.empty (* FIXME get_provers ()*) in +let fill_prover_data stats session = Mstr.iter (fun prover data -> Hashtbl.add stats.prover_data prover - (data.Session.prover_name ^ " " ^ data.Session.prover_version)) - provers + (data.prover_name ^ " " ^ data.prover_version)) + session.provers let extract_stats_from_file stats fname = let project_dir = get_project_dir fname in try - let file_list = read_project_dir ~allow_obsolete ~env project_dir in - fill_prover_data stats; - List.iter (stats_of_file stats) file_list + let session = read_project_dir ~allow_obsolete ~env project_dir in + fill_prover_data stats session; + List.iter (stats_of_file stats) session.files with e when not (Debug.test_flag Debug.stack_trace) -> eprintf "Error while opening session with database '%s' : %a@." project_dir Exn_printer.exn_printer e; @@ -198,7 +197,7 @@ let finalize_stats stats = stats.prover_avg_time let print_stats stats = - printf "== Provers used ==@\n @["; + printf "== Provers available ==@\n @["; Hashtbl.iter (fun prover data -> printf "%-10s: %s@\n" prover data) stats.prover_data; printf "@]@\n"; -- 2.24.1