From bcb1525fc7aab6f5e9ae23f4454a59983fea5bde Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Fri, 26 Aug 2016 15:59:40 +0200 Subject: [PATCH] why3shell in progress --- src/session/controller_itp.ml | 128 ++++++++++++++++++++++++++++++++- src/session/controller_itp.mli | 23 +++++- src/session/session_itp.mli | 24 +++++-- src/why3shell/why3shell.ml | 87 ++++++++++++++-------- 4 files changed, 223 insertions(+), 39 deletions(-) diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index 64f67cce1..0b954a12e 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -27,15 +27,139 @@ type transformation_status = module type Scheduler = sig val timeout: ms:int -> (unit -> bool) -> unit - val idle: (unit -> bool) -> unit + val idle: prio:int -> (unit -> bool) -> unit end module Make(S : Scheduler) = struct +let scheduled_proof_attempts = Queue.create () + +let prover_tasks_in_progress = Queue.create () + +let timeout_handler_running = ref false + +let max_number_of_running_provers = ref 1 + +let number_of_running_provers = ref 0 + +open Call_provers + +let dummy_result = + { + pr_answer = Call_provers.Unknown ("I'm dumb", None); + pr_status = Unix.WEXITED 0; + pr_output = ""; + pr_time = 3.14; + pr_steps = 42; + pr_model = Model_parser.default_model; +} + +let build_prover_call s id pr timelimit callback = + let c = ref 0 in + let call () = + incr c; + if !c = 1000 then Call_provers.ProverStarted else + if !c = 10000 then Call_provers.ProverFinished dummy_result + else Call_provers.NoUpdates +(* + match find_prover eS a with + | None -> + callback a a.proof_prover Call_provers.empty_limit None Starting; + (* nothing to do *) + callback a a.proof_prover Call_provers.empty_limit None MissingProver + | Some(ap,npc,a) -> + callback a ap Call_provers.empty_limit None Starting; + 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 ~interactive:itp ~use_steps a in + let inplace = npc.prover_config.Whyconf.in_place in + let command = + Whyconf.get_complete_command npc.prover_config + ~with_steps:(limit.Call_provers.limit_steps <> + Call_provers.empty_limit.Call_provers.limit_steps) in + let cb result = + let result = fuzzy_proof_time result previous_result in + callback a ap limit + (match previous_result with Done res -> Some res | _ -> None) + (StatusChange result) in + try + let old = + match get_edited_as_abs eS.session a with + | None -> None + | Some f -> + if Sys.file_exists f then Some f + else raise (NoFile f) in + schedule_proof_attempt + ~cntexample ~limit + ?old ~inplace ~command + ~driver:npc.prover_driver + ~callback:cb + eT + (goal_task_or_recover eS a.proof_parent) + with NoFile f -> + callback a ap Call_provers.empty_limit None (MissingFile f) + end + + let call = + Driver.prove_task ?old:None ~cntexample:false ~inplace:false ~command + ~limit driver goal + in + *) + in + let pa = (callback,false,call) in + Queue.push pa prover_tasks_in_progress + +let timeout_handler () = + (* examine all the prover tasks in progress *) + let q = Queue.create () in + while not (Queue.is_empty prover_tasks_in_progress) do + let (callback,started,call) as c = Queue.pop prover_tasks_in_progress in + match (*Call_provers.query_call*) call () with + | Call_provers.NoUpdates -> Queue.add c q + | Call_provers.ProverStarted -> + assert (not started); + callback Running; + incr number_of_running_provers; + Queue.add (callback,true,call) q + | Call_provers.ProverFinished res -> + if started then decr number_of_running_provers; + callback (Done res) + done; + Queue.transfer q prover_tasks_in_progress; + (* if the number of prover tasks in less that 3 times the maximum + number of running provers, then we heuristically decide to add + more tasks *) + try + for i = Queue.length prover_tasks_in_progress + to 3 * !max_number_of_running_provers do + let (s,id,pr,timelimit,callback) = Queue.pop scheduled_proof_attempts in + try + build_prover_call s id pr timelimit callback + with e when not (Debug.test_flag Debug.stack_trace) -> + Format.eprintf + "@[Exception raise in Controler_itp.build_prover_call:@ %a@.@]" + Exn_printer.exn_printer e; + callback (InternalFailure e) + done; + true + with Queue.Empty -> true + +let run_timeout_handler () = + if not !timeout_handler_running then + begin + timeout_handler_running := true; + S.timeout ~ms:125 timeout_handler; + end + let schedule_proof_attempt s id pr ~timelimit ~callback = graft_proof_attempt s id pr ~timelimit; - callback Scheduled + Queue.add (s,id,pr,timelimit,callback) scheduled_proof_attempts; + callback Scheduled; + run_timeout_handler () let schedule_transformations s id name args ~callback = let tid = graft_transf s id name args in diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index 61602d30c..c957547b9 100644 --- a/src/session/controller_itp.mli +++ b/src/session/controller_itp.mli @@ -26,8 +26,27 @@ val print_status : Format.formatter -> proof_attempt_status -> unit type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed module type Scheduler = sig - val timeout: ms:int -> (unit -> bool) -> unit - val idle: (unit -> bool) -> unit + + (** Any module of this signature should implement a scheduler, + that allows the register functions to call, and call them + depending on some time constraints: after a given delay, or simply + when there is no more tasks with higher priority. *) + + val timeout: ms:int -> (unit -> bool) -> unit + (** [timeout ~ms f] registers the function [f] as a function to be + called every [ms] milliseconds. The function is called repeatedly + until it returns false. the [ms] delay is not strictly guaranteed: + it is only a minimum delay between the end of the last call and + the beginning of the next call. Several functions can be + registered at the same time. *) + + val idle: prio:int -> (unit -> bool) -> unit + (** [idle prio f] registers the function [f] as a function to be + called whenever there is nothing else to do. Several functions can + be registered at the same time. Several functions can be + registered at the same time. Functions registered with higher + priority will be called first. *) + end diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index 5642222e6..f99ef5e57 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -2,7 +2,18 @@ type session type transID type proofNodeID type proof_attempt -type trans_arg + +type trans_arg = + | TAint of int + | TAstring of string + | TAterm of Term.term + | TAty of Ty.ty + | TAtysymbol of Ty.tysymbol + (* | ... *) + + + + (* New Proof sessions ("Refectoire") *) @@ -17,12 +28,17 @@ type trans_arg type tree = Tree of (proofNodeID * string - * proof_attempt list (* proof attempts in this node *) - * (transID * string * tree list) list) (* transformation in this node *) + * proof_attempt list (* proof attempts on this node *) + * (transID * string * tree list) list) (* transformations on this node *) +(* a tree is a complete proof whenever at least one proof_attempf or + one transformation proves the goal, where a transformation proves a + goal when all subgoals have a complete proof. In other word, the + list of proof_attempt and transformation are "disjunctive" but the + list of tree below a transformation is "conjunctive" *) val get_theories : session -> (string * (string * proofNodeID list) list) list (** [get_theories s] returns a list of pairs [name,l] where [name] is a - file name and [l] is a list of pairs [thnmae,l'] where [thname] is + file name and [l] is a list of pairs [thname,l'] where [thname] is a theory name and [l'] is the list of goal ids *) val get_tree : session -> proofNodeID -> tree diff --git a/src/why3shell/why3shell.ml b/src/why3shell/why3shell.ml index 64239e27f..587ed3279 100644 --- a/src/why3shell/why3shell.ml +++ b/src/why3shell/why3shell.ml @@ -2,8 +2,12 @@ module Unix_scheduler = struct + (* the private list of functions to call on idle, sorted higher + priority first. *) let idle_handler = ref [] + (* [insert_idle_handler p f] inserts [f] as a new function to call + on idle, with priority [p] *) let insert_idle_handler p f = let rec aux l = match l with @@ -13,8 +17,12 @@ module Unix_scheduler = struct in idle_handler := aux !idle_handler + (* the private list of functions to call on idle, sorted on + earliest trigger time first. *) let timeout_handler = ref [] + (* [insert_timeout_handler ms t f] inserts [f] as a new function to call + on timeout, with time step of [ms] and first call time as [t] *) let insert_timeout_handler ms t f = let rec aux l = match l with @@ -24,47 +32,57 @@ module Unix_scheduler = struct in timeout_handler := aux !timeout_handler - + (* public function to register a task to run on idle *) let idle ~(prio:int) f = insert_idle_handler prio f + (* public function to register a task to run on timeout *) let timeout ~ms f = + assert (ms > 0); let ms = float ms /. 1000.0 in let time = Unix.gettimeofday () in insert_timeout_handler ms (time +. ms) f + (* buffer for storing character read on stdin *) let buf = Bytes.create 256 + (* [main_loop interp] starts the scheduler. On idle, standard input is + read. When a complete line is read from stdin, it is passed + as a string to the function [interp] *) let main_loop interp = try while true do (* attempt to run the first timeout handler *) let time = Unix.gettimeofday () in match !timeout_handler with - | (ms,t,f) :: rem when t <= time -> - timeout_handler := rem; - let b = f () in - let time = Unix.gettimeofday () in - if b then insert_timeout_handler ms (ms +. time) f - | _ -> - (* attempt to run the first idle handler *) - match !idle_handler with - | (p,f) :: rem -> - idle_handler := rem; - let b = f () in - if b then insert_idle_handler p f - | [] -> - (* check stdin for a some delay *) - let delay = - match !timeout_handler with - | [] -> 0.1 - | (_,t,_) :: _ -> t -. time - in - let a,_,_ = Unix.select [Unix.stdin] [] [] delay in - match a with - | [_] -> let n = Unix.read Unix.stdin buf 0 256 in - interp (Bytes.sub_string buf 0 (n-1)) - | [] -> () - | _ -> assert false + | (ms,t,f) :: rem when t <= time -> + timeout_handler := rem; + let b = f () in + let time = Unix.gettimeofday () in + if b then insert_timeout_handler ms (ms +. time) f + | _ -> + (* time is not yet passed *) + (* attempt to run the first idle handler *) + match !idle_handler with + | (p,f) :: rem -> + idle_handler := rem; + let b = f () in + if b then insert_idle_handler p f + | [] -> + (* no idle handler *) + (* check stdin for a some delay *) + let delay = + match !timeout_handler with + | [] -> 0.125 + (* 1/8 second by default *) + | (_,t,_) :: _ -> t -. time + (* or the time left until the next timeout otherwise *) + in + let a,_,_ = Unix.select [Unix.stdin] [] [] delay in + match a with + | [_] -> let n = Unix.read Unix.stdin buf 0 256 in + interp (Bytes.sub_string buf 0 (n-1)) + | [] -> () (* nothing read *) + | _ -> assert false done with Exit -> () @@ -72,17 +90,17 @@ end -(* module C = Why3.Controller_itp.Make(Unix_scheduler) - *) + +open Why3.Session_itp let interp s = match s with | "a" -> - let c = ref 10 in Unix_scheduler.timeout ~ms:1000 - (fun () -> decr c; + (let c = ref 10 in + fun () -> decr c; if !c > 0 then (Format.printf "%d@." !c; true) else @@ -91,7 +109,14 @@ let interp s = Unix_scheduler.idle ~prio:0 (fun () -> Format.printf "idle@."; false) - | _ -> Format.printf "unknowm command `%s`@." s +(* + | "p" -> + let s = empty_session () in + C.schedule_proof_attempt + s (get_node s 0) +*) + + | _ -> Format.printf "unknown command `%s`@." s -- GitLab