Commit 5b9cffda authored by MARCHE Claude's avatar MARCHE Claude

New policies for uninstalled provers

parent 3ee0459f
......@@ -62,9 +62,10 @@ type prover =
}
let print_prover fmt p =
Format.fprintf fmt "%s (%s%s%s)"
p.prover_name p.prover_version
(if p.prover_altern = "" then "" else " ") p.prover_altern
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
......@@ -73,20 +74,20 @@ module Prover = struct
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
(* if c <> 0 then c else *)
(* let c = String.compare s1.prover_altern s2.prover_altern in *)
c
let equal s1 s2 =
s1 == s2 ||
(s1.prover_name = s2.prover_name &&
s1.prover_version = s2.prover_version &&
s1.prover_altern = s2.prover_altern)
s1.prover_version = s2.prover_version(* && *)
(* s1.prover_altern = s2.prover_altern *))
let hash s1 =
2 * Hashtbl.hash s1.prover_name +
3 * Hashtbl.hash s1.prover_version +
5 * Hashtbl.hash s1.prover_altern
3 * Hashtbl.hash s1.prover_version (* + *)
(* 5 * Hashtbl.hash s1.prover_altern *)
end
module Mprover = Map.Make(Prover)
......@@ -102,6 +103,11 @@ module Meditor = Map.Make(Editor)
(* Configuration file *)
type prover_upgrade_policy =
| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
type config_prover = {
prover : prover;
id : string;
......@@ -118,6 +124,7 @@ type config_editor = {
editor_options : string list;
}
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
......@@ -187,6 +194,7 @@ type config = {
main : main;
provers : config_prover Mprover.t;
editors : config_editor Meditor.t;
provers_upgrade_policy : prover_upgrade_policy Mprover.t;
}
let default_main =
......@@ -224,8 +232,7 @@ let set_prover _ prover (ids,family) =
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.prover.prover_version in
let section = set_string ~default:""
section "alternative" prover.prover.prover_altern 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
(Sstr.add prover.id ids,(prover.id,section)::family)
......@@ -244,16 +251,45 @@ let set_editors rc editors =
let _,family = Meditor.fold set_editor editors (Sstr.empty,[]) in
set_family rc "editor" family
let set_prover_upgrade_policy prover policy (i, family) =
let section = empty_section in
let section = set_string section "name" prover.prover_name in
let section = set_string section "version" prover.prover_version in
let section = set_string section "alternative" prover.prover_altern in
let section =
match policy with
| CPU_keep ->
set_string section "policy" "keep"
| CPU_upgrade p ->
let section = set_string section "target_name" p.prover_name in
let section = set_string section "target_version" p.prover_version in
let section = set_string section "target_alternative" p.prover_altern in
set_string section "policy" "upgrade"
| CPU_duplicate p ->
let section = set_string section "target_name" p.prover_name in
let section = set_string section "target_version" p.prover_version in
let section = set_string section "target_alternative" p.prover_altern in
set_string section "policy" "duplicate"
in
(i+1,("policy" ^ string_of_int i, section)::family)
let set_policies rc policy =
let _,family =
Mprover.fold set_prover_upgrade_policy policy (0,[])
in
set_family rc "uninstalled_prover" family
let absolute_filename = Sysutil.absolutize_filename
let load_prover dirname provers (id,section) =
let name = get_string section "name" in
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_name = name;
prover_version = version;
prover_altern = altern}
prover_altern = altern;
}
in
Mprover.add prover
{ id = id;
......@@ -272,6 +308,36 @@ let load_editor editors (id, section) =
editor_options = [];
} editors
let load_policy provers acc (_,section) =
let source =
{prover_name = get_string section "name";
prover_version = get_string section "version";
prover_altern = get_string ~default:"" section "alternative"
} in
try
match get_string section "policy" with
| "keep" -> Mprover.add source CPU_keep acc
| "upgrade" ->
let target =
{ prover_name = get_string section "target_name";
prover_version = get_string section "target_version";
prover_altern = get_string ~default:"" section "target_alternative";
}
in
let _target = Mprover.find target provers in
Mprover.add source (CPU_upgrade target) acc
| "duplicate" ->
let target =
{ prover_name = get_string section "target_name";
prover_version = get_string section "target_version";
prover_altern = get_string ~default:"" section "target_alternative";
}
in
let _target = Mprover.find target provers in
Mprover.add source (CPU_duplicate target) acc
| _ -> raise Not_found
with Not_found -> acc
let load_main dirname section =
if get_int ~default:0 section "magic" <> magicnumber then
raise WrongMagicNumber;
......@@ -318,11 +384,14 @@ let get_config (filename,rc) =
let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
let editors = get_family rc "editor" in
let editors = List.fold_left load_editor Meditor.empty editors in
let policy = get_family rc "uninstalled_prover" in
let policy = List.fold_left (load_policy provers) Mprover.empty policy in
{ conf_file = filename;
config = rc;
main = main;
provers = provers;
editors = editors;
provers_upgrade_policy = policy;
}
let default_config conf_file =
......@@ -383,6 +452,9 @@ let save_config config =
let get_main config = config.main
let get_provers config = config.provers
let get_policies config = config.provers_upgrade_policy
let get_prover_upgrade_policy config p =
Mprover.find p config.provers_upgrade_policy
let set_main config main =
{config with
......@@ -402,6 +474,25 @@ let set_editors config editors =
editors = editors;
}
let set_prover_upgrade_policy config prover target =
let m = Mprover.add prover target config.provers_upgrade_policy in
{config with
config = set_policies config.config m;
provers_upgrade_policy = m;
}
let set_policies config policies =
Format.eprintf "set_policies:";
Mprover.iter
(fun p _ -> Format.eprintf " %a, " print_prover p)
policies;
Format.eprintf "@.";
{ config with
config = set_policies config.config policies;
provers_upgrade_policy = policies }
(*******)
let set_conf_file config conf_file = {config with conf_file = conf_file}
......
......@@ -146,6 +146,28 @@ val editor_by_id : config -> string -> config_editor
(** return the configuration of the editor if found, otherwise return
Not_found *)
(** prover upgrade policy *)
type prover_upgrade_policy =
| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
val set_prover_upgrade_policy :
config -> prover -> prover_upgrade_policy -> config
(** [set_prover_upgrade c p cpu] sets or updates the policy to follow if the
prover [p] is absent from the system *)
val get_prover_upgrade_policy : config -> prover -> prover_upgrade_policy
(** [get_prover_upgrade config] returns a map providing the policy to
follow for each absent prover (if it has already been decided
by the user and thus stored in the config) *)
val get_policies : config -> prover_upgrade_policy Mprover.t
val set_policies : config -> prover_upgrade_policy Mprover.t -> config
(** {2 For accesing other parts of the configuration } *)
(** Access to the Rc.t *)
......
......@@ -27,7 +27,7 @@ open Whyconf
(* config file *)
type altern_provers = prover option Mprover.t
(* type altern_provers = prover option Mprover.t *)
(** Todo do something generic perhaps*)
(*
......@@ -59,7 +59,7 @@ type t =
mutable env : Env.env;
mutable config : Whyconf.config;
original_config : Whyconf.config;
mutable altern_provers : altern_provers;
(* mutable altern_provers : altern_provers; *)
(* mutable replace_prover : conf_replace_prover; *)
(* hidden prover buttons *)
mutable hidden_provers : string list;
......@@ -190,9 +190,9 @@ let load_config config original_config =
Format.eprintf "hidden provers : ";
List.iter (fun p -> Format.eprintf "%s" p) ide.ide_hidden_provers;
Format.eprintf "@.";
let alterns =
List.fold_left load_altern
Mprover.empty (get_family config "alternative_prover") in
(* let alterns = *)
(* List.fold_left load_altern *)
(* Mprover.empty (get_family config "alternative_prover") in *)
(* temporary sets env to empty *)
let env = Env.create_env [] in
set_labels_flag ide.ide_show_labels;
......@@ -217,13 +217,15 @@ let load_config config original_config =
config = config;
original_config = original_config;
env = env;
altern_provers = alterns;
(* altern_provers = alterns; *)
(* replace_prover = ide.ide_replace_prover; *)
hidden_provers = ide.ide_hidden_provers;
}
let save_altern unknown known (id,family) =
(*
let save_altern unknown known (id,family) =
let alt = empty_section in
let alt = set_string alt "unknown_name" unknown.prover_name in
let alt = set_string alt "unknown_version" unknown.prover_version in
......@@ -237,14 +239,17 @@ let save_altern unknown known (id,family) =
set_string ~default:"" alt "known_alternative" known.prover_altern in
(id+1,(sprintf "alt%i" id,alt)::family)
*)
let save_config t =
let config = t.original_config in
let config = set_main config
(set_limits (get_main config)
t.time_limit t.mem_limit t.max_running_processes)
in
let _,alterns = Mprover.fold save_altern t.altern_provers (0,[]) in
let config = set_family config "alternative_prover" alterns in
(* let _,alterns = Mprover.fold save_altern t.altern_provers (0,[]) in *)
(* let config = set_family config "alternative_prover" alterns in *)
let config = set_policies config (get_policies t.config) in
let ide = empty_section in
let ide = set_int ide "window_height" t.window_height in
let ide = set_int ide "window_width" t.window_width in
......@@ -469,7 +474,7 @@ let show_about_window () =
let ( _ : GWindow.Buttons.about) = about_dialog#run () in
about_dialog#destroy ()
let alternatives_frame c (notebook:GPack.notebook) =
let alternatives_frame _c (notebook:GPack.notebook) =
let label = GMisc.label ~text:"Alternative provers" () in
let page =
GPack.vbox ~homogeneous:false ~packing:
......@@ -494,13 +499,16 @@ let alternatives_frame c (notebook:GPack.notebook) =
GBin.frame ~label:"Click for removing an association"
~packing:page#add ()
in
let box =
let _box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:frame#add ()
in
let remove button unknown () =
let _remove button _unknown () =
button#destroy ();
c.altern_provers <- Mprover.remove unknown c.altern_provers in
assert false (* TODO *)
(* c.altern_provers <- Mprover.remove unknown c.altern_provers *)
in
(*
let iter unknown known =
let label =
match known with
......@@ -512,6 +520,8 @@ let alternatives_frame c (notebook:GPack.notebook) =
button#connect#released ~callback:(remove button unknown)
in () in
Mprover.iter iter c.altern_provers
*)
()
let preferences (c : t) =
let dialog = GWindow.dialog ~title:"Why3: preferences" () in
......@@ -742,9 +752,87 @@ let run_auto_detection gconfig =
(* let () = eprintf "[Info] end of configuration initialization@." *)
let unknown_prover c eS unknown =
try Mprover.find unknown c.altern_provers
let uninstalled_prover c eS unknown =
Format.eprintf "uninstalled_prover@.";
try
Whyconf.get_prover_upgrade_policy c.config unknown
with Not_found ->
Format.eprintf "making dialog@.";
let others,names,versions = Session_tools.unknown_to_known_provers
(Whyconf.get_provers eS.Session.whyconf) unknown in
let dialog = GWindow.dialog ~title:"Why3: Uninstalled prover" () in
let vbox = dialog#vbox in
let label = Pp.sprintf "The prover %a is not installed. Please select \
a policy for associated proof attemtps" Whyconf.print_prover unknown in
let policy_frame = GBin.frame ~label ~packing:vbox#add () in
let choice = ref 0 in
let prover_choosed = ref None in
let set_prover prover () = prover_choosed := Some prover in
let box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:policy_frame#add ()
in
let choice0 = GButton.radio_button
~label:"keep proofs as they are, do not try to play them"
~active:true
~packing:box#add () in
ignore (choice0#connect#toggled
~callback:(fun () -> choice := 0));
let choice1 = GButton.radio_button
~label:"move proofs to the selected prover below"
~active:false ~group:choice0#group
~packing:box#add () in
ignore (choice1#connect#toggled
~callback:(fun () -> choice := 1));
let choice2 = GButton.radio_button
~label:"duplicate proofs to the selected prover below"
~active:false ~group:choice0#group
~packing:box#add () in
ignore (choice2#connect#toggled
~callback:(fun () -> choice := 2));
let first = ref None in
let alternatives_section label alternatives =
if alternatives <> [] then
let frame = GBin.frame ~label ~packing:vbox#add () in
let box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:frame#add ()
in
let iter_alter prover =
let choice =
let label = Pp.string_of_wnl print_prover prover in
match !first with
| None ->
let choice =
GButton.radio_button ~label ~active:true ~packing:box#add ()
in
prover_choosed := Some prover;
first := Some choice;
choice
| Some first ->
GButton.radio_button ~label ~group:first#group
~active:false ~packing:box#add ()
in
ignore (choice#connect#toggled ~callback:(set_prover prover))
in
List.iter iter_alter alternatives in
alternatives_section "Same name and same version" versions;
alternatives_section "Same name and different version" names;
alternatives_section "Different name and different version" others;
dialog#add_button "Ok" `CLOSE ;
ignore (dialog#run ());
dialog#destroy ();
let policy =
match !choice, !prover_choosed with
| 0,_ -> CPU_keep
| 1, Some p -> CPU_upgrade p
| 2, Some p -> CPU_duplicate p
| _ -> assert false
in
c.config <- set_prover_upgrade_policy c.config unknown policy;
policy
(*
let unknown_prover c eS unknown =
let others,names,versions = Session_tools.unknown_to_known_provers
(Whyconf.get_provers eS.Session.whyconf) unknown in
let dialog = GWindow.dialog ~title:"Why3: Unknown prover" () in
......@@ -796,8 +884,9 @@ an alternative?" Whyconf.print_prover unknown in
if save#active then
c.altern_provers <- Mprover.add unknown !prover_choosed c.altern_provers;
!prover_choosed
*)
(* obsolete dialog
(* obsolete dialog
let replace_prover c to_be_removed to_be_copied =
if not to_be_removed.Session.proof_obsolete &&
c.replace_prover = CRP_Not_Obsolete
......
......@@ -47,7 +47,7 @@ type t =
mutable env : Why3.Env.env;
mutable config : Whyconf.config;
original_config : Whyconf.config;
mutable altern_provers : prover option Mprover.t;
(* mutable altern_provers : prover option Mprover.t; *)
(* mutable replace_prover : conf_replace_prover; *)
mutable hidden_provers : string list;
}
......@@ -105,8 +105,14 @@ val image_failure_obs : GdkPixbuf.pixbuf ref
val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
val uninstalled_prover :
t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
(*
val unknown_prover :
t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover option
*)
(* obsolete dialog
val replace_prover :
......
......@@ -608,25 +608,33 @@ module M = Session_scheduler.Make
(if r=0 then "Running: 0" else
"Running: " ^ (string_of_int r)^ " " ^ (fan (!c / 10)))
let notify any =
session_needs_saving := true;
let row,exp =
match any with
| S.Goal g ->
g.S.goal_key, g.S.goal_expanded
| S.Goal g -> g.S.goal_key, g.S.goal_expanded
| S.Theory t -> t.S.theory_key, t.S.theory_expanded
| S.File f -> f.S.file_key, f.S.file_expanded
| S.Proof_attempt a -> a.S.proof_key,false
| S.Transf tr -> tr.S.transf_key,tr.S.transf_expanded
in
(* name is set by notify since upgrade policy may update the prover name *)
goals_model#set ~row:row#iter ~column:name_column
(match any with
| S.Goal g -> S.goal_expl g
| S.Theory th -> th.S.theory_name.Ident.id_string
| S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a ->
let p = a.S.proof_prover in
Pp.string_of_wnl C.print_prover p
| S.Transf tr -> tr.S.transf_name);
let ind = goals_model#get ~row:row#iter ~column:index_column in
begin
match !current_selected_row with
| Some r when r == ind ->
update_task_view any
| _ -> ()
end;
end;
if exp then goals_view#expand_to_path row#path else
goals_view#collapse_row row#path;
match any with
......@@ -663,20 +671,15 @@ let init =
| S.File _ -> !image_directory
| S.Proof_attempt _ -> !image_prover
| S.Transf _ -> !image_transf);
goals_model#set ~row:row#iter ~column:name_column
(match any with
| S.Goal g -> S.goal_expl g
| S.Theory th -> th.S.theory_name.Ident.id_string
| S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a ->
let p = a.S.proof_prover in
Pp.string_of_wnl C.print_prover p
| S.Transf tr -> tr.S.transf_name);
notify any
(*
let unknown_prover = Gconfig.unknown_prover gconfig
let replace_prover _ _ = false (* Gconfig.replace_prover gconfig *)
*)
let uninstalled_prover = Gconfig.uninstalled_prover gconfig
end)
......@@ -961,26 +964,6 @@ let save_session () =
let exit_function ?(destroy=false) () =
eprintf "[Info] saving IDE config file@.";
save_config ();
(*
eprintf "saving session (testing only)@.";
begin
M.test_save ();
try
let l = M.test_load () in
eprintf "reloaded successfully %d elements@." (List.length l);
match l with
| [] -> ()
| f :: _ ->
eprintf "first element is a '%s' with %d sub-elements@."
f.Xml.name (List.length f.Xml.elements);
with e -> eprintf "test reloading failed with exception %s@."
(Printexc.to_string e)
end;
let ret = Sys.command
"xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in
if ret = 0 then eprintf "DTD validation succeeded, good!@.";
*)
if not !session_needs_saving then GMain.quit () else
match (Gconfig.config ()).saving_policy with
| 0 -> save_session (); GMain.quit ()
......
......@@ -198,9 +198,17 @@ let notify _any = ()
(Session.transformation_id tr.M.transf) tr.M.transf_proved
*)
(*
let unknown_prover _ _ = None
let replace_prover _ _ = false
*)
let uninstalled_prover _eS unknown =
try
Whyconf.get_prover_upgrade_policy config unknown
with Not_found ->
Whyconf.CPU_keep
module Scheduler = Session_scheduler.Base_scheduler(struct end)
......
......@@ -63,7 +63,7 @@ type 'a goal =
and 'a proof_attempt =
{ proof_key : 'a;
proof_prover : Whyconf.prover;
mutable proof_prover : Whyconf.prover;
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
......@@ -575,6 +575,8 @@ let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
notify (Proof_attempt a);
check_goal_proved notify a.proof_parent
let change_prover a p = a.proof_prover <- p
let set_edited_as edited_as a = a.proof_edited_as <- edited_as
let set_timelimit timelimit a = a.proof_timelimit <- timelimit
......
......@@ -80,7 +80,7 @@ type 'a goal = private
and 'a proof_attempt = private
{ proof_key : 'a;
proof_prover : Whyconf.prover;
mutable proof_prover : Whyconf.prover;
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
......@@ -275,6 +275,8 @@ val set_proof_state :
proof_attempt_status ->
'key proof_attempt -> unit
val change_prover : 'a proof_attempt -> Whyconf.prover -> unit
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit
val set_archived : 'key proof_attempt -> bool -> unit
......
......@@ -43,10 +43,15 @@ module type OBSERVER = sig
val notify : key any -> unit
(*
val unknown_prover :
key env_session -> Whyconf.prover -> Whyconf.prover option
val replace_prover : key proof_attempt -> key proof_attempt -> bool
*)
val uninstalled_prover :
key env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
end
......@@ -324,6 +329,7 @@ let add_file env_session f =
(*****************************************************)
(* method: run a given prover on each unproved goals *)
(*****************************************************)
(*
let rec find_loadable_prover eS prover =
(** try the default one *)
match load_prover eS prover with
......@@ -334,6 +340,36 @@ let rec find_loadable_prover eS prover =
| Some prover -> find_loadable_prover eS prover
end
| Some npc -> Some (prover,npc)
*)
let find_prover eS a =
match load_prover eS a.proof_prover with
| Some p -> Some (a.proof_prover, p,a)
| None ->
match O.uninstalled_prover eS a.proof_prover with
| Whyconf.CPU_keep -> None
| Whyconf.CPU_upgrade new_p ->
(* does a proof using new_p already exists ? *)
let g = a.proof_parent in
begin
try
let _ = PHprover.find g.goal_external_proofs new_p in
(* yes, then we do nothing *)
None
with Not_found ->
(* we modify the prover in-place *)
Session.change_prover a new_p;
match load_prover eS new_p with
| Some p -> Some (new_p,p,a)
| None ->
(* should never happen because at loading, config
ignores uninstalled prover targets.
Nevertheless, we can safely return None.
*)
None
end
| Whyconf.CPU_duplicate _p -> assert false (* TODO *)
let adapt_timelimit a =
match a.proof_state with
......@@ -351,6 +387,12 @@ let run_external_proof eS eT ?callback a =
(* Perhaps this test, a.proof_archived, should be done somewhere else *)
if a.proof_archived || running a then ()
else
match find_prover eS a with
| None ->
(* nothing to do *)
Util.apply_option2 () callback a a.proof_state
| Some(_,npc,a) ->
(*
let ap = a.proof_prover in
match find_loadable_prover eS a.proof_prover with
| None ->
......@@ -381,6 +423,8 @@ let run_external_proof eS eT ?callback a =
O.init a.proof_key (Proof_attempt a);