Commit 2e2e0d83 authored by François Bobot's avatar François Bobot

Session doesn't use anymore prover id.

Prover ids are only used for the command line option "-P".
The user can choose what he wants (they must be unique)
The prover name and version should not be modified. If someone want to
test different command line options for a prover he can use the
"alternative" field.

If someone want to replay an external proof but he doesn't have the
corresponding prover (same name,version,alternative), why3ide ask for
a replacement among the known provers. The choice can be saved.
parent ac98a7a4
......@@ -28,6 +28,10 @@ s
is not changed by a transformation, it will stay in the hash table forever,
since the key is the value. Should we use generation numbers in arguments
and results of transformations?
François -- I don't get that point the weak Hashtbl that we use
are designed to work on this case, even with the identity function.
What we should do is a way to remove the task from a session when
they are not needed anymore.
- uses : pour l'instant, l'ordre des théories dans le fichier est important
i.e. les théories mentionnées par uses doivent être définies précédemment
......@@ -41,3 +45,17 @@ error reporting
- should we create a common [exception Why.Error of exn] to facilitate
integration of the library? This would require a special [raise] call:
why_raise e = raise (Why.Error e)
session
-------
- save the output of the prover
- escape the string in the xml
tools
-----
- the tools should verify that the provers have the same version
than reported in the configuration
- Maybe : make something generic for the dialog box with memory.
- autodetection can be modified now that only name/version/altern
are taken into account in session.
\ No newline at end of file
......@@ -247,8 +247,8 @@ let () =
if !opt_list_provers then begin
opt_list := true;
let config = read_config !opt_config in
let print fmt prover _ = fprintf fmt "%s (%s)@\n"
prover.prover_id prover.prover_name in
let print fmt prover pc = fprintf fmt "%s (%a)@\n"
pc.id print_prover prover in
let print fmt m = Mprover.iter (print fmt) m in
let provers = get_provers config in
printf "@[<hov 2>Known provers:@\n%a@]@." print provers
......
......@@ -155,8 +155,11 @@ let detect_exec main data com =
supported, use it at your own risk!@." nam ver
end;
let c = make_command com data.prover_command in
Some {name = data.prover_name;
version = ver;
let prover = {Whyconf.prover_name = data.prover_name;
prover_version = ver;
prover_altern = ""} in
Some {prover = prover;
id = data.prover_id;
command = c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor;
......@@ -180,10 +183,7 @@ let detect_prover main acc l =
with Not_found -> None
in
let prover = Util.list_first detect_execs l in
let prover_id = {Whyconf.prover_id = prover_id;
prover_name = prover.name;
prover_version = prover.version} in
Mprover.add prover_id prover acc
Mprover.add prover.prover prover acc
with Not_found ->
eprintf "Prover %s not found.@." prover_id;
acc
......
......@@ -54,34 +54,37 @@ let default_conf_file =
(* Prover *)
type prover =
{ prover_id : string;
prover_name : string;
{ prover_name : string;
prover_version : string;
prover_altern : string;
}
let print_prover fmt p =
Format.fprintf fmt "%s(%s)" p.prover_name p.prover_version
Format.fprintf fmt "%s(%s%s%s)"
p.prover_name p.prover_version
(if p.prover_altern = "" then "" else " ") p.prover_altern
module Prover = struct
type t = prover
let compare s1 s2 =
if s1 == s2 then 0 else
let c = String.compare s1.prover_id s2.prover_id in
if c <> 0 then c else
let c = String.compare s1.prover_name s2.prover_name in
if c <> 0 then c else
let c = String.compare s1.prover_version s2.prover_version in
if c <> 0 then c else
let c = String.compare s1.prover_altern s2.prover_altern in
c
let equal s1 s2 =
s1.prover_id = s2.prover_id &&
s1.prover_name = s2.prover_name &&
s1.prover_version = s2.prover_version
s1 == s2 ||
(s1.prover_name = s2.prover_name &&
s1.prover_version = s2.prover_version &&
s1.prover_altern = s2.prover_altern)
let hash s1 =
2 * Hashtbl.hash s1.prover_id +
3 * Hashtbl.hash s1.prover_name +
5 * Hashtbl.hash s1.prover_version
2 * Hashtbl.hash s1.prover_name +
3 * Hashtbl.hash s1.prover_version +
5 * Hashtbl.hash s1.prover_altern
end
......@@ -93,10 +96,10 @@ module Hprover = Hashtbl.Make(Prover)
(* Configuration file *)
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
prover : prover;
id : string;
command : string;
driver : string;
editor : string;
interactive : bool;
}
......@@ -197,35 +200,41 @@ let set_main rc main =
let section = set_stringl section "plugin" main.plugins in
set_section rc "main" section
let set_prover prover_id prover family =
exception NonUniqueId
let set_prover _ prover (ids,family) =
if Sstr.mem prover.id ids then raise NonUniqueId;
let section = empty_section in
let section = set_string section "name" prover.name in
let section = set_string section "name" prover.prover.prover_name in
let section = set_string section "command" prover.command in
let section = set_string section "driver" prover.driver in
let section = set_string section "version" prover.version in
let section = set_string section "version" prover.prover.prover_version in
let section = set_string ~default:""
section "alternative" prover.prover.prover_altern in
let section = set_string section "editor" prover.editor in
let section = set_bool section "interactive" prover.interactive in
(prover_id.prover_id,section)::family
(Sstr.add prover.id ids,(prover.id,section)::family)
let set_provers rc provers =
let family = Mprover.fold set_prover provers [] in
let _,family = Mprover.fold set_prover provers (Sstr.empty,[]) in
set_family rc "prover" family
let absolute_filename = Sysutil.absolutize_filename
let load_prover dirname provers (id,section) =
let version = get_string ~default:"" section "version" in
let altern = get_string ~default:"" section "alternative" in
let name = get_string section "name" in
let prover =
{ prover_id = id;
prover_name = name;
prover_version = version }
{ prover_name = name;
prover_version = version;
prover_altern = altern}
in
Mprover.add prover
{ name = name;
{ id = id;
prover = prover;
command = get_string section "command";
driver = absolute_filename dirname (get_string section "driver");
version = version;
editor = get_string ~default:"" section "editor";
interactive = get_bool ~default:false section "interactive";
} provers
......@@ -261,6 +270,8 @@ let () = Exn_printer.register (fun fmt e -> match e with
Format.fprintf fmt "error in config file %s: %s" f s
| WrongMagicNumber ->
Format.fprintf fmt "outdated config file; rerun why3config"
| NonUniqueId ->
Format.fprintf fmt "InternalError : two provers share the same id"
| _ -> raise e)
let get_config (filename,rc) =
......@@ -330,7 +341,7 @@ exception ProverAmbiguity of config * string * prover list
let prover_by_id whyconf id =
let potentials =
Mprover.filter (fun p _ -> p.prover_id = id) whyconf.provers in
Mprover.filter (fun _ p -> p.id = id) whyconf.provers in
match Mprover.keys potentials with
| [] -> raise (ProverNotFound(whyconf,id))
| [_] -> snd (Mprover.choose potentials)
......
......@@ -85,9 +85,9 @@ val load_plugins : main -> unit
(** {3 Prover's identifier} *)
type prover =
{ prover_id : string;
prover_name : string;
prover_version : string;
{ prover_name : string; (* "Alt-Ergo" *)
prover_version : string; (* "2.95" *)
prover_altern : string; (* "special" *)
}
(** record of necessary data for a given external prover
In the future prover_id will disappear.
......@@ -103,10 +103,10 @@ module Hprover : Hashtbl.S with type key = prover
(** {3 Prover configuration} *)
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
prover : prover; (* unique name for session *)
id : string; (* unique name for command line *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Dedicated editor *)
interactive : bool; (* Interative theorem prover *)
}
......
This diff is collapsed.
......@@ -18,6 +18,12 @@
(**************************************************************************)
open Why3
open Whyconf
(** Todo do something generic perhaps*)
type conf_replace_prover =
| CRP_Ask
| CRP_Not_Obsolete
type t =
{ mutable window_width : int;
......@@ -39,6 +45,8 @@ type t =
mutable error_color : string;
mutable env : Why3.Env.env;
mutable config : Whyconf.config;
mutable altern_provers : prover option Mprover.t;
mutable replace_prover : conf_replace_prover;
}
val read_config : string option -> unit
......@@ -94,7 +102,10 @@ val image_failure_obs : GdkPixbuf.pixbuf ref
val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
val unknown_prover :
t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
val replace_prover :
t -> 'key Session.proof_attempt -> 'key Session.proof_attempt -> bool
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
......
......@@ -549,6 +549,10 @@ let init =
| S.Transf tr -> tr.S.transf_name);
notify any
let unknown_prover = Gconfig.unknown_prover gconfig
let replace_prover = Gconfig.replace_prover gconfig
end)
......@@ -556,6 +560,7 @@ let init =
(* opening database *)
(********************)
(** TODO remove that should done only in session *)
let project_dir, file_to_read =
if Sys.file_exists fname then
begin
......@@ -1358,8 +1363,8 @@ let edit_selected_row r =
| S.File _file ->
()
| S.Proof_attempt a ->
M.edit_proof !env_session sched ~default_editor:gconfig.default_editor
~project_dir a
M.edit_proof
!env_session sched ~default_editor:gconfig.default_editor a
| S.Transf _ -> ()
let edit_current_proof () =
......
......@@ -211,6 +211,9 @@ let notify _any = ()
(Session.transformation_id tr.M.transf) tr.M.transf_proved
*)
let unknown_prover _ _ = None
let replace_prover _ _ = false
end)
......
......@@ -68,31 +68,33 @@ let () =
Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0
let string_of_prover p = Pp.string_of_wnl C.print_prover p
type proof_stats =
{ mutable no_proof : Sstr.t;
mutable only_one_proof : Sstr.t;
prover_min_time : (string, float) Hashtbl.t;
prover_avg_time : (string, float) Hashtbl.t;
prover_max_time : (string, float) Hashtbl.t;
prover_num_proofs : (string, int) Hashtbl.t;
prover_data : (string, string) Hashtbl.t
prover_min_time : float C.Hprover.t;
prover_avg_time : float C.Hprover.t;
prover_max_time : float C.Hprover.t;
prover_num_proofs : int C.Hprover.t;
prover_data : (string) C.Hprover.t
}
let new_proof_stats () =
{ no_proof = Sstr.empty;
only_one_proof = Sstr.empty;
prover_min_time = Hashtbl.create 3;
prover_avg_time = Hashtbl.create 3;
prover_max_time = Hashtbl.create 3;
prover_num_proofs = Hashtbl.create 3;
prover_data = Hashtbl.create 3 }
prover_min_time = C.Hprover.create 3;
prover_avg_time = C.Hprover.create 3;
prover_max_time = C.Hprover.create 3;
prover_num_proofs = C.Hprover.create 3;
prover_data = C.Hprover.create 3 }
let apply_f_on_hashtbl_entry ~tbl ~f ~name =
try
let cur_time = Hashtbl.find tbl name in
Hashtbl.replace tbl name (f (Some cur_time))
let cur_time = C.Hprover.find tbl name in
C.Hprover.replace tbl name (f (Some cur_time))
with Not_found ->
Hashtbl.add tbl name (f None)
C.Hprover.add tbl name (f None)
let update_min_time tbl (prover, time) =
apply_f_on_hashtbl_entry
......@@ -143,7 +145,7 @@ let rec stats_of_goal prefix_name stats goal =
begin
match result.Call_provers.pr_answer with
| Call_provers.Valid ->
(prover.C.prover_name, result.Call_provers.pr_time) :: acc
(prover, result.Call_provers.pr_time) :: acc
| _ ->
acc
end
......@@ -156,7 +158,9 @@ let rec stats_of_goal prefix_name stats goal =
stats.no_proof <- Sstr.add proof_id stats.no_proof
| [ (prover, time) ] when no_transf ->
stats.only_one_proof <-
Sstr.add (proof_id ^ " : " ^ prover) stats.only_one_proof;
Sstr.add
(proof_id ^ " : " ^ (string_of_prover prover))
stats.only_one_proof;
update_perf_stats stats (prover, time)
| _ ->
List.iter (update_perf_stats stats) proof_list end;
......@@ -179,7 +183,7 @@ let stats_of_file stats _ file =
let fill_prover_data stats session =
C.Sprover.iter
(fun prover ->
Hashtbl.add stats.prover_data prover.C.prover_id
C.Hprover.add stats.prover_data prover
(prover.C.prover_name ^ " " ^ prover.C.prover_version))
(get_used_provers session)
......@@ -196,15 +200,17 @@ let extract_stats_from_file stats fname =
exit 1
let finalize_stats stats =
Hashtbl.iter
C.Hprover.iter
(fun prover time ->
let n = Hashtbl.find stats.prover_num_proofs prover in
Hashtbl.replace stats.prover_avg_time prover (time /. (float_of_int n)))
let n = C.Hprover.find stats.prover_num_proofs prover in
C.Hprover.replace stats.prover_avg_time prover
(time /. (float_of_int n)))
stats.prover_avg_time
let print_stats stats =
printf "== Provers available ==@\n @[";
Hashtbl.iter (fun prover data -> printf "%-10s: %s@\n" prover data)
C.Hprover.iter (fun prover data -> printf "%-10s: %s@\n"
(string_of_prover prover) data)
stats.prover_data;
printf "@]@\n";
......@@ -217,22 +223,26 @@ let print_stats stats =
printf "@]@\n";
printf "== Number of proofs per prover ==@\n @[";
Hashtbl.iter (fun prover n -> printf "%-10s: %d@\n" prover n)
C.Hprover.iter (fun prover n -> printf "%-10s: %d@\n"
(string_of_prover prover) n)
stats.prover_num_proofs;
printf "@]@\n";
printf "== Minimum time per prover ==@\n @[";
Hashtbl.iter (fun prover time -> printf "%-10s : %.3f s@\n" prover time)
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_min_time;
printf "@]@\n";
printf "== Maximum time per prover ==@\n @[";
Hashtbl.iter (fun prover time -> printf "%-10s : %.3f s@\n" prover time)
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_max_time;
printf "@]@\n";
printf "== Average time per prover ==@\n @[";
Hashtbl.iter (fun prover time -> printf "%-10s : %.3f s@\n" prover time)
C.Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
(string_of_prover prover) time)
stats.prover_avg_time;
printf "@]@\n"
......
......@@ -257,8 +257,8 @@ let () = try
if !opt_list_provers then begin
opt_list := true;
let config = read_config !opt_config in
let print fmt prover _ = fprintf fmt "%s (%s)@\n"
prover.prover_id prover.prover_name in
let print fmt prover pc = fprintf fmt "%s (%a)@\n"
pc.id print_prover prover in
let print fmt m = Mprover.iter (print fmt) m in
let provers = get_provers config in
printf "@[<hov 2>Known provers:@\n%a@]@." print provers
......
......@@ -19,6 +19,7 @@
open Stdlib
open Debug
open Util
module Mprover = Whyconf.Mprover
module Sprover = Whyconf.Sprover
......@@ -375,9 +376,11 @@ let save_file provers fmt _ f =
fprintf fmt "@]@\n</file>"
let save_prover fmt p (provers,id) =
fprintf fmt "@\n@[<v 1><prover@ id=\"%i\"@ prover_id=\"%s\" \
name=\"%s\"@ version=\"%s\"/>@]"
id p.C.prover_id p.C.prover_name p.C.prover_version;
fprintf fmt "@\n@[<v 1><prover@ id=\"%i\"@ \
name=\"%s\"@ version=\"%s\"%a/>@]"
id p.C.prover_name p.C.prover_version
(fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%s\"" s)
p.C.prover_altern;
Mprover.add p id provers, id+1
let save fname session =
......@@ -498,6 +501,7 @@ type 'a keygen = ?parent:'a -> unit -> 'a
let add_external_proof
?(notify=notify)
~(keygen:'a keygen) ~obsolete ~timelimit ~edit (g:'a goal) p result =
assert (edit <> Some "");
let key = keygen ~parent:g.goal_key () in
let a = { proof_prover = p;
proof_parent = g;
......@@ -749,6 +753,7 @@ and load_proof_or_transf ~old_provers mg a =
in
let edit = load_option "edited" a in
let edit = match edit with None | Some "" -> None | _ -> edit in
let obsolete = bool_attribute "obsolete" a true in
let timelimit = int_attribute "timelimit" a (-1) in
if timelimit < 0 then begin
......@@ -807,13 +812,14 @@ let load_file session old_provers f =
(load_theory ~old_provers mf) [] f.Xml.elements);
old_provers
| "prover" ->
(** The id is just for the session file *)
let id = string_attribute "id" f in
let prover_id = string_attribute_def "prover_id" f id in
let name = string_attribute "name" f in
let version = string_attribute "version" f in
let p = {C.prover_id = prover_id;
prover_name = name;
prover_version = version} in
let altern = string_attribute_def "alternative" f "" in
let p = {C.prover_name = name;
prover_version = version;
prover_altern = altern} in
Util.Mstr.add id p old_provers
| s ->
eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
......@@ -1065,6 +1071,135 @@ let () = Exn_printer.register
| _ -> raise exn)
let ft_of_th th =
let fn = Filename.basename th.theory_parent.file_name in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
(fn, th.theory_name.Ident.id_string)
let rec ft_of_goal g =
match g.goal_parent with
| Parent_transf tr -> ft_of_goal tr.transf_parent
| Parent_theory th -> ft_of_th th
let ft_of_pa a =
ft_of_goal a.proof_parent
(** TODO see with Undone Edited
But since it will be perhaps removed...
*)
let copy_external_proof
?notify ~keygen ?obsolete ?timelimit ?edit
?goal ?prover ?attempt_status ?env_session ?session a =
let session = match env_session with
| Some eS -> Some eS.session
| _ -> session in
let obsolete = default_option a.proof_obsolete obsolete in
let timelimit = default_option a.proof_timelimit timelimit in
let pas = default_option a.proof_state attempt_status in
let ngoal = default_option a.proof_parent goal in
let nprover = match prover with
| None -> a.proof_prover
| Some prover -> prover in
(** copy or generate the edit file if needed *)
let edit =
match edit, a.proof_edited_as, session with
| Some edit, _, _ -> edit
| _, None, _ -> None
| _, _, None -> (** In the other case a session is needed *)
None
| _, Some file, Some session ->
assert (file != "");
(** Copy the edited file *)
let dir = session.session_dir in
let file = Filename.concat dir file in
if not (Sys.file_exists file) then None else
match prover,goal, ngoal.goal_task, env_session with
| None,None,_,_ ->
let dst_file = Sysutil.uniquify file in
Sysutil.copy_file file dst_file;
let dst_file = Sysutil.relativize_filename dir dst_file in
Some dst_file
| (_, _, None,_)| (_, _, _, None) ->
(** In the other cases an env_session and a task are needed *)
None
| _, _, Some task, Some env_session ->
match load_prover env_session nprover with
| None -> None
| Some prover_conf ->
let (fn,tn) = ft_of_goal ngoal in
let driver = prover_conf.prover_driver in
let dst_file = Driver.file_of_task driver fn tn task in
let dst_file = Filename.concat dir dst_file in
let dst_file = Sysutil.uniquify dst_file in
let old = open_in file in
let ch = open_out dst_file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ~old driver fmt task;
close_in old;
close_out ch;
let dst_file = Sysutil.relativize_filename dir dst_file in
Some (dst_file)
in
add_external_proof ?notify ~keygen
~obsolete ~timelimit ~edit ngoal nprover pas
exception UnloadableProver of Whyconf.prover
let update_edit_external_proof env_session a =
let prover_conf = match load_prover env_session a.proof_prover with
| Some prover_conf -> prover_conf
| None -> raise (UnloadableProver a.proof_prover) in
let driver = prover_conf.prover_driver in
let goal = goal_task a.proof_parent in
let session_dir = env_session.session.session_dir in
let file =
match a.proof_edited_as with
| None ->
let (fn,tn) = ft_of_pa a in
let file = Driver.file_of_task driver fn tn goal in
let file = Filename.concat session_dir file in
let file = Sysutil.uniquify file in
let file = Sysutil.relativize_filename session_dir file in
set_edited_as (Some file) a;
if a.proof_state = Undone Unedited
then set_proof_state ~notify ~obsolete:a.proof_obsolete
(Undone Interrupted) a;
file
| Some f -> f
in
let file = Filename.concat session_dir file in
let old =
if Sys.file_exists file
then
begin
let backup = file ^ ".bak" in
if Sys.file_exists backup
then Sys.remove backup;
Sys.rename file backup;
Some(open_in backup)
end
else None
in
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ?old driver fmt goal;
Util.option_iter close_in old;
close_out ch;
file
let print_attempt_status fmt = function
| Undone _ -> pp_print_string fmt "Undone"
| Done pr -> Call_provers.print_prover_result fmt pr
| InternalFailure _ -> pp_print_string fmt "Failure"
let print_external_proof fmt p =
fprintf fmt "%a - %a (%i)%s%s"
Whyconf.print_prover p.proof_prover
print_attempt_status p.proof_state
p.proof_timelimit
(if p.proof_obsolete then " obsolete" else "")