controller_itp.ml 6.36 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3 4 5 6 7 8 9 10 11 12
open Session_itp

(** State of a proof *)
type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26
open Format

let print_status fmt st =
  match st with
  | Unedited -> fprintf fmt "Unedited"
  | JustEdited -> fprintf fmt "JustEdited"
  | Interrupted -> fprintf fmt "Interrupted"
  | Scheduled -> fprintf fmt "Scheduled"
  | Running -> fprintf fmt "Running"
  | Done r -> fprintf fmt "Done(%a)" Call_provers.print_prover_result r
  | InternalFailure e -> fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e

type transformation_status =
  | TSscheduled of transID | TSdone of transID | TSfailed
Clément Fumex's avatar
Clément Fumex committed
27

28 29
module type Scheduler = sig
  val timeout: ms:int -> (unit -> bool) -> unit
MARCHE Claude's avatar
MARCHE Claude committed
30
  val idle: prio:int -> (unit -> bool) -> unit
31 32 33 34 35
end


module Make(S : Scheduler) = struct

MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
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;
}

58
let build_prover_call _s _id _pr _timelimit callback =
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  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
137
    for _i = Queue.length prover_tasks_in_progress
MARCHE Claude's avatar
MARCHE Claude committed
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
        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

Clément Fumex's avatar
Clément Fumex committed
158 159
let schedule_proof_attempt s id pr ~timelimit ~callback =
  graft_proof_attempt s id pr ~timelimit;
MARCHE Claude's avatar
MARCHE Claude committed
160 161 162
  Queue.add (s,id,pr,timelimit,callback) scheduled_proof_attempts;
  callback Scheduled;
  run_timeout_handler ()
Clément Fumex's avatar
Clément Fumex committed
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189

let schedule_transformations s id name args ~callback =
  let tid = graft_transf s id name args in
  callback (TSscheduled tid)

let read_file env ?format fn =
  let theories = Env.read_file Env.base_language env ?format fn in
  let ltheories =
    Stdlib.Mstr.fold
      (fun name th acc ->
        (* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
        let th_name =
          Ident.id_register (Ident.id_derive name th.Theory.th_name) in
         match th.Theory.th_name.Ident.id_loc with
           | Some l -> (l,th_name,th)::acc
           | None   -> (Loc.dummy_position,th_name,th)::acc)
      theories []
  in
  let th =  List.sort
      (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
      ltheories
  in
  List.map (fun (_,_,a) -> a) th

let add_file_to_session env s ?format fname =
  let theories = read_file env ?format fname in
  add_file_section s fname theories None
MARCHE Claude's avatar
MARCHE Claude committed
190 191 192

let reload_session_files (_s : session)  =
  failwith "Controller_itp.reload_session_files not yet implemented"
193 194

end