Commit d098414b authored by MARCHE Claude's avatar MARCHE Claude

cleaning

parent fcb44a61
......@@ -63,52 +63,14 @@ 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
module Make(O : OBSERVER) = struct
let notify = O.notify
let rec init_any any =
O.init (key_any any) any;
iter init_any any
let init_session session = session_iter init_any session
(***************************)
(* session state *)
(***************************)
(* type prover_option = *)
(* | Detected_prover of prover_data *)
(* | Undetected_prover of string *)
(* let prover_id p = match p with *)
(* | Detected_prover p -> p.prover_id *)
(* | Undetected_prover s -> s *)
(* dead code
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.theory_verified
let goals t = t.theory_goals
let theory_expanded t = t.theory_expanded
*)
let running = function
| Scheduled | Running -> true
| Unedited | JustEdited | Interrupted
| Done _ | InternalFailure _ -> false
module Make(O : OBSERVER) = struct
(*************************)
(* Scheduler *)
......@@ -119,7 +81,6 @@ type action =
Driver.driver * (proof_attempt_status -> unit) * Task.task
| Action_delayed of (unit -> unit)
type timeout_action =
| Check_prover of (proof_attempt_status -> unit) * Call_provers.prover_call
| Any_timeout of (unit -> bool)
......@@ -147,7 +108,7 @@ type t =
}
let set_maximum_running_proofs max sched =
(** TODO dequeue actions if maximum_running_proofs increase *)
(* TODO dequeue actions if maximum_running_proofs increase *)
sched.maximum_running_proofs <- max
let init max =
......@@ -228,16 +189,19 @@ let schedule_any_timeout t callback =
t.running_proofs <- (Any_timeout callback) :: t.running_proofs;
run_timeout_handler t
(* unused
let schedule_check t callback =
Debug.dprintf debug "[Sched] add a new check@.";
t.running_check <- callback :: t.running_check;
run_timeout_handler t
*)
(* idle handler *)
let idle_handler t =
try
if Queue.length t.proof_attempts_queue < 3 * t.maximum_running_proofs then begin
if Queue.length t.proof_attempts_queue < 3 * t.maximum_running_proofs then
begin
match Queue.pop t.actions_queue with
| Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
callback,goal) ->
......@@ -250,19 +214,21 @@ let idle_handler t =
Queue.push (callback,pre_call) t.proof_attempts_queue;
run_timeout_handler t
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf "@[Exception raise in Session.idle_handler:@ \
%a@.@]"
Format.eprintf
"@[Exception raise in Session.idle_handler:@ %a@.@]"
Exn_printer.exn_printer e;
callback (InternalFailure e)
end
| Action_delayed callback -> callback ()
end else
end
else
ignore (Unix.select [] [] [] 0.1);
true
with Queue.Empty ->
t.idle_handler_activated <- false;
Debug.dprintf debug "[Sched] idle_handler stopped@.";
false
with
| Queue.Empty ->
t.idle_handler_activated <- false;
Debug.dprintf debug "[Sched] idle_handler stopped@.";
false
| e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
Exn_printer.exn_printer e;
......@@ -331,14 +297,21 @@ let schedule_delayed_action t callback =
run_idle_handler t
(**************************)
(* session function *)
(* session functions *)
(**************************)
let notify = O.notify
let rec init_any any = O.init (key_any any) any; iter init_any any
let init_session session = session_iter init_any session
let update_session ?release ~allow_obsolete old_session env whyconf =
O.reset ();
let (env_session,_,_) as res =
update_session ?release
~keygen:O.create ~allow_obsolete old_session env whyconf in
~keygen:O.create ~allow_obsolete old_session env whyconf
in
Debug.dprintf debug "Init_session@\n";
init_session env_session.session;
res
......@@ -353,18 +326,6 @@ let add_file env_session ?format 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
| None -> begin
(** If its not loadable ask for one*)
match O.unknown_prover eS prover with
| None -> None
| 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
......@@ -533,6 +494,11 @@ let run_external_proof_v2 eS eT a callback =
callback a ap timelimit previous state in
run_external_proof_v3 eS eT a callback
let running = function
| Scheduled | Running -> true
| Unedited | JustEdited | Interrupted
| Done _ | InternalFailure _ -> false
let run_external_proof_v2 eS eT a callback =
(* Perhaps the test a.proof_archived should be done somewhere else *)
if a.proof_archived || running a.proof_state then () else
......@@ -709,11 +675,6 @@ let check_external_proof eS eT todo a =
Todo._done todo (g, ap, tl, r) in
run_external_proof_v2 eS eT a callback
(* dead code
let check_goal_and_children eS eT todo g =
goal_iter_proof_attempt (check_external_proof eS eT todo) g
*)
let rec goal_iter_proof_attempt_with_release ~release f g =
let iter g = goal_iter_proof_attempt_with_release ~release f g in
PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
......@@ -852,32 +813,6 @@ let edit_proof_v3 eS sched ~default_editor callback a =
*)
()
| Some(_,npc,a) ->
(*
let ap = a.proof_prover in
match find_loadable_prover eS a.proof_prover with
| None -> ()
(** Perhaps a new prover *)
| Some (nap,npc) ->
let g = a.proof_parent in
try
if nap == ap then raise Not_found;
let np_a = PHprover.find g.goal_external_proofs nap in
if O.replace_prover np_a a then begin
(** The notification will be done by the new proof_attempt *)
O.remove np_a.proof_key;
raise Not_found end
with Not_found ->
(** replace [a] by a new_proof attempt if [a.proof_prover] was not
loadable *)
let a = if nap == ap then a
else
let a = copy_external_proof
~notify ~keygen:O.create ~prover:nap ~env_session:eS a in
O.init a.proof_key (Proof_attempt a);
a in
(** Now [a] is a proof_attempt of the lodable prover [nap] *)
*)
let editor =
match npc.prover_config.Whyconf.editor with
| "" -> default_editor
......
......@@ -9,11 +9,10 @@
(* *)
(********************************************************************)
open Why3
(** Scheduling operations on sessions and calls to provers *)
(*** One module for calling callback when it's time to *)
(** {2 One module for calling callback when it's time to} *)
module Todo : sig
type ('a,'b) todo
......@@ -31,8 +30,7 @@ module Todo : sig
end
(** Proof sessions *)
open Why3
open Session
(** {2 Observers signature} *)
......@@ -76,31 +74,20 @@ module type OBSERVER = sig
val notify : key any -> unit
(** notify modification of node of the session *)
(*
val unknown_prover : key env_session -> Whyconf.prover ->
Whyconf.prover option
(** When a prover must be called on a task but it is currently
unknown another prover can be used instead. (the proof_attempt
will have the new prover) *)
val replace_prover : key proof_attempt -> key proof_attempt -> bool
(** If the previous function give a prover which already have a
proof attempt attached to the goal, this function is fired. If
[replace_prover to_be_removed to_be_copied] return [true] the
proof_attempt is replaced *)
*)
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
not installed, what policy to apply *)
end
(** {2 Main functor} *)
module Make(O: OBSERVER) : sig
(** A session, with the environment, and the configuration *)
(** {2 Scheduler} *)
type t (** the scheduler environment *)
val set_maximum_running_proofs : int -> t -> unit
......@@ -108,10 +95,20 @@ module Make(O: OBSERVER) : sig
val init : int -> t
(** [init max] *)
(** {2 static state of a session} *)
(* not used
val schedule_check: t -> (unit -> bool) -> unit
(** test the check time to time, reschedule it if it returns true *)
*)
(* used by why3session_run, but it should not as it is a low-level scheduler
function *)
val schedule_any_timeout: t -> (unit -> bool) -> unit
(** run it when an action slot/worker/cpu is available. Reschedule it if it
return true *)
(** {2 Save and load a state} *)
(** {2 Save and load a state} *)
val update_session :
?release:bool ->
......@@ -141,24 +138,23 @@ module Make(O: OBSERVER) : sig
the proof attempts are only scheduled for running, and they
will be started asynchronously when processors are available.
~context_unproved_goals_only indicates if verified goals must be
discarded
*)
~context_unproved_goals_only indicates if prover must be run
on already proved goals or not *)
val run_external_proof :
O.key env_session -> t ->
?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
O.key proof_attempt -> unit
(** [redo_external_proof es sched ?timelimit p g] run
*)
(** [run_external_proof es sched ?callback p] reruns an existing
proof attempt [p] *)
type run_external_status =
| Starting
| MissingProver
| MissingFile of string
| StatusChange of proof_attempt_status
| Starting
| MissingProver
| MissingFile of string
| StatusChange of proof_attempt_status
val run_external_proof_v3 :
O.key Session.env_session -> t -> O.key Session.proof_attempt ->
......@@ -170,7 +166,7 @@ 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 be started *)
proof_attempt had already been started *)
val prover_on_goal :
......@@ -179,7 +175,7 @@ module Make(O: OBSERVER) : sig
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
{!redo_external_proof} but creates or reuses existing proof_attempt
*)
......@@ -198,7 +194,7 @@ module Make(O: OBSERVER) : sig
(** [transform es sched tr g] applies registered
transformation [tr] on the given goal.
If keep_dumb_transformation is false (default)
If [keep_dumb_transformation] is false (default)
and the transformation gives one task equal to [g]
the transformation is not added (the callback is called with None).
Otherwise the transformation is added and given to the callback.
......@@ -213,27 +209,26 @@ module Make(O: OBSERVER) : sig
(** [transform es sched tr a] applies registered
transformation [tr] on all leaf goals under [a].
~context_unproved_goals_only indicates if verified goals must be
discarded
*)
[~context_unproved_goals_only] indicates if the transformation
must be applied also on alreadt proved goals *)
val edit_proof :
O.key env_session -> t ->
default_editor:string ->
O.key proof_attempt -> unit
(** edit the given proof attempt using the appropriate editor *)
(** edits the given proof attempt using the appropriate editor *)
val edit_proof_v3 :
O.key env_session -> t ->
default_editor:string ->
callback:(O.key Session.proof_attempt -> unit) ->
O.key proof_attempt -> unit
(** edit the given proof attempt using the appropriate editor but don't
modify the session *)
(** edits the given proof attempt using the appropriate editor but
don't modify the session *)
val cancel : O.key any -> unit
(** [cancel a] marks all proofs under [a] as obsolete *)
(** [cancel a] marks all proofs under [a] as obsolete *)
val remove_proof_attempt : O.key proof_attempt -> unit
......@@ -262,13 +257,13 @@ module Make(O: OBSERVER) : sig
context_unproved_goals_only:bool -> O.key any -> unit
(** [replay es sched ~obsolete_only ~context_unproved_goals_only a]
reruns proofs under [a]
if obsolete_only is set then does not rerun non-obsolete proofs
if context_unproved_goals_only is set then don't rerun proofs
already 'valid'
if [obsolete_only] is set then does not rerun non-obsolete proofs
if [context_unproved_goals_only] is set then don't rerun proofs
already 'valid' (FIXME: its the opposite, no?)
*)
val check_all:
?release:bool -> (** Can all the goal be release at the end? def: false *)
?release:bool -> (** Can all the goals be released at the end? def: false *)
?filter:(O.key proof_attempt -> bool) ->
O.key env_session -> t ->
callback:((Ident.ident * Whyconf.prover * int * report) list -> unit) ->
......@@ -300,13 +295,6 @@ module Make(O: OBSERVER) : sig
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
val schedule_check: t -> (unit -> bool) -> unit
(** test the check time to time, reschedule it if it returns true *)
val schedule_any_timeout: t -> (unit -> bool) -> unit
(** run it when an action slot/worker/cpu is available. Reschedule it if it
return true *)
end
......
......@@ -163,22 +163,6 @@
</theory>
<theory name="NonTerm" expanded="true">
<goal name="g" sum="440373155c791eedfdbcd9785975a319" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g.1" expl="1." sum="ca724c1f318987fce7ceabe6e2557be7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g.1.1" expl="1." sum="99e17190190f38a7a4196a062c86c56a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g.1.1.1" expl="1." sum="a3a541f8601bdff948f870b1d53744a1" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g.1.1.1.1" expl="1." sum="78bcedde0f0ebdb60b12d26aae95fe2d">
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g3" sum="314ec6d25b740db3661c1f0f021c3a08" expanded="true">
<transf name="compute_in_goal" expanded="true">
......@@ -212,7 +196,11 @@
</goal>
<goal name="g8" sum="bd3022caac8d766e84e9626d267db4bf" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g8.1" expl="1." sum="cc3f72907e4480b8f31f994806a15bd6">
<goal name="g8.1" expl="1." sum="cc3f72907e4480b8f31f994806a15bd6" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g8.1.1" expl="1." sum="b24a5ce76c941ddc16a76c9202ea22e4">
</goal>
</transf>
</goal>
</transf>
</goal>
......
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