Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 414a7182 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

The "steplimit" feature is now used only when option -use-steps is given

on the command line (for the "replay" command)

This is to avoid recurrent replay error from Alt-Ergo, that does
not reliably replay a proof with the same number of steps
parent a3155c0a
......@@ -294,7 +294,7 @@ let schedule_edition t command filename callback =
Call_provers.prp_regexps = [];
Call_provers.prp_timeregexps = [];
Call_provers.prp_stepregexps = [];
Call_provers.prp_model_parser = fun _ _ -> Model_parser.empty_model
Call_provers.prp_model_parser = fun _ _ -> Model_parser.empty_model
} in
let precall =
Call_provers.call_on_file ~command ~res_parser ~redirect:false filename ~printer_mapping:Printer.get_default_printer_mapping in
......@@ -399,10 +399,11 @@ 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 a =
let adapt_limits ~use_steps a =
match a.proof_state with
| Done { Call_provers.pr_answer = r;
Call_provers.pr_time = t } ->
Call_provers.pr_time = t;
Call_provers.pr_steps = s } ->
(* 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 *)
......@@ -414,18 +415,23 @@ let adapt_limits a =
let increased_mem = 3 * a.proof_memlimit / 2 in
begin
match r with
| Call_provers.OutOfMemory -> increased_time, a.proof_memlimit
| Call_provers.Timeout -> a.proof_timelimit, increased_mem
| Call_provers.StepLimitExceeded
| Call_provers.Valid
| Call_provers.OutOfMemory -> increased_time, a.proof_memlimit, -1
| Call_provers.Timeout -> a.proof_timelimit, increased_mem, -1
| Call_provers.Valid ->
let steplimit =
if use_steps && not a.proof_obsolete then s else -1
in
increased_time, increased_mem, steplimit
| Call_provers.Unknown _
| Call_provers.Invalid -> increased_time, increased_mem
| Call_provers.StepLimitExceeded
| Call_provers.Invalid -> increased_time, increased_mem, -1
| Call_provers.Failure _
| Call_provers.HighFailure ->
(* correct ? failures are supposed to appear quickly anyway... *)
a.proof_timelimit, a.proof_memlimit
a.proof_timelimit, a.proof_memlimit, -1
end
| _ -> a.proof_timelimit, a.proof_memlimit
| _ -> a.proof_timelimit, a.proof_memlimit, -1
type run_external_status =
......@@ -451,7 +457,7 @@ let dummy_limits = (0,0,0)
(** run_external_proof_v3 doesn't modify existing proof attempt, it can just
create new one by find_prover *)
let run_external_proof_v3 eS eT a ?(cntexample=false) callback =
let run_external_proof_v3 ~use_steps eS eT a ?(cntexample=false) callback =
match find_prover eS a with
| None ->
callback a a.proof_prover dummy_limits None Starting;
......@@ -465,15 +471,7 @@ let run_external_proof_v3 eS eT a ?(cntexample=false) callback =
callback a ap dummy_limits None (MissingFile "unedited")
end else begin
let previous_result = a.proof_state in
let timelimit, memlimit = adapt_limits a in
let steplimit =
match a with
| { proof_state =
Done { Call_provers.pr_answer = Call_provers.Valid;
Call_provers.pr_steps = s };
proof_obsolete = false } when s >= 0 -> s
| _ -> -1
in
let timelimit, memlimit, steplimit = adapt_limits ~use_steps a in
let inplace = npc.prover_config.Whyconf.in_place in
let command = Whyconf.get_complete_command npc.prover_config steplimit in
let cb result =
......@@ -500,7 +498,7 @@ let run_external_proof_v3 eS eT a ?(cntexample=false) callback =
end
(** run_external_proof_v2 modify the session according to the current state *)
let run_external_proof_v2 eS eT a ~cntexample callback =
let run_external_proof_v2 ~use_steps eS eT a ~cntexample callback =
let previous_res = ref (a.proof_state,a.proof_obsolete) in
let callback a ap limits previous state =
begin match state with
......@@ -522,17 +520,17 @@ let run_external_proof_v2 eS eT a ~cntexample callback =
end;
callback a ap limits previous state
in
run_external_proof_v3 eS eT a ~cntexample callback
run_external_proof_v3 ~use_steps eS eT a ~cntexample callback
let running = function
| Scheduled | Running -> true
| Unedited | JustEdited | Interrupted
| Done _ | InternalFailure _ -> false
let run_external_proof_v2 eS eT a ?(cntexample=false) callback =
let run_external_proof_v2 ~use_steps eS eT a ?(cntexample=false) callback =
(* Perhaps the test a.proof_archived should be done somewhere else *)
if a.proof_archived || running a.proof_state then () else
run_external_proof_v2 eS eT a ~cntexample callback
run_external_proof_v2 ~use_steps eS eT a ~cntexample callback
let run_external_proof eS eT ?(cntexample=false) ?callback a =
let callback =
......@@ -545,7 +543,7 @@ let run_external_proof eS eT ?(cntexample=false) ?callback a =
| MissingFile _ -> c a a.proof_state
| StatusChange s -> c a s
in
run_external_proof_v2 eS eT a ~cntexample callback
run_external_proof_v2 ~use_steps:false eS eT a ~cntexample callback
let prover_on_goal eS eT ?callback ?(cntexample=false) ~timelimit ~memlimit p g =
let a =
......@@ -628,7 +626,7 @@ type report =
let push_report report (g,p,limits,r) =
(g.goal_name,p,limits,r)::report
let check_external_proof eS eT todo a =
let check_external_proof ~use_steps eS eT todo a =
let callback a ap limits old s =
let g = a.proof_parent in
match s with
......@@ -648,7 +646,7 @@ let check_external_proof eS eT todo a =
| None -> No_former_result res
| Some old -> Result (res, old) in
Todo._done todo (g, ap, limits, r) in
run_external_proof_v2 eS eT a callback
run_external_proof_v2 ~use_steps eS eT a callback
let rec goal_iter_proof_attempt_with_release ~release f g =
let iter g = goal_iter_proof_attempt_with_release ~release f g in
......@@ -657,7 +655,7 @@ let rec goal_iter_proof_attempt_with_release ~release f g =
Mmetas_args.iter (fun _ t -> iter t.metas_goal) g.goal_metas;
if release then release_task g
let check_all ?(release=false) ?filter eS eT ~callback =
let check_all ?(release=false) ~use_steps ?filter eS eT ~callback =
Debug.dprintf debug "[Sched] check all@.%a@." print_session eS.session;
let todo = Todo.create [] push_report callback in
Todo.start todo;
......@@ -666,7 +664,7 @@ let check_all ?(release=false) ?filter eS eT ~callback =
let c = match filter with
| None -> true
| Some f -> f a in
if c then check_external_proof eS eT todo a in
if c then check_external_proof ~use_steps eS eT todo a in
goal_iter_proof_attempt_with_release ~release check g
in
PHstr.iter (fun _ file ->
......
......@@ -140,7 +140,7 @@ module Make(O: OBSERVER) : sig
will be started asynchronously when processors are available.
~context_unproved_goals_only indicates if prover must be run
on already proved goals or not
on already proved goals or not
~cntexample indicates if prover should be asked to get counter-example
model
*)
......@@ -152,7 +152,7 @@ module Make(O: OBSERVER) : sig
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
O.key proof_attempt -> unit
(** [run_external_proof es sched ?cntexample ?callback p] reruns an existing
proof attempt [p]
proof attempt [p]
~cntexample indicates if prover should be asked to get counter-example
model
......@@ -166,6 +166,7 @@ module Make(O: OBSERVER) : sig
| StatusChange of proof_attempt_status
val run_external_proof_v3 :
use_steps:bool ->
O.key Session.env_session -> t -> O.key Session.proof_attempt ->
?cntexample : bool ->
(O.key Session.proof_attempt -> Whyconf.prover ->
......@@ -176,8 +177,8 @@ module Make(O: OBSERVER) : sig
status]. run_external_proof_v3 don't change the existing proof
attempt just can add new by O.uninstalled_prover. Be aware since
the session is not modified there is no test to see if the
proof_attempt had already been started
proof_attempt had already been started
?cntexample indicates if prover should be asked to get counter-example
model
*)
......@@ -191,7 +192,7 @@ module Make(O: OBSERVER) : sig
Whyconf.prover -> O.key goal -> unit
(** [prover_on_goal es sched ?cntexample ?timelimit p g] same as
{!redo_external_proof} but creates or reuses existing proof_attempt
?cntexample indicates if prover should be asked to get counter-example
model
*)
......@@ -283,6 +284,7 @@ module Make(O: OBSERVER) : sig
val check_all:
?release:bool -> (** Can all the goals be released at the end? def: false *)
use_steps:bool -> (** Replay use recorded number of proof steps *)
?filter:(O.key proof_attempt -> bool) ->
O.key env_session -> t ->
callback:((Ident.ident * Whyconf.prover * (int * int * int) * report) list -> unit) ->
......
......@@ -38,6 +38,7 @@ let opt_file = ref None
let opt_stats = ref true
let opt_force = ref false
let opt_obsolete_only = ref false
let opt_use_steps = ref false
let opt_bench = ref false
let opt_provers = ref []
......@@ -71,6 +72,9 @@ let option_list = [
("--force",
Arg.Set opt_force,
" same as -f");
("--use-steps",
Arg.Set opt_use_steps,
" replay using recorded number of proof steps (when possible)");
("--obsolete-only",
Arg.Set opt_obsolete_only,
" replay only if session is obsolete") ;
......@@ -316,13 +320,15 @@ let add_to_check_no_smoke config some_merge_miss found_obs env_session sched =
end
in
if !opt_provers = [] then
M.check_all ~release:true ~callback env_session sched
M.check_all ~release:true ~use_steps:!opt_use_steps
~callback env_session sched
else
let filter a =
List.exists
(fun p -> Whyconf.filter_prover p a.Session.proof_prover)
!opt_provers in
M.check_all ~release:true ~filter ~callback env_session sched
M.check_all ~release:true ~use_steps:!opt_use_steps
~filter ~callback env_session sched
let add_to_check_smoke env_session sched =
let callback report =
......@@ -346,7 +352,8 @@ let add_to_check_smoke env_session sched =
exit 1
end
in
M.check_all ~release:true ~callback env_session sched
M.check_all ~release:true ~use_steps:!opt_use_steps
~callback env_session sched
let add_to_check config some_merge_miss found_obs =
match !opt_smoke with
......@@ -358,7 +365,7 @@ let add_to_check config some_merge_miss found_obs =
let transform_smoke env_session =
let trans tr_name s =
Session_tools.filter_proof_attempt
Session_tools.filter_proof_attempt
(fun p -> Opt.inhabited (S.proof_verified p)) s.S.session;
Session_tools.transform_proof_attempt ~keygen:O.create s tr_name
in
......
......@@ -305,13 +305,13 @@ let run_one sched env config filters interactive_provers fname =
let checkyn = ask_yn_nonblock ~callback:(fun b ->
if b then
let callback_edit pa =
M.run_external_proof_v3
env_session sched pa
M.run_external_proof_v3 ~use_steps:false
env_session sched pa
callback in
M.edit_proof_v3 env_session sched
~cntexample:false
~default_editor:"" (** TODO? *)
~callback:callback_edit a
~callback:callback_edit a
else
Todo.stop todo;
if not (Queue.is_empty to_edit_queue) then
......@@ -320,7 +320,7 @@ let run_one sched env config filters interactive_provers fname =
) in
O.timeout ~ms:100 checkyn
in
M.run_external_proof_v3 env_session sched pr callback
M.run_external_proof_v3 ~use_steps:false env_session sched pr callback
) stack;
Todo.stop todo
......
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