session_scheduler.ml 31.6 KB
Newer Older
François Bobot's avatar
François Bobot committed
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
François Bobot's avatar
François Bobot committed
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
François Bobot's avatar
François Bobot committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Session
open Debug

25
let debug = register_info_flag "scheduler"
26
27
  ~desc:"About@ the@ session@ scheduler@ which@ schedules@ the@ application@ \
          of@ transformtions@ or@ the@ call@ of@ provers."
François Bobot's avatar
François Bobot committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

(***************************)
(*     main functor        *)
(***************************)

module type OBSERVER = sig
  type key
  val create: ?parent:key -> unit -> key
  val remove: key -> unit
  val reset: unit -> unit

  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: (unit -> bool) -> unit

  val notify_timer_state : int -> int -> int -> unit

  val init : key -> key any -> unit

  val notify : key any -> unit

48
(*
49
50
51
52
  val unknown_prover :
    key env_session -> Whyconf.prover -> Whyconf.prover option

  val replace_prover : key proof_attempt -> key proof_attempt -> bool
53
54
55
56
*)

  val uninstalled_prover :
    key env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
57

François Bobot's avatar
François Bobot committed
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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 *)

82
(* dead code
François Bobot's avatar
François Bobot committed
83
84
85
86
87
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
88
*)
François Bobot's avatar
François Bobot committed
89

90
91
92
let running = function
  | Scheduled | Running -> true
  | Unedited | JustEdited | Interrupted
93
  | Done _ | InternalFailure _ -> false
François Bobot's avatar
François Bobot committed
94
95
96
97
98
99

(*************************)
(*         Scheduler     *)
(*************************)

type action =
100
  | Action_proof_attempt of int * int * string option * bool * string *
François Bobot's avatar
François Bobot committed
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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
      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)

type t =
    { (** Actions that wait some idle time *)
      actions_queue : action Queue.t;
      (** Quota of action slot *)
      mutable maximum_running_proofs : int;
      (** Running actions which take one action slot *)
      mutable running_proofs : timeout_action list;
      (** Running check which doesn't take a running slot.
          Check the end of some computation *)
      mutable running_check : (unit -> bool) list;
      (** proof attempt that wait some available action slot *)
      proof_attempts_queue :
        ((proof_attempt_status -> unit) *
            (unit -> Call_provers.prover_call))
        Queue.t;
      (** timeout handler state *)
      mutable timeout_handler_activated : bool;
      mutable timeout_handler_running : bool;
      (** idle handler state *)
      mutable idle_handler_activated : bool;
    }

let set_maximum_running_proofs max sched =
 (** TODO dequeue actions if maximum_running_proofs increase *)
  sched.maximum_running_proofs <- max

let init max =
  dprintf debug "[Sched] init scheduler max=%i@." max;
  { actions_queue = Queue.create ();
    maximum_running_proofs = max;
    running_proofs = [];
    running_check = [];
    proof_attempts_queue = Queue.create ();
    timeout_handler_activated = false;
    timeout_handler_running = false;
    idle_handler_activated = false
  }

(* timeout handler *)

let timeout_handler t =
  dprintf debug "[Sched] Timeout handler called@.";
  assert (not t.timeout_handler_running);
  t.timeout_handler_running <- true;
  (** Check if some action ended *)
  let l = List.fold_left
    (fun acc c ->
       match c with
         | Check_prover(callback,call)  ->
             (match Call_provers.query_call call with
               | None -> c::acc
               | Some post ->
                   let res = post () in callback (Done res);
                   acc)
         | Any_timeout callback ->
             let b = callback () in
             if b then c::acc else acc)
    [] t.running_proofs
  in
  (** Check if some new actions must be started *)
  let l =
    if List.length l < t.maximum_running_proofs then
      begin try
        let (callback,pre_call) = Queue.pop t.proof_attempts_queue in
173
        callback Running;
François Bobot's avatar
François Bobot committed
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
        dprintf debug "[Sched] proof attempts started@.";
        let call = pre_call () in
        (Check_prover(callback,call))::l
      with Queue.Empty -> l
      end
    else l
  in
  t.running_proofs <- l;
  (** Call the running check *)
  t.running_check <- List.fold_left
    (fun acc check -> if check () then check::acc else acc)
    [] t.running_check;
  let continue =
    match l with
      | [] ->
          dprintf debug "[Sched] Timeout handler stopped@.";
          false
      | _ -> true
  in
  O.notify_timer_state
    (Queue.length t.actions_queue)
    (Queue.length t.proof_attempts_queue) (List.length l);
  t.timeout_handler_activated <- continue;
  t.timeout_handler_running <- false;
  continue

let run_timeout_handler t =
  if t.timeout_handler_activated then () else
    begin
      t.timeout_handler_activated <- true;
      dprintf debug "[Sched] Timeout handler started@.";
      O.timeout ~ms:100 (fun () -> timeout_handler t)
    end

let schedule_any_timeout t callback =
  dprintf debug "[Sched] schedule a new timeout@.";
  t.running_proofs <- (Any_timeout callback) :: t.running_proofs;
  run_timeout_handler t

213
(* dead code 
François Bobot's avatar
François Bobot committed
214
215
216
217
let add_a_check t callback =
  dprintf debug "[Sched] add a new check@.";
  t.running_check <- callback :: t.running_check;
  run_timeout_handler t
218
*)
François Bobot's avatar
François Bobot committed
219
220
221
222
223
224
225
226

(* idle handler *)


let idle_handler t =
  try
    begin
      match Queue.pop t.actions_queue with
227
        | Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
François Bobot's avatar
François Bobot committed
228
229
230
231
232
                               callback,goal) ->
            begin
              try
                let pre_call =
                  Driver.prove_task
233
                    ?old ~inplace ~command ~timelimit ~memlimit driver goal
François Bobot's avatar
François Bobot committed
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
                in
                Queue.push (callback,pre_call) t.proof_attempts_queue;
                run_timeout_handler t
              with e ->
                Format.eprintf "@[Exception raise in Session.idle_handler:@ \
%a@.@]"
                  Exn_printer.exn_printer e;
                callback (InternalFailure e)
            end
        | Action_delayed callback -> callback ()
    end;
    true
  with Queue.Empty ->
    t.idle_handler_activated <- false;
    dprintf debug "[Sched] idle_handler stopped@.";
    false
    | e ->
      Format.eprintf "@[Exception raise in Session.idle_handler:@ %a@.@]"
        Exn_printer.exn_printer e;
      eprintf "Session.idle_handler stopped@.";
      false


let run_idle_handler t =
  if t.idle_handler_activated then () else
    begin
      t.idle_handler_activated <- true;
      dprintf debug "[Sched] idle_handler started@.";
      O.idle (fun () -> idle_handler t)
    end

(* main scheduling functions *)

let cancel_scheduled_proofs t =
  let new_queue = Queue.create () in
  try
    while true do
      match Queue.pop t.actions_queue with
272
        | Action_proof_attempt(_timelimit,_memlimit,_old,_inplace,_command,
François Bobot's avatar
François Bobot committed
273
                               _driver,callback,_goal) ->
274
            callback Interrupted
François Bobot's avatar
François Bobot committed
275
276
277
278
279
280
281
282
        | Action_delayed _ as a->
            Queue.push a new_queue
    done
  with Queue.Empty ->
    Queue.transfer new_queue t.actions_queue;
    try
      while true do
        let (callback,_) = Queue.pop t.proof_attempts_queue in
283
        callback Interrupted
François Bobot's avatar
François Bobot committed
284
285
      done
    with
286
      | Queue.Empty ->
François Bobot's avatar
François Bobot committed
287
288
289
          O.notify_timer_state 0 0 (List.length t.running_proofs)


290
let schedule_proof_attempt ~timelimit ~memlimit ?old ~inplace
François Bobot's avatar
François Bobot committed
291
    ~command ~driver ~callback t goal =
292
293
294
  dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@."
    (fun fmt g -> Format.pp_print_string fmt
      (Task.task_goal g).Decl.pr_name.Ident.id_string) goal;
295
  callback Scheduled;
François Bobot's avatar
François Bobot committed
296
  Queue.push
297
    (Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver,
François Bobot's avatar
François Bobot committed
298
299
300
301
302
303
304
305
306
307
                        callback,goal))
    t.actions_queue;
  run_idle_handler t

let schedule_edition t command filename callback =
  dprintf debug "[Sched] Scheduling an edition@.";
  let precall =
    Call_provers.call_on_file ~command ~regexps:[] ~timeregexps:[]
      ~exitcodes:[(0,Call_provers.Unknown "")] filename
  in
308
  callback Running;
François Bobot's avatar
François Bobot committed
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
  t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
  run_timeout_handler t

let schedule_delayed_action t callback =
  dprintf debug "[Sched] Scheduling a delayed action@.";
  Queue.push (Action_delayed callback) t.actions_queue;
  run_idle_handler t

(**************************)
(*  session function      *)
(**************************)

let update_session ~allow_obsolete old_session env whyconf  =
  O.reset ();
  let (env_session,_) as res =
    update_session ~keygen:O.create ~allow_obsolete old_session env whyconf in
François Bobot's avatar
François Bobot committed
325
  dprintf debug "Init_session@\n";
François Bobot's avatar
François Bobot committed
326
327
328
  init_session env_session.session;
  res

329
330
let add_file env_session ?format f =
  let mfile = add_file ~keygen:O.create env_session ?format f in
François Bobot's avatar
François Bobot committed
331
332
333
334
335
336
337
338
  let any_file = (File mfile) in
  init_any any_file;
  O.notify any_file;
  mfile

(*****************************************************)
(* method: run a given prover on each unproved goals *)
(*****************************************************)
339
(*
340
341
342
343
344
345
346
347
348
349
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)
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
*)

let find_prover eS a =
  match load_prover eS a.proof_prover with
    | Some p -> Some (a.proof_prover, p,a)
    | None ->
        match O.uninstalled_prover eS a.proof_prover with
          | Whyconf.CPU_keep -> None
          | Whyconf.CPU_upgrade new_p ->
            (* does a proof using new_p already exists ? *)
            let g = a.proof_parent in
            begin
              try
                let _ = PHprover.find g.goal_external_proofs new_p in
                (* yes, then we do nothing *)
                None
              with Not_found ->
                (* we modify the prover in-place *)
                Session.change_prover a new_p;
                match load_prover eS new_p with
                  | Some p -> Some (new_p,p,a)
                  | None -> 
                    (* should never happen because at loading, config
                       ignores uninstalled prover targets.
                       Nevertheless, we can safely return None.
                    *)
                    None
            end
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
          | Whyconf.CPU_duplicate new_p -> 
            (* does a proof using new_p already exists ? *)
            let g = a.proof_parent in
            begin
              try
                let _ = PHprover.find g.goal_external_proofs new_p in
                (* yes, then we do nothing *)
                None
              with Not_found ->
                (* we duplicate the proof_attempt *)
                let new_a = copy_external_proof
                  ~notify ~keygen:O.create ~prover:new_p ~env_session:eS a 
                in
                O.init new_a.proof_key (Proof_attempt new_a);
                match load_prover eS new_p with
                  | Some p -> Some (new_p,p,new_a)
                  | None -> 
                    (* should never happen because at loading, config
                       ignores uninstalled prover targets.
                       Nevertheless, we can safely return None.
                    *)
                    None
            end
401

François Bobot's avatar
François Bobot committed
402

403
404
let adapt_timelimit a =
  match a.proof_state with
405
406
    | Done { Call_provers.pr_answer = 
        (Call_provers.Valid | Call_provers.Unknown _ | Call_provers.Invalid);
407
             Call_provers.pr_time = t } ->
408
409
      let t = truncate (1.0 +. 2.0 *. t) in
      max a.proof_timelimit (min t (2 * a.proof_timelimit))
410
411
    | _ -> a.proof_timelimit

412
413
414
415
416
417
418
419
type run_external_status =
  | Starting
  | MissingProver
  | MissingFile of string
  | StatusChange of proof_attempt_status

exception NoFile of string

420
421
422
423
424
425
426
427
428
429
(* do not modify the proof duration if it changed by less than
   10% or 0.1s, so as to avoid diff noise in session files *)
let fuzzy_proof_time nres ores =
  match ores, nres with
  | Done { Call_provers.pr_time = told },
    Done ({ Call_provers.pr_time = tnew } as res')
    when tnew >= told *. 0.9 -. 0.1 && tnew <= told *. 1.1 +. 0.1 ->
    Done { res' with Call_provers.pr_time = told }
  | _, _ -> nres

430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
let run_external_proof_v2 eS eT a callback =
  callback a a.proof_prover 0 None Starting;
  match find_prover eS a with
  | None ->
    (* nothing to do *)
    callback a a.proof_prover 0 None MissingProver
  | Some(ap,npc,a) ->
    if a.proof_edited_as = None &&
       npc.prover_config.Whyconf.interactive
    then begin
      set_proof_state ~notify ~obsolete:false ~archived:false
        Unedited a;
      callback a ap 0 None (MissingFile "unedited")
    end else begin
      let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
      let timelimit = adapt_timelimit a in
      let memlimit = a.proof_memlimit in
      let inplace = npc.prover_config.Whyconf.in_place in
      let command = Whyconf.get_complete_command npc.prover_config in
      let cb result =
450
        let result = fuzzy_proof_time result previous_result in
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
        begin match result with
        | Interrupted ->
          set_proof_state ~notify ~obsolete:previous_obs
            ~archived:false previous_result a
        | _ ->
          set_proof_state ~notify ~obsolete:false
            ~archived:false result a
        end;
        callback a ap timelimit
          (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
          ~timelimit ~memlimit
          ?old ~inplace ~command
          ~driver:npc.prover_driver
          ~callback:cb
          eT
          (goal_task a.proof_parent)
      with NoFile f ->
        set_proof_state ~notify ~obsolete:false ~archived:false
          Unedited a;
        callback a ap 0 None (MissingFile f)
    end

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
  run_external_proof_v2 eS eT a callback
486

487
let run_external_proof eS eT ?callback a =
488
489
490
491
492
493
494
495
496
497
  let callback =
    match callback with
    | None -> fun _ _ _ _ _ -> ()
    | Some c -> fun a _ _ _ s ->
      match s with
      | Starting -> ()
      | MissingProver -> c a Interrupted
      | MissingFile _ -> c a a.proof_state
      | StatusChange s -> c a s in
  run_external_proof_v2 eS eT a callback
François Bobot's avatar
François Bobot committed
498

499
let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g =
François Bobot's avatar
François Bobot committed
500
  let a =
501
502
503
    try
      let a = PHprover.find g.goal_external_proofs p in
      set_timelimit timelimit a;
504
      set_memlimit memlimit a;
505
      a
François Bobot's avatar
François Bobot committed
506
    with Not_found ->
507
      let ep = add_external_proof ~keygen:O.create ~obsolete:false
508
        ~archived:false ~timelimit ~memlimit 
509
        ~edit:None g p Interrupted in
François Bobot's avatar
François Bobot committed
510
511
512
      O.init ep.proof_key (Proof_attempt ep);
      ep
  in
513
  run_external_proof eS eT ?callback a
François Bobot's avatar
François Bobot committed
514

515
let prover_on_goal_or_children eS eT
516
    ~context_unproved_goals_only ~timelimit ~memlimit p g =
517
  goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
518
    (prover_on_goal eS eT ~timelimit ~memlimit p) g
François Bobot's avatar
François Bobot committed
519

520
let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
François Bobot's avatar
François Bobot committed
521
522
523
  match a with
    | Goal g ->
        prover_on_goal_or_children eS eT
524
          ~context_unproved_goals_only ~timelimit ~memlimit pr g
François Bobot's avatar
François Bobot committed
525
526
527
    | Theory th ->
        List.iter
          (prover_on_goal_or_children eS eT
528
             ~context_unproved_goals_only ~timelimit ~memlimit pr)
François Bobot's avatar
François Bobot committed
529
530
531
532
533
534
          th.theory_goals
    | File file ->
        List.iter
          (fun th ->
             List.iter
               (prover_on_goal_or_children eS eT
535
                  ~context_unproved_goals_only ~timelimit ~memlimit pr)
François Bobot's avatar
François Bobot committed
536
537
538
539
               th.theory_goals)
          file.file_theories
    | Proof_attempt a ->
        prover_on_goal_or_children eS eT
540
          ~context_unproved_goals_only ~timelimit ~memlimit pr a.proof_parent
François Bobot's avatar
François Bobot committed
541
542
543
    | Transf tr ->
        List.iter
          (prover_on_goal_or_children eS eT
544
             ~context_unproved_goals_only ~timelimit ~memlimit pr)
François Bobot's avatar
François Bobot committed
545
          tr.transf_goals
François Bobot's avatar
François Bobot committed
546
547
548
    | Metas m ->
      prover_on_goal_or_children eS eT
        ~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
François Bobot's avatar
François Bobot committed
549
550
551
552
553

(**********************************)
(* method: replay obsolete proofs *)
(**********************************)

554
let proof_successful_or_just_edited a =
François Bobot's avatar
François Bobot committed
555
  match a.proof_state with
556
    | Done { Call_provers.pr_answer = Call_provers.Valid }
557
    | JustEdited -> true
François Bobot's avatar
François Bobot committed
558
559
560
561
    | _ -> false

let rec replay_on_goal_or_children eS eT
    ~obsolete_only ~context_unproved_goals_only g =
François Bobot's avatar
François Bobot committed
562
563
  iter_goal
    (fun a ->
François Bobot's avatar
François Bobot committed
564
       if not obsolete_only || a.proof_obsolete then
565
         if not context_unproved_goals_only || proof_successful_or_just_edited a
566
         then run_external_proof eS eT a)
François Bobot's avatar
François Bobot committed
567
568
569
570
571
572
573
574
575
    (iter_transf
       (replay_on_goal_or_children eS eT
          ~obsolete_only ~context_unproved_goals_only)
    )
    (iter_metas
       (replay_on_goal_or_children eS eT
          ~obsolete_only ~context_unproved_goals_only)
    )
    g
François Bobot's avatar
François Bobot committed
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602

let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
  match a with
    | Goal g ->
        replay_on_goal_or_children eS eT
          ~obsolete_only ~context_unproved_goals_only g
    | Theory th ->
        List.iter
          (replay_on_goal_or_children eS eT
             ~obsolete_only ~context_unproved_goals_only)
          th.theory_goals
    | File file ->
        List.iter
          (fun th ->
             List.iter
               (replay_on_goal_or_children eS eT
                  ~obsolete_only ~context_unproved_goals_only)
               th.theory_goals)
          file.file_theories
    | Proof_attempt a ->
        replay_on_goal_or_children eS eT
          ~obsolete_only ~context_unproved_goals_only a.proof_parent
    | Transf tr ->
        List.iter
          (replay_on_goal_or_children eS eT
             ~obsolete_only ~context_unproved_goals_only)
          tr.transf_goals
François Bobot's avatar
François Bobot committed
603
604
605
606
    | Metas m ->
      replay_on_goal_or_children eS eT
        ~obsolete_only ~context_unproved_goals_only m.metas_goal

François Bobot's avatar
François Bobot committed
607
608
609
610
611

(***********************************)
(* method: mark proofs as obsolete *)
(***********************************)

612
613
614
let cancel_proof a =
  if not a.proof_archived then
    set_obsolete ~notify a
François Bobot's avatar
François Bobot committed
615
616
617

let cancel = iter_proof_attempt cancel_proof

618
619
(** Set or unset archive *)

620
let set_archive a b = set_archived a b; notify (Proof_attempt a)
621

François Bobot's avatar
François Bobot committed
622
623
624
625
626
627
628
629
(*********************************)
(* method: check existing proofs *)
(*********************************)

type report =
  | Result of Call_provers.prover_result * Call_provers.prover_result
  | CallFailed of exn
  | Prover_not_installed
630
  | Edited_file_absent of string
François Bobot's avatar
François Bobot committed
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
  | No_former_result of Call_provers.prover_result

module Todo = struct
  type ('a,'b) todo =
      {mutable todo : int;
       report : 'a;
       push_report : 'a -> 'b -> unit}

  let create init push =
    {todo = 0;  report = init; push_report = push}

  let _done todo v =
    todo.todo <- todo.todo - 1;
    todo.push_report todo.report v

646
(* dead code
François Bobot's avatar
François Bobot committed
647
648
  let stop todo =
    todo.todo <- todo.todo - 1
649
*)
François Bobot's avatar
François Bobot committed
650
651
652
653
654
655
656

  let todo todo =
    todo.todo <- todo.todo + 1

  let _end todo =
    if todo.todo<>0 then None else Some todo.report

657
(* dead code
François Bobot's avatar
François Bobot committed
658
659
  let print todo =
    dprintf debug "[Sched] todo : %i@." todo.todo
660
*)
François Bobot's avatar
François Bobot committed
661
662
end

663
664
let push_report report (g,p,t,r) =
  report := (g.goal_name,p,t,r)::!report
François Bobot's avatar
François Bobot committed
665
666

let check_external_proof eS eT todo a =
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
  let callback a ap tl old s =
    let g = a.proof_parent in
    match s with
    | Starting ->
      Todo.todo todo
    | MissingFile f ->
      Todo._done todo (g, ap, tl, Edited_file_absent f)
    | MissingProver ->
      Todo._done todo (g, ap, tl, Prover_not_installed)
    | StatusChange (Scheduled | Running) -> ()
    | StatusChange (Interrupted | Unedited | JustEdited) -> assert false
    | StatusChange (InternalFailure e) ->
      Todo._done todo (g, ap, tl, CallFailed e)
    | StatusChange (Done res) ->
      let r =
        match old with
        | None -> No_former_result res
        | Some old -> Result (res, old) in
      Todo._done todo (g, ap, tl, r) in
  run_external_proof_v2 eS eT a callback
François Bobot's avatar
François Bobot committed
687

688
(* dead code
François Bobot's avatar
François Bobot committed
689
690
let check_goal_and_children eS eT todo g =
  goal_iter_proof_attempt (check_external_proof eS eT todo) g
691
*)
François Bobot's avatar
François Bobot committed
692
693
694
695
696
697
698
699

let check_all eS eT ~callback =
  dprintf debug "[Sched] check all@.%a@." print_session eS.session;
  let todo = Todo.create (ref []) push_report  in
  session_iter_proof_attempt (check_external_proof eS eT todo)
    eS.session;
  let timeout () =
    match Todo._end todo with
700
701
      | None -> true
      | Some reports -> callback !reports;false
François Bobot's avatar
François Bobot committed
702
703
704
  in
  schedule_any_timeout eT timeout

705
706
707
708
709

(***********************************)
(* play all                        *)
(***********************************)

710
let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
711
  let callback _key status =
712
    if not (running status) then Todo._done todo () in
713
  List.iter
714
    (fun p ->
715
      Todo.todo todo;
716
717
718
      (* eprintf "todo increased to %d@." todo.Todo.todo; *)
      (* eprintf "prover %a on goal %s@." *)
      (*   Whyconf.print_prover p g.goal_name.Ident.id_string; *)
719
      prover_on_goal eS eT ~callback ~timelimit ~memlimit p g)
720
    l;
François Bobot's avatar
François Bobot committed
721
722
723
724
725
726
727
728
729
  iter_goal
    (fun _ -> ())
    (iter_transf
       (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
    )
    (iter_metas
       (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
    )
    g
730
731


732
let play_all eS eT ~callback ~timelimit ~memlimit l =
733
  let todo = Todo.create (ref ()) (fun _ _ -> ())  in
734
  PHstr.iter
735
    (fun _ file ->
736
737
738
      List.iter
        (fun th ->
          List.iter
739
            (play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
740
741
            th.theory_goals)
        file.file_theories)
742
743
    eS.session.session_files;
  let timeout () =
744
    (* eprintf "Timeout handler@."; *)
745
746
747
748
749
750
    match Todo._end todo with
      | None ->  true
      | Some _ -> callback (); false
  in
  schedule_any_timeout eT timeout

751

752

François Bobot's avatar
François Bobot committed
753
754
(** Transformation *)

755
let transformation_on_goal_aux eS tr keep_dumb_transformation g =
François Bobot's avatar
François Bobot committed
756
  let subgoals = Trans.apply_transform tr eS.env (goal_task g) in
757
  let b = keep_dumb_transformation ||
François Bobot's avatar
François Bobot committed
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
    match subgoals with
      | [task] ->
              (* let s1 = task_checksum (get_task g) in *)
              (* let s2 = task_checksum task in *)
              (* (\* *)
              (*   eprintf "Transformation returned only one task.
                   sum before = %s, sum after = %s@." (task_checksum g.task)
                   (task_checksum task); *)
              (*   eprintf "addresses: %x %x@." (Obj.magic g.task)
                   (Obj.magic task); *)
              (* *\) *)
              (* s1 <> s2 *)
        not (Task.task_equal task (goal_task g))
      | _ -> true
  in
  if b then
    let goal_name = g.goal_name.Ident.id_string in
    let i = ref (-1) in
    let ntr = add_transformation
      ~keygen:O.create
      ~goal:(fun subtask ->
        incr i;
        let gid,expl,task = goal_expl_task subtask in
        let gid =
          Ident.id_derive (goal_name ^ "." ^ (string_of_int (!i))) gid in
        let gid = Ident.id_register gid in
        gid,expl,task)
785
      eS tr g subgoals in
786
787
788
    init_any (Transf ntr);
    Some ntr
  else None
François Bobot's avatar
François Bobot committed
789

790
791
792
793
794
795
let transform_goal eS sched ?(keep_dumb_transformation=false)
    ?callback tr g =
  schedule_delayed_action sched
    (fun () -> let ntr = transformation_on_goal_aux eS tr
                 keep_dumb_transformation g in
               Util.apply_option () callback ntr)
François Bobot's avatar
François Bobot committed
796
797


798
799
800
801
802
let transform_goal_or_children ~context_unproved_goals_only eS sched ?callback
    tr g =
  goal_iter_leaf_goal ~unproved_only:context_unproved_goals_only
    (transform_goal eS sched ~keep_dumb_transformation:false
       ?callback tr) g
François Bobot's avatar
François Bobot committed
803

804
let rec transform eS sched ~context_unproved_goals_only ?callback tr a =
François Bobot's avatar
François Bobot committed
805
806
  match a with
    | Goal g | Proof_attempt {proof_parent = g} ->
807
808
809
      transform_goal_or_children ~context_unproved_goals_only eS sched
        ?callback tr g
    | _ -> iter (transform ~context_unproved_goals_only eS sched ?callback tr) a
François Bobot's avatar
François Bobot committed
810
811
812
813
814

(*****************************)
(* method: edit current goal *)
(*****************************)

815
let edit_proof eS sched ~default_editor a =
François Bobot's avatar
François Bobot committed
816
  (* check that the state is not Scheduled or Running *)
817
  if a.proof_archived || running a.proof_state then ()
François Bobot's avatar
François Bobot committed
818
819
820
821
(*
    info_window `ERROR "Edition already in progress"
*)
  else
822
823
824
825
826
827
828
829
      match find_prover eS a with
        | None ->
          (* nothing to do 
             TODO: report an non replayable proof if some option is set
          *)
          ()
        | Some(_,npc,a) ->
(*
830
831
    let ap = a.proof_prover in
    match find_loadable_prover eS a.proof_prover with
François Bobot's avatar
François Bobot committed
832
      | None -> ()
833
834
        (** Perhaps a new prover *)
      | Some (nap,npc) ->
François Bobot's avatar
François Bobot committed
835
          let g = a.proof_parent in
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
          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] *)
853
854
*)

François Bobot's avatar
François Bobot committed
855
856
          let callback res =
            match res with
857
              | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
858
                set_proof_state ~notify ~obsolete:true ~archived:false
859
                  JustEdited a
François Bobot's avatar
François Bobot committed
860
              | _ ->
861
862
                  set_proof_state ~notify ~obsolete:false ~archived:false
                    res a
François Bobot's avatar
François Bobot committed
863
864
          in
          let editor =
865
            match npc.prover_config.Whyconf.editor with
866
867
868
869
870
871
872
            | "" -> default_editor
            | s ->
              try
                let ed = Whyconf.editor_by_id eS.whyconf s in
                String.concat " "(ed.Whyconf.editor_command ::
                  ed.Whyconf.editor_options)
              with Not_found -> default_editor
François Bobot's avatar
François Bobot committed
873
          in
874
          let file = update_edit_external_proof eS a in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
875
          dprintf debug "[Editing] goal %a with command '%s' on file %s@."
876
877
878
879
880
            (fun fmt a -> pp_print_string fmt
              (Task.task_goal (goal_task a.proof_parent))
              . Decl.pr_name.Ident.id_string)
            a editor file;
          schedule_edition sched editor file callback
François Bobot's avatar
François Bobot committed
881
882
883
884
885
886
887
888
889
890
891
892
893
894

(*************)
(* removing  *)
(*************)

let remove_proof_attempt (a:O.key proof_attempt) =
  O.remove a.proof_key;
  let notify = (notify : O.key notify) in
  remove_external_proof ~notify a

let remove_transformation t =
  O.remove t.transf_key;
  remove_transformation ~notify t

François Bobot's avatar
François Bobot committed
895
896
897
898
let remove_metas t =
  O.remove t.metas_key;
  remove_metas ~notify t

François Bobot's avatar
François Bobot committed
899
900
901
902
let rec clean = function
  | Goal g when g.goal_verified ->
    iter_goal
      (fun a ->
903
        if a.proof_obsolete || not (proof_successful_or_just_edited a) then
François Bobot's avatar
François Bobot committed
904
905
906
          remove_proof_attempt a)
      (fun t ->
        if not t.transf_verified then remove_transformation t
François Bobot's avatar
François Bobot committed
907
908
909
910
911
        else transf_iter clean t)
      (fun m ->
        if not m.metas_verified then remove_metas m
        else metas_iter clean m)
      g
François Bobot's avatar
François Bobot committed
912
  | Goal g ->
François Bobot's avatar
François Bobot committed
913
914
915
916
    (** don't iter on proof_attempt if the goal is not proved *)
    iter_goal
      (fun _ -> ())
      (fun t ->
MARCHE Claude's avatar
MARCHE Claude committed
917
918
919
920
921
        (* NO !!! 
           if not t.transf_verified then remove_transformation t
        else 
        *)
        transf_iter clean t)
François Bobot's avatar
François Bobot committed
922
923
924
925
      (fun m ->
        if not m.metas_verified then remove_metas m
        else metas_iter clean m)
      g
François Bobot's avatar
François Bobot committed
926
927
928
929
930
931
932
933
934
  | Proof_attempt a -> clean (Goal a.proof_parent)
  | any -> iter clean any

(**** convert ***)

let convert_unknown_prover =
  Session_tools.convert_unknown_prover ~keygen:O.create

end
935
936
937
938
939
940
941
942
943
944
945


module Base_scheduler (X : sig end)  =
  (struct

    let usleep t = ignore (Unix.select [] [] [] t)


    let idle_handler = ref None
    let timeout_handler = ref None

946
947
    let verbose = ref true

948
949
950
951
952
953
954
955
956
957
958
     let idle f =
       match !idle_handler with
         | None -> idle_handler := Some f;
         | Some _ -> failwith "Replay.idle: already one handler installed"

     let timeout ~ms f =
       match !timeout_handler with
         | None -> timeout_handler := Some(float ms /. 1000.0 ,f);
         | Some _ -> failwith "Replay.timeout: already one handler installed"

     let notify_timer_state w s r =
959
960
       if !verbose then
         Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008

     let main_loop () =
       let last = ref (Unix.gettimeofday ()) in
       try while true do
           let time = Unix.gettimeofday () -. !last in
           (* attempt to run timeout handler *)
           let timeout =
             match !timeout_handler with
               | None -> false
               | Some(ms,f) ->
                 if time > ms then
                   let b = f () in
                   if b then true else
                     begin
                       timeout_handler := None;
                       true
                     end
                 else false
           in
           if timeout then
             last := Unix.gettimeofday ()
           else
      (* attempt to run the idle handler *)
             match !idle_handler with
               | None ->
                 begin
                   let ms =
                     match !timeout_handler with
                       | None -> raise Exit
                       | Some(ms,_) -> ms
                   in
                   usleep (ms -. time)
                 end
               | Some f ->
                 let b = f () in
                 if b then () else
                   begin
                     idle_handler := None;
                   end
         done
       with Exit -> ()

end)





François Bobot's avatar
François Bobot committed
1009
1010
1011
1012
1013
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
End:
*)