Commit 3b938adc authored by MARCHE Claude's avatar MARCHE Claude

Real support for memlimit in IDE and sessions

parent c7093cbc
......@@ -202,9 +202,9 @@ let default_main =
libdir = Config.libdir;
datadir = Config.datadir;
loadpath = default_loadpath;
timelimit = 10;
memlimit = 0;
running_provers_max = 2;
timelimit = 5; (* 5 seconds *)
memlimit = 1000; (* 1 Mb *)
running_provers_max = 2; (* two provers run in parallel *)
plugins = [];
}
......
......@@ -493,24 +493,36 @@ let general_settings c (notebook:GPack.notebook) =
(fun () -> c.verbose <- 1 - c.verbose)
in
*)
(* timelimit ? *)
(* time limit *)
let main = Whyconf.get_main c.config in
let width = 200 and xalign = 0.0 in
let timelimit = ref (Whyconf.timelimit main) in
let memlimit = ref (Whyconf.memlimit main) in
let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
let _ = GMisc.label ~text:"Time limit: "
let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
~packing:(hb#pack ~expand:false) () in
let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:300. ~step_incr:1. ();
timelimit_spin#adjustment#set_value (float_of_int !timelimit);
let (_ : GtkSignal.id) =
timelimit_spin#connect#value_changed ~callback:
(fun () -> timelimit := timelimit_spin#value_as_int)
in
(* mem limit *)
let memlimit = ref (Whyconf.memlimit main) in
let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
~packing:(hb#pack ~expand:false) () in
let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:4000. ~step_incr:100. ();
memlimit_spin#adjustment#set_value (float_of_int !memlimit);
let (_ : GtkSignal.id) =
memlimit_spin#connect#value_changed ~callback:
(fun () -> memlimit := memlimit_spin#value_as_int)
in
(* nb of processes ? *)
let nb_processes = ref (Whyconf.running_provers_max main) in
let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in
let _ = GMisc.label ~text:"Nb of processes: "
let _ = GMisc.label ~text:"Nb of processes: " ~width ~xalign
~packing:(hb#pack ~expand:false) () in
let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
nb_processes_spin#adjustment#set_bounds
......
......@@ -468,7 +468,8 @@ let set_proof_state a =
| S.InternalFailure _ -> "(internal failure)"
| S.Undone S.Interrupted -> "(interrupted)"
| S.Undone (S.Scheduled | S.Running) ->
Format.sprintf "[limit=%d.0]" a.S.proof_timelimit
Format.sprintf "[limit=%d sec., %d M]"
a.S.proof_timelimit a.S.proof_memlimit
in
let t = if obsolete then t ^ " (obsolete)" else t in
(* TODO find a better way to signal arhived row *)
......@@ -806,7 +807,9 @@ let () =
(*****************************************************)
let prover_on_selected_goals pr =
let timelimit = Whyconf.timelimit (Whyconf.get_main gconfig.config) in
let main = Whyconf.get_main gconfig.config in
let timelimit = Whyconf.timelimit main in
let memlimit = Whyconf.memlimit main in
List.iter
(fun row ->
try
......@@ -814,7 +817,7 @@ let prover_on_selected_goals pr =
M.run_prover
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~timelimit
~timelimit ~memlimit
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......
......@@ -413,7 +413,7 @@ let run_as_bench env_session =
eprintf " done.@.";
exit 0
in
M.play_all env_session sched ~callback ~timelimit:2 provers;
M.play_all env_session sched ~callback ~timelimit:2 ~memlimit:0 provers;
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
exit 1
......
......@@ -67,6 +67,7 @@ and 'a proof_attempt =
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_memlimit : int;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
......@@ -341,9 +342,10 @@ let opt lab fmt = function
let save_proof_attempt provers fmt _key a =
fprintf fmt
"@\n@[<v 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ %a\
obsolete=\"%b\"@ archived=\"%b\">"
"@\n@[<v 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ \
memlimit=\"%d\"@ %aobsolete=\"%b\"@ archived=\"%b\">"
(Mprover.find a.proof_prover provers) a.proof_timelimit
a.proof_memlimit
(opt "edited") a.proof_edited_as a.proof_obsolete
a.proof_archived;
save_status fmt a.proof_state;
......@@ -546,7 +548,7 @@ type 'a keygen = ?parent:'a -> unit -> 'a
let add_external_proof
?(notify=notify)
~(keygen:'a keygen) ~obsolete
~archived ~timelimit ~edit (g:'a goal) p result =
~archived ~timelimit ~memlimit ~edit (g:'a goal) p result =
assert (edit <> Some "");
let key = keygen ~parent:g.goal_key () in
let a = { proof_prover = p;
......@@ -556,6 +558,7 @@ let add_external_proof
proof_archived = archived;
proof_state = result;
proof_timelimit = timelimit;
proof_memlimit = memlimit;
proof_edited_as = edit;
}
in
......@@ -586,6 +589,7 @@ let change_prover a p =
let set_edited_as edited_as a = a.proof_edited_as <- edited_as
let set_timelimit timelimit a = a.proof_timelimit <- timelimit
let set_memlimit memlimit a = a.proof_memlimit <- memlimit
let set_obsolete ?(notify=notify) a =
a.proof_obsolete <- true;
......@@ -825,16 +829,19 @@ 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 true in
let archived = bool_attribute "archived" a false in
let timelimit = int_attribute "timelimit" a (-1) in
let timelimit = int_attribute "timelimit" a 2 in
let memlimit = int_attribute "memlimit" a 0 in
(*
if timelimit < 0 then begin
eprintf "[Error] incorrector unspecified timelimit '%i'@."
eprintf "[Error] incorrect or unspecified timelimit '%i'@."
timelimit;
raise (LoadError (a,sprintf "incorrect or unspecified timelimit %i"
timelimit))
end;
*)
let (_ : 'a proof_attempt) =
add_external_proof ~keygen ~archived ~obsolete
~timelimit ~edit mg p res
~timelimit ~memlimit ~edit mg p res
in
()
| "transf" ->
......@@ -1167,7 +1174,7 @@ let ft_of_pa a =
But since it will be perhaps removed...
*)
let copy_external_proof
?notify ~keygen ?obsolete ?archived ?timelimit ?edit
?notify ~keygen ?obsolete ?archived ?timelimit ?memlimit ?edit
?goal ?prover ?attempt_status ?env_session ?session a =
let session = match env_session with
| Some eS -> Some eS.session
......@@ -1175,6 +1182,7 @@ let copy_external_proof
let obsolete = def_option a.proof_obsolete obsolete in
let archived = def_option a.proof_archived archived in
let timelimit = def_option a.proof_timelimit timelimit in
let memlimit = def_option a.proof_memlimit memlimit in
let pas = def_option a.proof_state attempt_status in
let ngoal = def_option a.proof_parent goal in
let nprover = match prover with
......@@ -1221,7 +1229,7 @@ let copy_external_proof
Some (dst_file)
in
add_external_proof ?notify ~keygen
~obsolete ~archived ~timelimit ~edit ngoal nprover pas
~obsolete ~archived ~timelimit ~memlimit ~edit ngoal nprover pas
exception UnloadableProver of Whyconf.prover
......@@ -1274,10 +1282,10 @@ let print_attempt_status fmt = function
| InternalFailure _ -> pp_print_string fmt "Failure"
let print_external_proof fmt p =
fprintf fmt "%a - %a (%i)%s%s%s"
fprintf fmt "%a - %a (%i, %i)%s%s%s"
Whyconf.print_prover p.proof_prover
print_attempt_status p.proof_state
p.proof_timelimit
p.proof_timelimit p.proof_memlimit
(if p.proof_obsolete then " obsolete" else "")
(if p.proof_archived then " archived" else "")
(if p.proof_edited_as <> None then " edited" else "")
......@@ -1607,6 +1615,7 @@ let merge_proof ~keygen obsolete to_goal _ from_proof =
~obsolete:(obsolete || from_proof.proof_obsolete)
~archived:from_proof.proof_archived
~timelimit:from_proof.proof_timelimit
~memlimit:from_proof.proof_memlimit
~edit:from_proof.proof_edited_as
to_goal
from_proof.proof_prover
......
......@@ -84,6 +84,7 @@ and 'a proof_attempt = private
proof_parent : 'a goal;
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_memlimit : int;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
......@@ -267,6 +268,7 @@ val add_external_proof :
obsolete:bool ->
archived:bool ->
timelimit:int ->
memlimit:int ->
edit:string option ->
'key goal ->
Whyconf.prover ->
......@@ -300,6 +302,7 @@ val update_edit_external_proof :
val set_timelimit : int -> 'key proof_attempt -> unit
val set_memlimit : int -> 'key proof_attempt -> unit
val copy_external_proof :
?notify:'key notify ->
......@@ -307,6 +310,7 @@ val copy_external_proof :
?obsolete:bool ->
?archived:bool ->
?timelimit:int ->
?memlimit:int ->
?edit:string option ->
?goal:'key goal ->
?prover:Whyconf.prover ->
......
......@@ -458,6 +458,7 @@ let run_external_proof eS eT ?callback a =
begin
let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
let timelimit = adapt_timelimit a in
let memlimit = a.proof_memlimit in
let callback result =
begin match result with
| Undone Interrupted ->
......@@ -486,7 +487,7 @@ let run_external_proof eS eT ?callback a =
npc.prover_config.Whyconf.extra_options) in
(* eprintf "scheduling it...@."; *)
schedule_proof_attempt
~timelimit ~memlimit:0
~timelimit ~memlimit
?old ~command
~driver:npc.prover_driver
~callback
......@@ -494,15 +495,16 @@ let run_external_proof eS eT ?callback a =
(goal_task g)
end
let prover_on_goal eS eT ?callback ~timelimit p g =
let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
set_timelimit timelimit a;
set_memlimit memlimit a;
a
with Not_found ->
let ep = add_external_proof ~keygen:O.create ~obsolete:false
~archived:false ~timelimit
~archived:false ~timelimit ~memlimit
~edit:None g p (Undone Interrupted) in
O.init ep.proof_key (Proof_attempt ep);
ep
......@@ -510,35 +512,35 @@ let prover_on_goal eS eT ?callback ~timelimit p g =
run_external_proof eS eT ?callback a
let prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit p g =
~context_unproved_goals_only ~timelimit ~memlimit p g =
goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
(prover_on_goal eS eT ~timelimit p) g
(prover_on_goal eS eT ~timelimit ~memlimit p) g
let run_prover eS eT ~context_unproved_goals_only ~timelimit pr a =
let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
match a with
| Goal g ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit pr g
~context_unproved_goals_only ~timelimit ~memlimit pr g
| Theory th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit pr)
~context_unproved_goals_only ~timelimit ~memlimit pr)
th.theory_goals
| File file ->
List.iter
(fun th ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit pr)
~context_unproved_goals_only ~timelimit ~memlimit pr)
th.theory_goals)
file.file_theories
| Proof_attempt a ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit pr a.proof_parent
~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent
| Transf tr ->
List.iter
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit pr)
~context_unproved_goals_only ~timelimit ~memlimit pr)
tr.transf_goals
(**********************************)
......@@ -692,6 +694,7 @@ let check_external_proof eS eT todo a =
a in
*)
let timelimit = adapt_timelimit a in
let memlimit = a.proof_memlimit in
let callback result =
match result with
| Undone Scheduled | Undone Running | Undone Interrupted -> ()
......@@ -725,7 +728,7 @@ let check_external_proof eS eT todo a =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt eT
~timelimit ~memlimit:0
~timelimit ~memlimit
?old ~command
~driver:npc.prover_driver
~callback
......@@ -752,7 +755,7 @@ let check_all eS eT ~callback =
(* play all *)
(***********************************)
let rec play_on_goal_and_children eS eT ~timelimit todo l g =
let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
let callback _key status =
match status with
| Undone Running | Undone Scheduled -> ()
......@@ -766,24 +769,24 @@ let rec play_on_goal_and_children eS eT ~timelimit todo l g =
(* eprintf "todo increased to %d@." todo.Todo.todo; *)
(* eprintf "prover %a on goal %s@." *)
(* Whyconf.print_prover p g.goal_name.Ident.id_string; *)
prover_on_goal eS eT ~callback ~timelimit p g)
prover_on_goal eS eT ~callback ~timelimit ~memlimit p g)
l;
PHstr.iter
(fun _ t ->
List.iter
(play_on_goal_and_children eS eT ~timelimit todo l)
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
t.transf_goals)
g.goal_transformations
let play_all eS eT ~callback ~timelimit l =
let play_all eS eT ~callback ~timelimit ~memlimit l =
let todo = Todo.create (ref ()) (fun _ _ -> ()) in
PHstr.iter
(fun _ file ->
List.iter
(fun th ->
List.iter
(play_on_goal_and_children eS eT ~timelimit todo l)
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
th.theory_goals)
file.file_theories)
eS.session.session_files;
......
......@@ -77,9 +77,9 @@ module type OBSERVER = sig
proof_attempt is replaced *)
*)
val uninstalled_prover :
val uninstalled_prover :
key env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
(** When a prover must be called on a task but it is currently
(** When a prover must be called on a task but it is currently
not installed, what policy to apply *)
end
......@@ -120,7 +120,8 @@ module Make(O: OBSERVER) : sig
val run_prover :
O.key env_session -> t ->
context_unproved_goals_only:bool ->
timelimit:int -> Whyconf.prover -> O.key any -> unit
timelimit:int -> memlimit:int ->
Whyconf.prover -> O.key any -> unit
(** [run_prover es sched p a] runs prover [p] on all goals under [a]
the proof attempts are only scheduled for running, and they
will be started asynchronously when processors are available.
......@@ -141,7 +142,8 @@ module Make(O: OBSERVER) : sig
val prover_on_goal :
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
timelimit:int -> Whyconf.prover -> O.key goal -> unit
timelimit:int -> memlimit:int ->
Whyconf.prover -> O.key goal -> unit
(** [prover_on_goal es sched ?timelimit p g] same as
{!redo_external_proof} but create or reuse existing proof_attempt
*)
......@@ -231,7 +233,7 @@ module Make(O: OBSERVER) : sig
val play_all :
O.key env_session -> t -> callback:(unit-> unit) ->
timelimit:int -> Whyconf.prover list -> unit
timelimit:int -> memlimit:int -> Whyconf.prover list -> unit
(** [play_all es sched l] runs every prover of list [l] on all
goals and sub-goals of the session, with the given time limit.
[callback] is called when all tasks are finished.
......
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