Commit 6ba6a9dc authored by Andrei Paskevich's avatar Andrei Paskevich

Session_scheduler: interactive provers do not get limits by default

However, we limit the execution time on replay.
parent fd40e931
......@@ -248,7 +248,7 @@ let actualcommand command limit file =
| "l" -> Config.libdir
| "d" -> Config.datadir
| "S" -> string_of_int limit.limit_steps
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
| _ -> failwith "unknown specifier, use %%, %f, %t, %m, %l, %d or %S"
in
let args =
List.map (Str.global_substitute cmd_regexp replace) arglist
......
......@@ -394,7 +394,7 @@ let find_prover eS a =
(* to avoid corner cases when prover results are obtained very closely
to the time or mem limits, we adapt these limits when we replay a
proof *)
let adapt_limits ~use_steps a =
let adapt_limits ~interactive ~use_steps a =
let timelimit = (a.proof_limit.Call_provers.limit_time) in
let memlimit = (a.proof_limit.Call_provers.limit_mem) in
match a.proof_state with
......@@ -404,12 +404,11 @@ let adapt_limits ~use_steps a =
(* increased time limit is 1 + twice the previous running time,
but enforced to remain inside the interval [l,2l] where l is
the previous time limit *)
let increased_time =
let t = truncate (1.0 +. 2.0 *. t) in
max timelimit (min t (2 * timelimit))
in
let increased_time = if interactive then t
else max timelimit (min t (2 * timelimit)) in
(* increased mem limit is just 1.5 times the previous mem limit *)
let increased_mem = 3 * memlimit / 2 in
let increased_mem = if interactive then 0 else 3 * memlimit / 2 in
begin
match r with
| Call_provers.OutOfMemory -> increased_time, memlimit, 0
......@@ -427,10 +426,11 @@ let adapt_limits ~use_steps a =
(* correct ? failures are supposed to appear quickly anyway... *)
timelimit, memlimit, 0
end
| _ when interactive -> 0, 0, 0
| _ -> timelimit, memlimit, 0
let adapt_limits ~use_steps a =
let t, m, s = adapt_limits ~use_steps a in
let adapt_limits ~interactive ~use_steps a =
let t, m, s = adapt_limits ~interactive ~use_steps a in
{ Call_provers.limit_time = t; limit_mem = m; limit_steps = s }
type run_external_status =
......@@ -462,13 +462,12 @@ let run_external_proof_v3 ~use_steps eS eT a ?(cntexample=false) callback =
callback a a.proof_prover Call_provers.empty_limit None MissingProver
| Some(ap,npc,a) ->
callback a ap Call_provers.empty_limit None Starting;
if a.proof_edited_as = None &&
npc.prover_config.Whyconf.interactive
then begin
let itp = npc.prover_config.Whyconf.interactive in
if itp && a.proof_edited_as = None then begin
callback a ap Call_provers.empty_limit None (MissingFile "unedited")
end else begin
let previous_result = a.proof_state in
let limit = adapt_limits ~use_steps a in
let limit = adapt_limits ~interactive:itp ~use_steps a in
let inplace = npc.prover_config.Whyconf.in_place in
let command =
Whyconf.get_complete_command npc.prover_config
......
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