...
  View open merge request
Commits (1)
......@@ -42,6 +42,7 @@ type prover_result = {
}
(* END{proverresult} anchor for automatic documentation, do not remove *)
(* BEGIN{resourcelimit} anchor for automatic documentation, do not remove *)
type resource_limit = {
limit_time : int;
......@@ -464,6 +465,7 @@ type prover_update =
| InternalFailure of exn
| ProverStarted
| ProverFinished of prover_result
| CacheMiss
let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17
......
......@@ -170,6 +170,7 @@ type prover_update =
| InternalFailure of exn
| ProverStarted
| ProverFinished of prover_result
| CacheMiss
val get_new_results: blocking:bool -> (prover_call * prover_update) list
(** returns new results from why3server, in an unordered fashion. *)
......
......@@ -49,6 +49,12 @@ let default_conf_file =
| None -> Filename.concat (Rc.get_home_dir ()) ".why3.conf"
| Some d -> Filename.concat d "why3.conf"
let default_cache_dir =
match Config.localdir with
| None -> Filename.concat (Rc.get_home_dir ()) ".why3.cache"
| Some d -> Filename.concat d "why3.cache"
(* Prover *)
(* BEGIN{provertype} anchor for automatic documentation, do not remove *)
......@@ -174,6 +180,11 @@ let set_strategies rc strategies =
(** Main record *)
type cache_mode =
| Cache_none
| Cache_use
| Cache_record
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
......@@ -188,6 +199,12 @@ type main = {
(* plugins to load, without extension, relative to [libdir]/plugins *)
default_editor : string;
(* editor name used when no specific editor known for a prover *)
use_cache: bool;
(* Use the cache information *)
update_cache: bool;
(* Use the cache information *)
cache_dir: string;
(* cache directory to use *)
}
let libdir m =
......@@ -235,6 +252,9 @@ let get_complete_command pc ~with_steps =
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
let cache_mode m = m.cache_mode
let set_cache_mode m cache_mode = { m with cache_mode }
let set_default_editor m e = { m with default_editor = e }
let plugins m = m.plugins
......@@ -278,6 +298,8 @@ let empty_main =
plugins = [];
default_editor = (try Sys.getenv "EDITOR" ^ " %f"
with Not_found -> "editor %f");
cache_mode = Cache_none;
cache_dir = default_cache_dir;
}
let default_main =
......@@ -538,6 +560,13 @@ let load_main dirname section =
section "running_provers_max";
plugins = get_stringl ~default:[] section "plugin";
default_editor = get_string ~default:default_main.default_editor section "default_editor";
cache_mode = begin match get_stringo section "cache_mode" with
| None -> default_main.cache_mode
| Some "none" -> Cache_node
| Some "yes" -> Cache_yes
| Some "only" -> Cache_only
end;
cache_dir = get_string ~default:default_main.cache_dir section "cache_dir";
}
let read_config_rc conf_file =
......
......@@ -79,6 +79,15 @@ val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main
type cache_mode =
| Cache_none
| Cache_yes
| Cache_only
val cache_mode: main -> cache_mode
val set_cache_mode: main -> cache_mode -> main
val default_editor: main -> string
(** editor name used when no specific editor known for a prover *)
val set_default_editor: main -> string -> main
......
......@@ -1392,6 +1392,7 @@ let on_selected_row r =
| Controller_itp.Undone -> "no result known"
| Controller_itp.Detached -> "detached proof attempt: parent goal has no task"
| Controller_itp.Interrupted -> "prover run was interrupted"
| Controller_itp.CacheMiss -> "prover call is deactivated and the call is not in the cache"
| Controller_itp.Scheduled -> "proof scheduled but not running yet"
| Controller_itp.Running -> "prover currently running"
| Controller_itp.InternalFailure e ->
......@@ -1605,7 +1606,8 @@ let is_selected_alone id =
let image_of_pa_status ~obsolete pa =
match pa with
| Controller_itp.Undone
| Controller_itp.Interrupted -> !image_undone
| Controller_itp.Interrupted
| Controller_itp.CacheMiss -> !image_undone
| Controller_itp.Scheduled -> !image_scheduled
| Controller_itp.Running -> !image_running
| Controller_itp.InternalFailure _e -> !image_failure
......@@ -1702,6 +1704,7 @@ let set_status_and_time_column ?limit row =
| C.InternalFailure _ -> "(internal failure)"
| C.Interrupted -> "(interrupted)"
| C.Undone -> "(undone)"
| C.CacheMiss -> "(cachemiss)"
| C.Uninstalled _ -> "(uninstalled prover)"
| C.UpgradeProver _ -> "(upgraded prover)"
| C.Removed _ -> "(removed prover)"
......
......@@ -32,6 +32,7 @@ type proof_attempt_status =
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
| Removed of Whyconf.prover (** prover has been removed or upgraded *)
| CacheMiss (** prover has been removed or upgraded *)
let print_status fmt st =
match st with
......@@ -42,6 +43,7 @@ let print_status fmt st =
fprintf fmt "Done(%a)"
(Call_provers.print_prover_result ~json_model:false) r
| Interrupted -> fprintf fmt "Interrupted"
| CacheMiss -> fprintf fmt "CacheMiss"
| Detached -> fprintf fmt "Detached"
| InternalFailure e ->
fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e
......@@ -450,6 +452,10 @@ let timeout_handler () =
if Hashtbl.length prover_tasks_in_progress != 0 then begin
let results = Call_provers.get_new_results ~blocking:S.blocking in
List.iter (fun (call, prover_update) ->
let end_run ptp =
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
in
match Hashtbl.find prover_tasks_in_progress call with
| ptp ->
begin match prover_update with
......@@ -461,19 +467,20 @@ let timeout_handler () =
Hashtbl.replace prover_tasks_in_progress ptp.tp_call
{ptp with tp_started = true}
| Call_provers.ProverFinished res ->
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
end_run ptp;
let res = Opt.fold fuzzy_proof_time res ptp.tp_ores in
(* inform the callback *)
ptp.tp_callback (Done res)
| Call_provers.ProverInterrupted ->
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
end_run ptp;
(* inform the callback *)
ptp.tp_callback (Interrupted)
| Call_provers.CacheMiss ->
end_run ptp;
(* inform the callback *)
ptp.tp_callback (CacheMiss)
| Call_provers.InternalFailure exn ->
Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
if ptp.tp_started then decr number_of_running_provers;
end_run ptp;
(* inform the callback *)
ptp.tp_callback (InternalFailure (exn))
end
......@@ -578,6 +585,7 @@ let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
update_proof_attempt ~obsolete:false notification ses id pr res;
update_goal_node notification ses id
| Interrupted
| CacheMiss
| InternalFailure _ ->
Hpan.remove c.controller_running_proof_attempts panid;
(* what to do ?
......@@ -732,7 +740,7 @@ let schedule_edition c id pr ~callback ~notification =
print_proofAttemptID panid print_proofNodeID id;
update_proof_attempt ~obsolete:true notification session id pr res;
update_goal_node notification session id
| Interrupted
| Interrupted | CacheMiss
| InternalFailure _ ->
update_goal_node notification session id
| Undone | Detached | Uninstalled _ | Scheduled | Removed _ -> assert false
......@@ -811,7 +819,7 @@ let run_strategy_on_goal
| Done { Call_provers.pr_answer = Call_provers.Valid } ->
(* proof succeeded, nothing more to do *)
callback STShalt
| Interrupted | InternalFailure _ ->
| Interrupted | CacheMiss | InternalFailure _ ->
callback STShalt
| Done _ ->
(* proof did not succeed, goto to next step *)
......@@ -1118,7 +1126,7 @@ let replay ~valid_only ~obsolete_only ?(use_steps=false) ?(filter=fun _ -> true)
found_upgraded_prover := true;
decr count
| Scheduled | Running -> ()
| Undone | Interrupted ->
| Undone | Interrupted | CacheMiss ->
decr count;
report := (id, pr, limits, Replay_interrupted ) :: !report
| Done new_r ->
......@@ -1263,7 +1271,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
begin match st with
| UpgradeProver _ | Scheduled | Running -> ()
| Detached | Uninstalled _ | Removed _ -> assert false
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| Undone | Interrupted | CacheMiss -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "Bisecting interrupted by an error %a.@."
......@@ -1335,7 +1343,7 @@ later on. We do has if proof fails. *)
debug "[Bisect] prover on subtask is running@.";
| Detached
| Uninstalled _ -> assert false
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| Undone | Interrupted | CacheMiss -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
Debug.dprintf debug "[Bisect] prover interrupted by an error: %a.@."
......
......@@ -27,6 +27,7 @@ type proof_attempt_status =
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
| Removed of Whyconf.prover (** prover has been removed or upgraded *)
| CacheMiss (** The call to provers has been deactivated and not in the cache *)
val print_status : Format.formatter -> proof_attempt_status -> unit
......
......@@ -1111,7 +1111,7 @@ end
P.notify (Node_change (node_id, Name_change n))
| Removed _ -> P.notify (Remove node_id); raise Return
| Uninstalled _ -> ()
| Undone | Scheduled | Running
| Undone | Scheduled | Running | CacheMiss
| Interrupted | Detached | Done _
| InternalFailure _ -> ()
end;
......
......@@ -87,7 +87,7 @@ let convert_proof_result (pr: prover_result) =
let convert_proof_attempt (pas: proof_attempt_status) =
Record (match pas with
| Undone ->
| Undone | CacheMiss ->
convert_record ["proof_attempt", String "Undone"]
| Interrupted ->
convert_record ["proof_attempt", String "Interrupted"]
......