controller_itp.ml 48.4 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
open Format
13
open Wstdlib
Clément Fumex's avatar
Clément Fumex committed
14 15
open Session_itp

Sylvain Dailler's avatar
Sylvain Dailler committed
16 17 18 19
let debug_sched = Debug.register_info_flag "scheduler"
  ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
         and@ transformation@ applications."

Sylvain Dailler's avatar
Sylvain Dailler committed
20
let debug_call_prover = Debug.lookup_flag "call_prover"
21 22
let default_delay_ms = 100 (* 0.1 seconds *)

Clément Fumex's avatar
Clément Fumex committed
23 24
(** State of a proof *)
type proof_attempt_status =
25
  | Undone   (** prover was never called *)
26 27 28
  | Scheduled (** external proof attempt is scheduled *)
  | Running (** external proof attempt is in progress *)
  | Done of Call_provers.prover_result (** external proof done *)
29 30
  | Interrupted (** external proof has never completed *)
  | Detached (** parent goal has no task, is detached *)
31 32
  | InternalFailure of exn (** external proof aborted by internal error *)
  | Uninstalled of Whyconf.prover (** prover is uninstalled *)
33
  | UpgradeProver of Whyconf.prover (** prover is upgraded *)
34
  | Removed of Whyconf.prover (** prover has been removed or upgraded *)
Clément Fumex's avatar
Clément Fumex committed
35

MARCHE Claude's avatar
MARCHE Claude committed
36 37
let print_status fmt st =
  match st with
38
  | Undone            -> fprintf fmt "Undone"
Sylvain Dailler's avatar
Sylvain Dailler committed
39 40 41
  | Scheduled         -> fprintf fmt "Scheduled"
  | Running           -> fprintf fmt "Running"
  | Done r            ->
42 43
      fprintf fmt "Done(%a)"
        (Call_provers.print_prover_result ~json_model:false) r
44 45
  | Interrupted       -> fprintf fmt "Interrupted"
  | Detached          -> fprintf fmt "Detached"
Sylvain Dailler's avatar
Sylvain Dailler committed
46 47 48 49
  | InternalFailure e ->
      fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e
  | Uninstalled pr    ->
      fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
50 51
  | UpgradeProver pr    ->
      fprintf fmt "Prover upgrade to %a" Whyconf.print_prover pr
52 53
  | Removed pr    ->
      fprintf fmt "Prover %a removed" Whyconf.print_prover pr
MARCHE Claude's avatar
MARCHE Claude committed
54 55

type transformation_status =
56
  | TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
Sylvain Dailler's avatar
Sylvain Dailler committed
57
  | TSfatal of (proofNodeID * exn)
58 59 60 61

let print_trans_status fmt st =
  match st with
  | TSscheduled -> fprintf fmt "TScheduled"
62
  | TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
63
  | TSfailed _e -> fprintf fmt "TSfailed"
Sylvain Dailler's avatar
Sylvain Dailler committed
64
  | TSfatal _e -> fprintf fmt "TSfatal"
Clément Fumex's avatar
Clément Fumex committed
65

66
type strategy_status = STSgoto of proofNodeID * int | STShalt
Sylvain Dailler's avatar
Sylvain Dailler committed
67
                     | STSfatal of string * proofNodeID * exn
68 69 70

let print_strategy_status fmt st =
  match st with
Sylvain Dailler's avatar
Sylvain Dailler committed
71 72
  | STSgoto(id,n) ->
      fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
73
  | STShalt -> fprintf fmt "halt"
Sylvain Dailler's avatar
Sylvain Dailler committed
74
  | STSfatal _ -> fprintf fmt "fatal"
75 76


77
type controller =
Sylvain Dailler's avatar
Sylvain Dailler committed
78
  { mutable controller_session: Session_itp.session;
79
    mutable controller_config : Whyconf.config;
MARCHE Claude's avatar
MARCHE Claude committed
80
    mutable controller_env: Env.env;
Sylvain Dailler's avatar
Sylvain Dailler committed
81 82
    controller_provers:
      (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
83
    controller_strategies : (string * string * string * Strategy.instruction array) Hstr.t;
84
    controller_running_proof_attempts : unit Hpan.t;
85 86
  }

87 88 89 90 91
let session_max_tasks = ref 1

let set_session_max_tasks n =
  session_max_tasks := n;
  Prove_client.set_max_running_provers n
92

93 94 95 96 97 98 99 100 101 102 103 104 105 106
let set_session_memlimit c n =
  let main = Whyconf.get_main c.controller_config in
  let timelimit = Whyconf.timelimit main in
  let run_max = Whyconf.running_provers_max main in
  let main = Whyconf.set_limits main timelimit n run_max in
  c.controller_config <- Whyconf.set_main c.controller_config main

let set_session_timelimit c n =
  let main = Whyconf.get_main c.controller_config in
  let memlimit = Whyconf.memlimit main in
  let run_max = Whyconf.running_provers_max main in
  let main = Whyconf.set_limits main n memlimit run_max in
  c.controller_config <- Whyconf.set_main c.controller_config main

107 108 109
let set_session_prover_upgrade_policy c p u =
  c.controller_config <- Whyconf.set_prover_upgrade_policy c.controller_config p u

MARCHE Claude's avatar
MARCHE Claude committed
110 111 112
let load_drivers c =
  let env = c.controller_env in
  let config = c.controller_config in
113 114 115 116
  let provers = Whyconf.get_provers config in
  Whyconf.Mprover.iter
    (fun _ p ->
     try
117
       let d = Whyconf.load_driver (Whyconf.get_main config) env p.Whyconf.driver [] in
118 119
       Whyconf.Hprover.add c.controller_provers p.Whyconf.prover (p,d)
     with e ->
Sylvain Dailler's avatar
Sylvain Dailler committed
120
       Debug.dprintf debug_call_prover
121 122 123
         "[Controller_itp] error while loading driver for prover %a: %a@."
         Whyconf.print_prover p.Whyconf.prover
         Exn_printer.exn_printer e)
MARCHE Claude's avatar
MARCHE Claude committed
124 125 126 127 128 129 130 131 132
    provers

let create_controller config env ses =
  let c =
    {
      controller_session = ses;
      controller_config = config;
      controller_env = env;
      controller_provers = Whyconf.Hprover.create 7;
133
      controller_strategies = Hstr.create 7;
MARCHE Claude's avatar
MARCHE Claude committed
134 135 136 137
      controller_running_proof_attempts = Hpan.create 17;
    }
  in
  load_drivers c;
138 139
  c

140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160

(* Cannot remove a proof_attempt that was scheduled but did not finish yet.
   It can be interrupted though. *)
let removable_proof_attempt c pa =
  try let () = Hpan.find c.controller_running_proof_attempts pa in false
  with Not_found -> true

let any_removable c any =
  match any with
  | APa pa -> removable_proof_attempt c pa
  | _ -> true

(* Check whether the subtree [n] contains an unremovable proof_attempt
   (ie: scheduled or running) *)
let check_removable c (n: any) =
  fold_all_any c.controller_session (fun acc any -> acc && any_removable c any) true n


let remove_subtree ~(notification:notifier) ~(removed:notifier) c (n: any) =
  if check_removable c n then
    Session_itp.remove_subtree ~notification ~removed c.controller_session n
161

162 163 164
(* Get children of any without proofattempts *)
let get_undetached_children_no_pa s any : any list =
  match any with
165
  | AFile f -> List.map (fun th -> ATh th) (file_theories f)
166 167 168
  | ATh th  -> List.map (fun g -> APn g) (theory_goals th)
  | ATn tn  -> List.map (fun pn -> APn pn) (get_sub_tasks s tn)
  | APn pn  -> List.map (fun tn -> ATn tn) (get_transformations s pn)
Sylvain Dailler's avatar
Sylvain Dailler committed
169
  | APa _ -> []
170

171 172


173 174 175 176 177 178 179 180 181 182
(* printing *)

module PSession = struct

  type any =
    | Session
    | File of file
    | Theory of theory
    | Goal of proofNodeID
    | Transf of transID
183
    | ProofAttempt of proof_attempt_node
184 185 186 187 188 189 190 191

  type 'a t = { tcont : controller;
                tkind : any }

  let decomp x =
    let s = x.tcont.controller_session in
    let n y acc = { x with tkind = y } :: acc in
    match x.tkind with
192
    | Session -> "", Hfile.fold (fun _ f -> n (File f)) (get_files s) []
193
    | File f ->
194
       string_of_file_path (file_path f),
195
       List.fold_right (fun th -> n (Theory th)) (file_theories f) []
196 197 198
    | Theory th ->
       let id = theory_name th in
       let name = id.Ident.id_string in
199
       let name = if th_proved s th then name^"!" else name^"?" in
200
       name,
Sylvain Dailler's avatar
Sylvain Dailler committed
201 202 203
       List.fold_right
         (fun g -> n (Goal g))
         (theory_goals th)
MARCHE Claude's avatar
MARCHE Claude committed
204
         []
205 206 207
    | Goal id ->
       let gid = get_proof_name s id in
       let name = gid.Ident.id_string in
208
       let name = if pn_proved s id then name^"!" else name^"?" in
209 210 211 212 213 214 215
       let pas = get_proof_attempts s id in
       let trs = get_transformations s id in
       name,
       List.fold_right (fun g -> n (Transf g)) trs
                       (List.fold_right (fun g -> n (ProofAttempt g)) pas [])
    | ProofAttempt pa ->
       Pp.sprintf_wnl "%a%s%s"
Sylvain Dailler's avatar
Sylvain Dailler committed
216 217 218 219 220
          Whyconf.print_prover pa.prover
          (match pa.Session_itp.proof_state with
          | Some { Call_provers.pr_answer = Call_provers.Valid} -> ""
          | _ -> "?")
          (if pa.proof_obsolete then "O" else ""), []
221 222
    | Transf id ->
       let name = get_transf_name s id in
223
       let name = if tn_proved s id then name^"!" else name^"?" in
224 225
       let sts = get_sub_tasks s id in
       name,
MARCHE Claude's avatar
MARCHE Claude committed
226
       List.fold_right (fun g -> n (Goal g)) sts []
227 228 229 230 231 232 233 234 235 236 237 238

end

module P = Print_tree.PMake(PSession)

let print_session fmt c =
  P.print fmt { PSession.tcont = c; PSession.tkind = PSession.Session }

(*********)



239 240 241 242 243 244

(** reload files, associating old proof attempts and transformations
    to the new goals.  old theories and old goals for which we cannot
    find a corresponding new theory resp. old goal are kept, with
    tasks associated to them *)

245
let reload_files (c : controller) ~shape_version =
246
  let old_ses = c.controller_session in
MARCHE Claude's avatar
MARCHE Claude committed
247
  c.controller_env <- Env.create_env (Env.get_loadpath c.controller_env);
MARCHE Claude's avatar
MARCHE Claude committed
248 249
  Whyconf.Hprover.reset c.controller_provers;
  load_drivers c;
250
  c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
251
  merge_files ~shape_version c.controller_env c.controller_session old_ses
252 253 254

exception Errors_list of exn list

255 256
let reload_files (c: controller) ~shape_version =
  let errors, b1, b2 = reload_files c ~shape_version in
257 258 259
  match errors with
  | [] -> b1, b2
  | _ -> raise (Errors_list errors)
260 261

let add_file c ?format fname =
262 263 264
  let file_is_detached,theories,errors =
    try false,(Session_itp.read_file c.controller_env ?format fname), None
    with e -> true,[], Some e
265
  in
266
  let (_ : file) = add_file_section c.controller_session fname ~file_is_detached theories format in
267
  errors
268

269 270 271 272 273
let add_file c ?format fname =
  let errors = add_file c ?format fname in
  match errors with
  | None -> ()
  | Some error -> raise (Errors_list [error])
274 275

module type Scheduler = sig
276
  val blocking: bool
277
  val multiplier: int
278 279 280 281
  val timeout: ms:int -> (unit -> bool) -> unit
  val idle: prio:int -> (unit -> bool) -> unit
end

282 283
module Make(S : Scheduler) = struct

Sylvain Dailler's avatar
Sylvain Dailler committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
(* type for scheduled proof attempts *)
type sched_pa_rec =
  { spa_contr    : controller;
    spa_id       : proofNodeID;
    spa_pr       : Whyconf.prover;
    spa_limit    : Call_provers.resource_limit;
    spa_pr_scr   : string option;
    spa_callback : (proof_attempt_status -> unit);
    spa_ores     : Call_provers.prover_result option;
  }

let scheduled_proof_attempts : sched_pa_rec Queue.t = Queue.create ()

(* type for prover tasks in progress *)
type tasks_prog_rec =
  {
    tp_session  : Session_itp.session;
    tp_id       : proofNodeID;
    tp_pr       : Whyconf.prover;
    tp_callback : (proof_attempt_status -> unit);
    tp_started  : bool;
    tp_call     : Call_provers.prover_call;
    tp_ores     : Call_provers.prover_result option;
  }
MARCHE Claude's avatar
MARCHE Claude committed
308

Sylvain Dailler's avatar
Sylvain Dailler committed
309 310 311
let prover_tasks_in_progress :
    (Call_provers.prover_call,tasks_prog_rec) Hashtbl.t =
  Hashtbl.create 17
312 313 314 315 316

(* We need to separate tasks that are edited from proofattempt in progress
   because we are not using why3server for the edited proofs and timeout_handler
   rely on a loop on why3server's results. *)
let prover_tasks_edited = Queue.create ()
MARCHE Claude's avatar
MARCHE Claude committed
317 318 319

let timeout_handler_running = ref false

320

MARCHE Claude's avatar
MARCHE Claude committed
321
let number_of_running_provers = ref 0
322

323 324 325 326
let observer = ref (fun _ _ _ -> ())

let register_observer = (:=) observer

327
module Hprover = Whyconf.Hprover
MARCHE Claude's avatar
MARCHE Claude committed
328

Sylvain Dailler's avatar
Sylvain Dailler committed
329
(* calling provers, with limits adaptation *)
330 331 332 333 334 335 336 337 338 339


(* to avoid corner cases when prover results are obtained very closely
   to the time or mem limits, we adapt these limits when we replay a
   proof *)

let adapt_limits ~interactive ~use_steps limits a =
  let t, m, s =
    let timelimit = limits.Call_provers.limit_time in
    let memlimit = limits.Call_provers.limit_mem in
340
    let steplimit = limits.Call_provers.limit_steps in
341 342 343 344 345 346 347
    match a.proof_state with
    | Some { Call_provers.pr_answer = r;
             Call_provers.pr_time = t;
             Call_provers.pr_steps = s } ->
       (* increased time limit is 1 + twice the previous running time,
       but enforced to remain inside the interval [l,2l] where l is
       the previous time limit *)
348
       let t = truncate (1.5 +. 2.0 *. t) in
349
       let increased_time = if interactive then 0
350 351 352 353 354
                            else max timelimit (min t (2 * timelimit)) in
       (* increased mem limit is just 1.5 times the previous mem limit *)
       let increased_mem = if interactive then 0 else 3 * memlimit / 2 in
       begin
         match r with
355 356
         | Call_provers.OutOfMemory -> increased_time, memlimit, steplimit
         | Call_provers.Timeout -> timelimit, increased_mem, steplimit
357 358
         | Call_provers.Valid ->
            let steplimit =
359 360 361 362 363 364 365 366 367
              if use_steps && not a.proof_obsolete then
                (* We need to allow at least one more step than what was used to
                   prove the same statement. Otherwise, the prover run out of
                   steps: this happens with cvc4 on some very fast proofs
                   (steps = 28).
                *)
                s + 1
              else
                0
368 369 370 371
            in
            increased_time, increased_mem, steplimit
         | Call_provers.Unknown _
         | Call_provers.StepLimitExceeded
372
         | Call_provers.Invalid -> increased_time, increased_mem, steplimit
373 374 375
         | Call_provers.Failure _
         | Call_provers.HighFailure ->
            (* correct ? failures are supposed to appear quickly anyway... *)
376
            timelimit, memlimit, steplimit
377 378
       end
    | None when interactive -> 0, 0, 0
379
    | None -> timelimit, memlimit, steplimit
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
  in
  { Call_provers.limit_time = t; limit_mem = m; limit_steps = s }

let group_answer a =
  match a with
  | Call_provers.OutOfMemory
  | Call_provers.Unknown _
  | Call_provers.Timeout -> Call_provers.Timeout
  | _ -> a

let fuzzy_proof_time nres ores =
  let ansold = ores.Call_provers.pr_answer in
  let told = ores.Call_provers.pr_time in
  let ansnew = nres.Call_provers.pr_answer in
  let tnew = nres.Call_provers.pr_time in
395
  if ansnew <> Call_provers.Timeout && group_answer ansold = group_answer ansnew &&
396 397 398 399 400
       tnew >= told *. 0.9 -. 0.1 && tnew <= told *. 1.1 +. 0.1
  then { nres with Call_provers.pr_time = told }
  else nres


Sylvain Dailler's avatar
Sylvain Dailler committed
401 402 403 404 405 406
let build_prover_call spa =
  let c = spa.spa_contr in
  let limit = spa.spa_limit in
  let (config_pr,driver) = Hprover.find c.controller_provers spa.spa_pr in
  let with_steps =
    Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
407
  let command =
408
    Whyconf.get_complete_command config_pr ~with_steps in
409
  try
Sylvain Dailler's avatar
Sylvain Dailler committed
410
    let task = Session_itp.get_task c.controller_session spa.spa_id in
411
    Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
Sylvain Dailler's avatar
Sylvain Dailler committed
412
                  (Pp.print_option Pp.string) spa.spa_pr_scr;
413
    let inplace = config_pr.Whyconf.in_place in
414
    let interactive = config_pr.Whyconf.interactive in
415 416
    try
      let call =
Sylvain Dailler's avatar
Sylvain Dailler committed
417 418
        Driver.prove_task ?old:spa.spa_pr_scr ~inplace ~command
                        ~limit ~interactive driver task
419
      in
Sylvain Dailler's avatar
Sylvain Dailler committed
420 421 422 423 424 425 426 427
      let pa =
        { tp_session  = c.controller_session;
          tp_id       = spa.spa_id;
          tp_pr       = spa.spa_pr;
          tp_callback = spa.spa_callback;
          tp_started  = false;
          tp_call     = call;
          tp_ores     = spa.spa_ores } in
428 429
      Hashtbl.replace prover_tasks_in_progress call pa
    with Sys_error _ as e ->
Sylvain Dailler's avatar
Sylvain Dailler committed
430
      spa.spa_callback (InternalFailure e)
431
  with Not_found (* goal has no task, it is detached *) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
432
       spa.spa_callback Detached
MARCHE Claude's avatar
MARCHE Claude committed
433

434 435
let update_observer () =
  let scheduled = Queue.length scheduled_proof_attempts in
436
  let waiting_or_running = Hashtbl.length prover_tasks_in_progress in
437 438 439
  let running = !number_of_running_provers in
  !observer scheduled (waiting_or_running - running) running

MARCHE Claude's avatar
MARCHE Claude committed
440 441
let timeout_handler () =
  (* examine all the prover tasks in progress *)
442 443 444
  (* When no tasks are there, probably no tasks were scheduled and the server
     was not launched so getting results could fail. *)
  if Hashtbl.length prover_tasks_in_progress != 0 then begin
445
    let results = Call_provers.get_new_results ~blocking:S.blocking in
446 447
    List.iter (fun (call, prover_update) ->
      match Hashtbl.find prover_tasks_in_progress call with
Sylvain Dailler's avatar
Sylvain Dailler committed
448
      | ptp ->
449
        begin match prover_update with
450 451
        | Call_provers.NoUpdates -> ()
        | Call_provers.ProverStarted ->
Sylvain Dailler's avatar
Sylvain Dailler committed
452 453
            assert (not ptp.tp_started);
            ptp.tp_callback Running;
454
            incr number_of_running_provers;
Sylvain Dailler's avatar
Sylvain Dailler committed
455 456
            Hashtbl.replace prover_tasks_in_progress ptp.tp_call
              {ptp with tp_started = true}
457
        | Call_provers.ProverFinished res ->
Sylvain Dailler's avatar
Sylvain Dailler committed
458 459 460
            Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
            if ptp.tp_started then decr number_of_running_provers;
            let res = Opt.fold fuzzy_proof_time res ptp.tp_ores in
461
            (* inform the callback *)
Sylvain Dailler's avatar
Sylvain Dailler committed
462
            ptp.tp_callback (Done res)
463
        | Call_provers.ProverInterrupted ->
Sylvain Dailler's avatar
Sylvain Dailler committed
464 465
            Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
            if ptp.tp_started then decr number_of_running_provers;
466
            (* inform the callback *)
Sylvain Dailler's avatar
Sylvain Dailler committed
467
            ptp.tp_callback (Interrupted)
468
        | Call_provers.InternalFailure exn ->
Sylvain Dailler's avatar
Sylvain Dailler committed
469 470
            Hashtbl.remove prover_tasks_in_progress ptp.tp_call;
            if ptp.tp_started then decr number_of_running_provers;
471
            (* inform the callback *)
Sylvain Dailler's avatar
Sylvain Dailler committed
472
            ptp.tp_callback (InternalFailure (exn))
473 474 475 476 477 478
        end
      | exception Not_found -> ()
        (* We probably received ProverStarted after ProverFinished,
           because what is sent to and received from the server is
           not ordered. *)
    ) results;
479 480
  end;

481 482 483 484 485 486 487
  (* When blocking is activated, we are in script mode and we don't want editors
     to be launched so we don't need to go in this loop. *)
  if not S.blocking then begin
    (* Check for editor calls which are not finished *)
    let q = Queue.create () in
    while not (Queue.is_empty prover_tasks_edited) do
      (* call is an EditorCall *)
488
      let (callback,call,ores) as c =
489 490 491 492
        Queue.pop prover_tasks_edited in
      let prover_update = Call_provers.query_call call in
      match prover_update with
      | Call_provers.NoUpdates -> Queue.add c q
493
      | Call_provers.ProverFinished res ->
494 495
          (* res is meaningless for edition, we returned the old result *)
          (* inform the callback *)
496
          callback (match ores with None -> Done res | Some r -> Done r)
497 498 499 500
      | _ -> assert (false) (* An edition can only return Noupdates or finished *)
    done;
    Queue.transfer q prover_tasks_edited;
  end;
501 502

  (* if the number of prover tasks is less than S.multiplier times the maximum
MARCHE Claude's avatar
MARCHE Claude committed
503 504
     number of running provers, then we heuristically decide to add
     more tasks *)
505 506
  begin
    try
507
      for _i = Hashtbl.length prover_tasks_in_progress
508
          to S.multiplier * !session_max_tasks do
Sylvain Dailler's avatar
Sylvain Dailler committed
509 510
        let spa = Queue.pop scheduled_proof_attempts in
        try build_prover_call spa
511
        with e when not (Debug.test_flag Debug.stack_trace) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
512
          spa.spa_callback (InternalFailure e)
513 514 515
      done
  with Queue.Empty -> ()
  end;
516
  update_observer ();
517
  true
MARCHE Claude's avatar
MARCHE Claude committed
518

519
let interrupt () =
520
  (* Interrupt provers *)
MARCHE Claude's avatar
MARCHE Claude committed
521 522 523 524
  Hashtbl.iter
    (fun call e ->
     Call_provers.interrupt_call call;
     e.tp_callback Interrupted)
525 526 527 528
    prover_tasks_in_progress;
  Hashtbl.clear prover_tasks_in_progress;
  (* Do not interrupt editors
  while not (Queue.is_empty prover_tasks_edited) do
529
    let (_ses,_id,_pr,callback,_started,_call,_ores) =
530
      Queue.pop prover_tasks_edited in
531 532
    callback Interrupted
  done;
533
  *)
534 535
  number_of_running_provers := 0;
  while not (Queue.is_empty scheduled_proof_attempts) do
Sylvain Dailler's avatar
Sylvain Dailler committed
536 537
    let spa = Queue.pop scheduled_proof_attempts in
    spa.spa_callback Interrupted
538 539 540
  done;
  !observer 0 0 0

MARCHE Claude's avatar
MARCHE Claude committed
541 542 543 544
let run_timeout_handler () =
  if not !timeout_handler_running then
    begin
      timeout_handler_running := true;
545
      S.timeout ~ms:default_delay_ms timeout_handler;
MARCHE Claude's avatar
MARCHE Claude committed
546 547
    end

548
let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
549 550
  let ses = c.controller_session in
  let callback panid s =
551 552
    begin
      match s with
553
      | UpgradeProver _ | Removed _ -> ()
554 555 556 557 558 559 560 561
      | Scheduled ->
         Hpan.add c.controller_running_proof_attempts panid ();
         update_goal_node notification ses id
      | Running -> update_goal_node notification ses id
      | Done res ->
         Hpan.remove c.controller_running_proof_attempts panid;
         update_proof_attempt ~obsolete:false notification ses id pr res;
         update_goal_node notification ses id
562 563
      | Interrupted
      | InternalFailure _ ->
564 565 566 567 568
         Hpan.remove c.controller_running_proof_attempts panid;
         (* what to do ?
         update_proof_attempt ~obsolete:false notification ses id pr res;
          *)
         update_goal_node notification ses id
569 570
      | Detached -> assert false
      | Uninstalled _ -> assert false
571
      | Undone -> assert false
572
    end;
573 574 575
    callback panid s
  in
  let adaptlimit,ores,proof_script =
576
    try
577
      let h = get_proof_attempt_ids ses id in
578
      let pa = Hprover.find h pr in
579
      let a = get_proof_attempt_node ses pa in
580 581 582 583 584
      let old_res = a.proof_state in
      let config_pr,_ = Hprover.find c.controller_provers pr in
      let interactive = config_pr.Whyconf.interactive in
      let use_steps = Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
      let limit = adapt_limits ~interactive ~use_steps limit a in
585 586 587
      let script =
        if save_to = None then
          Opt.map (fun s ->
588 589
                            Debug.dprintf debug_sched "Script file = %s@." s;
                            Filename.concat (get_dir ses) s) a.proof_script
590 591
        else
          save_to
592 593
      in
      limit, old_res, script
594
    with Not_found | Session_itp.BadID -> limit,None,save_to
595
  in
596
  let panid = graft_proof_attempt ~limit ses id pr in
Sylvain Dailler's avatar
Sylvain Dailler committed
597 598 599 600 601 602 603 604 605
  let spa =
    { spa_contr    = c;
      spa_id       = id;
      spa_pr       = pr;
      spa_limit    = adaptlimit;
      spa_pr_scr   = proof_script;
      spa_callback = callback panid;
      spa_ores     = ores } in
  Queue.add spa scheduled_proof_attempts;
606
  callback panid Scheduled;
MARCHE Claude's avatar
MARCHE Claude committed
607
  run_timeout_handler ()
Clément Fumex's avatar
Clément Fumex committed
608

609

610 611


612 613
(*** { 2 edition of proof scripts} *)

Sylvain Dailler's avatar
Sylvain Dailler committed
614 615 616
(* create the path to a file for saving the external proof script *)
let create_file_rel_path c pr pn =
  let session = c.controller_session in
617
  let driver = snd (Hprover.find c.controller_provers pr) in
618
  let task = Session_itp.get_task session pn in
Sylvain Dailler's avatar
Sylvain Dailler committed
619 620 621 622
  let session_dir = Session_itp.get_dir session in
  let th = get_encapsulating_theory session (APn pn) in
  let th_name = (Session_itp.theory_name th).Ident.id_string in
  let f = get_encapsulating_file session (ATh th) in
623
  let fn = Filename.chop_extension (Session_itp.basename (file_path f)) in
Sylvain Dailler's avatar
Sylvain Dailler committed
624 625 626 627
  let file = Driver.file_of_task driver fn th_name task in
  let file = Filename.concat session_dir file in
  let file = Sysutil.uniquify file in
  let file = Sysutil.relativize_filename session_dir file in
628 629 630
  match file with
  | [f] -> f
  | _ -> assert false
Sylvain Dailler's avatar
Sylvain Dailler committed
631

632
let prepare_edition c ?file pn pr ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
633
  let session = c.controller_session in
634 635 636
  let proof_attempts_id = get_proof_attempt_ids session pn in
  let panid =
    try
637 638 639 640 641 642 643 644 645 646 647 648 649 650
      let panid = Hprover.find proof_attempts_id pr in
      (* if no proof script yet, we need to add one
         it happens e.g when editing a file for an automatic prover
       *)
      let pa = get_proof_attempt_node session panid in
      match pa.proof_script with
      | None ->
         let file = match file with
           | Some f -> f
           | None -> create_file_rel_path c pr pn
         in
         set_proof_script pa file;
         panid
      | Some _ -> panid
651
    with Not_found ->
652 653 654 655
      let file = match file with
        | Some f -> f
        | None -> create_file_rel_path c pr pn
      in
656 657
      let limit = Call_provers.empty_limit in
      graft_proof_attempt session pn pr ~file ~limit
Sylvain Dailler's avatar
Sylvain Dailler committed
658
  in
659
  update_goal_node notification session pn;
660 661
  let pa = get_proof_attempt_node session panid in
  let file = Opt.get pa.proof_script in
662
  let old_res = pa.proof_state in
663
  let session_dir = Session_itp.get_dir session in
Sylvain Dailler's avatar
Sylvain Dailler committed
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
  let file = Filename.concat session_dir file in
  let old =
    if Sys.file_exists file
    then
      begin
        let backup = file ^ ".bak" in
        if Sys.file_exists backup
        then Sys.remove backup;
        Sys.rename file backup;
        Some(open_in backup)
      end
    else None
  in
  let ch = open_out file in
  let fmt = formatter_of_out_channel ch in
679
  let task = Session_itp.get_task session pn in
680
  let driver = snd (Hprover.find c.controller_provers pr) in
681
  Driver.print_task ?old driver fmt task;
Sylvain Dailler's avatar
Sylvain Dailler committed
682 683
  Opt.iter close_in old;
  close_out ch;
684
  panid,file,old_res
Sylvain Dailler's avatar
Sylvain Dailler committed
685 686 687

exception Editor_not_found

688
let schedule_edition c id pr ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
689 690 691 692
  Debug.dprintf debug_sched "[Sched] Scheduling an edition@.";
  let config = c.controller_config in
  let session = c.controller_session in
  let prover_conf = Whyconf.get_prover_config config pr in
693
  (* Make sure editor exists. Fails otherwise *)
Sylvain Dailler's avatar
Sylvain Dailler committed
694 695
  let editor =
    match prover_conf.Whyconf.editor with
696
    | "" -> Whyconf.(default_editor (get_main config))
Sylvain Dailler's avatar
Sylvain Dailler committed
697
    | s ->
698 699 700 701 702
       try
         let ed = Whyconf.editor_by_id config s in
         String.concat " " (ed.Whyconf.editor_command ::
                              ed.Whyconf.editor_options)
       with Not_found -> raise Editor_not_found
Sylvain Dailler's avatar
Sylvain Dailler committed
703
  in
704
  let panid,file,old_res = prepare_edition c id pr ~notification in
705
  (* Notification node *)
706 707 708
  let callback panid s =
    begin
      match s with
709
      | UpgradeProver _ -> ()
710
      | Running -> ()
711 712
      | Done res ->
         (* set obsolete to true since we do not know if the manual
713
            proof was completed or not *)
714 715 716 717 718
         Debug.dprintf debug_sched
                       "Setting status of %a under parent %a to obsolete@."
                       print_proofAttemptID panid print_proofNodeID id;
         update_proof_attempt ~obsolete:true notification session id pr res;
         update_goal_node notification session id
719 720 721
      | Interrupted
      | InternalFailure _ ->
         update_goal_node notification session id
722
      | Undone | Detached | Uninstalled _ | Scheduled | Removed _ -> assert false
723 724
    end;
    callback panid s
725
  in
Sylvain Dailler's avatar
Sylvain Dailler committed
726
  Debug.dprintf debug_sched "[Editing] goal %s with command '%s' on file %s@."
727 728
                (Session_itp.get_proof_name session id).Ident.id_string
                editor file;
729 730
  let call = Call_provers.call_editor ~command:editor file in
  callback panid Running;
731
  Queue.add (callback panid,call,old_res) prover_tasks_edited;
732
  run_timeout_handler ()
733

734
exception TransAlreadyExists of string * string
735
exception GoalNodeDetached of proofNodeID
736

737 738
(*** { 2 transformations} *)

739 740 741 742 743
let schedule_transformation c id name args ~callback ~notification =
  let callback s =
    begin match s with
          | TSdone tid -> update_trans_node notification c.controller_session tid
          | TSscheduled
Sylvain Dailler's avatar
Sylvain Dailler committed
744
          | TSfailed _ | TSfatal _  -> ()
745 746 747
    end;
    callback s
  in
748
  let apply_trans () =
749 750
    begin
      try
751 752 753
        let subtasks =
          apply_trans_to_goal ~allow_no_effect:false
                              c.controller_session c.controller_env name args id
754
        in
755 756 757
        let tid = graft_transf c.controller_session id name args subtasks in
        callback (TSdone tid)
      with
758
      | NoProgress ->
759 760 761
          (* if result is same as input task, consider it as a failure *)
          callback (TSfailed (id, NoProgress))
      | e when not (is_fatal e) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
762
          callback (TSfailed (id, e))
763
      | e when not (Debug.test_flag Debug.stack_trace) ->
764
          (* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
765
          name Exn_printer.exn_printer e; TODO *)
766
          callback (TSfatal (id, e))
767 768
    end;
    false
769
  in
770 771
  if Session_itp.is_detached c.controller_session (APn id) then
    raise (GoalNodeDetached id);
772 773
  if Session_itp.check_if_already_exists c.controller_session id name args then
    raise (TransAlreadyExists (name, List.fold_left (fun acc s -> s ^ " " ^ acc) "" args));
774 775
  S.idle ~prio:0 apply_trans;
  callback TSscheduled
Clément Fumex's avatar
Clément Fumex committed
776

777 778 779

open Strategy

Sylvain Dailler's avatar
Sylvain Dailler committed
780
let run_strategy_on_goal
781
    c id strat ~callback_pa ~callback_tr ~callback ~notification =
782 783 784 785 786 787
  let rec exec_strategy pc strat g =
    if pc < 0 || pc >= Array.length strat then
      callback STShalt
    else
      match Array.get strat pc with
      | Icall_prover(p,timelimit,memlimit) ->
788 789 790
         let main = Whyconf.get_main c.controller_config in
         let timelimit = Opt.get_def (Whyconf.timelimit main) timelimit in
         let memlimit = Opt.get_def (Whyconf.memlimit main) memlimit in
MARCHE Claude's avatar
MARCHE Claude committed
791 792
         let callback panid res =
           callback_pa panid res;
793
           match res with
794
           | UpgradeProver _ | Scheduled | Running -> (* nothing to do yet *) ()
795 796 797
           | Done { Call_provers.pr_answer = Call_provers.Valid } ->
              (* proof succeeded, nothing more to do *)
              callback STShalt
798 799
           | Interrupted | InternalFailure _ ->
              callback STShalt
800 801 802 803 804
           | Done _ ->
              (* proof did not succeed, goto to next step *)
              callback (STSgoto (g,pc+1));
              let run_next () = exec_strategy (pc+1) strat g; false in
              S.idle ~prio:0 run_next
805
           | Undone | Detached | Uninstalled _ | Removed _ ->
806 807 808 809 810 811
                         (* should not happen *)
                         assert false
         in
         let limit = { Call_provers.empty_limit with
                       Call_provers.limit_time = timelimit;
                       limit_mem  = memlimit} in
812
         schedule_proof_attempt c g p ?save_to:None ~limit ~callback ~notification
813 814
      | Itransform(trname,pcsuccess) ->
         let callback ntr =
815
           callback_tr trname [] ntr;
816
           match ntr with
Sylvain Dailler's avatar
Sylvain Dailler committed
817 818
           | TSfatal (id, e) ->
               callback (STSfatal (trname, id, e))
819
           | TSfailed _e -> (* transformation failed *)
820 821 822 823 824 825 826 827 828 829 830 831
              callback (STSgoto (g,pc+1));
              let run_next () = exec_strategy (pc+1) strat g; false in
              S.idle ~prio:0 run_next
           | TSscheduled -> ()
           | TSdone tid ->
              List.iter
                (fun g ->
                 callback (STSgoto (g,pcsuccess));
                 let run_next () =
                   exec_strategy pcsuccess strat g; false
                 in
                 S.idle ~prio:0 run_next)
MARCHE Claude's avatar
MARCHE Claude committed
832
                (get_sub_tasks c.controller_session tid)
833
         in
834
         schedule_transformation c g trname [] ~callback ~notification
835 836 837 838 839 840
      | Igoto pc ->
         callback (STSgoto (g,pc));
         exec_strategy pc strat g
  in
  exec_strategy 0 strat id

Sylvain Dailler's avatar
Sylvain Dailler committed
841 842
let schedule_pa_with_same_arguments
    c (pa: proof_attempt_node) (pn: proofNodeID) ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
843 844 845 846
  let prover = pa.prover in
  let limit = pa.limit in
  schedule_proof_attempt c pn prover ~limit ~callback ~notification

Sylvain Dailler's avatar
Sylvain Dailler committed
847 848
let schedule_tr_with_same_arguments
    c (tr: transID) (pn: proofNodeID) ~callback ~notification =
Sylvain Dailler's avatar
Sylvain Dailler committed
849 850 851
  let s = c.controller_session in
  let args = get_transf_args s tr in
  let name = get_transf_name s tr in
852
  let callback = callback name args in
853

Sylvain Dailler's avatar
Sylvain Dailler committed
854 855
  schedule_transformation c pn name args ~callback ~notification

MARCHE Claude's avatar
MARCHE Claude committed
856 857 858 859 860
let proof_is_complete pa =
  match pa.Session_itp.proof_state with
  | None -> false
  | Some pr ->
     not pa.Session_itp.proof_obsolete &&
861
       Call_provers.(pr.pr_answer = Valid)
MARCHE Claude's avatar
MARCHE Claude committed
862

863

Sylvain Dailler's avatar
Sylvain Dailler committed
864
let clean c ~removed nid =
865

866
  (* clean should not change proved status *)
867 868 869
  let notification any =
    Format.eprintf "Cleaning error: cleaning attempts to change status of node %a@." fprintf_any any
  in
870
  let s = c.controller_session in
871
  (* This function is applied on leafs first for the case of removes *)
872
  let clean_aux () any =
873 874 875 876 877 878
    let do_remove =
      Session_itp.is_detached s any ||
      match any with
      | APa pa ->
         let pa = Session_itp.get_proof_attempt_node s pa in
         pn_proved s pa.parent && not (proof_is_complete pa)
879
      | ATn tn ->
880 881 882 883 884 885
         let pn = get_trans_parent s tn in
         pn_proved s pn && not (tn_proved s tn)
      | _ -> false
    in
    if do_remove then
      remove_subtree ~notification ~removed c any
886
  in
887 888 889 890 891
  match nid with
  | Some nid ->
      Session_itp.fold_all_any s clean_aux () nid
  | None ->
      Session_itp.fold_all_session s clean_aux ()
892

893 894 895 896 897 898 899 900 901 902 903 904 905 906
let reset_proofs c ~removed ~notification nid =
  let s = c.controller_session in
  (* This function is applied on leafs first for the case of removes *)
  let clean_aux () any =
    let do_remove =
      Session_itp.is_detached s any ||
      match any with
      | APa _ -> true
      | ATn _ -> true
      | _ -> false
    in
    if do_remove then
      remove_subtree ~notification ~removed c any
  in
907 908 909 910 911
  match nid with
  | Some nid ->
      Session_itp.fold_all_any s clean_aux () nid
  | None ->
      Session_itp.fold_all_session s clean_aux ()
912

913 914
(* This function folds on any subelements of given node and tries to mark all
   proof attempts it encounters *)
915
let mark_as_obsolete ~notification c any =
916
  let s = c.controller_session in
917
  (* Case for proof attempt only *)
918
  let mark_as_obsolete_pa n =
919 920
    let parent = get_proof_attempt_parent s n in
    Session_itp.mark_obsolete s n;
921
    notification (APa n);
922
    update_goal_node notification s parent
923
  in
924 925 926 927 928 929 930 931 932 933
  match any with
  | Some any ->
      fold_all_any s
        (fun () any -> match any with
        | APa n -> mark_as_obsolete_pa n
        | _ -> ()) () any
  | None ->
      session_iter_proof_attempt
        (fun pa _pan ->
          mark_as_obsolete_pa pa) s
934

Sylvain Dailler's avatar
Sylvain Dailler committed
935 936 937
exception BadCopyPaste

(* Reproduce the transformation made on node on an other one *)
938
let rec copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any =
Sylvain Dailler's avatar
Sylvain Dailler committed
939
  let s = c.controller_session in
940 941
  match from_any, to_any with
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
942 943 944 945
    | AFile _, AFile _ ->
        raise BadCopyPaste
    | ATh _from_th, ATh _to_th ->
        raise BadCopyPaste
946
 *)
Sylvain Dailler's avatar
Sylvain Dailler committed
947 948
    | APn from_pn, APn to_pn ->
      let from_pa_list = get_proof_attempts s from_pn in
949
      List.iter (fun x -> schedule_pa_with_same_arguments ?save_to:None c x to_pn
Sylvain Dailler's avatar
Sylvain Dailler committed
950 951
          ~callback:callback_pa ~notification) from_pa_list;
      let from_tr_list = get_transformations s from_pn in
952
      let callback x tr args st = callback_tr tr args st;
Sylvain Dailler's avatar
Sylvain Dailler committed
953
        match st with
Sylvain Dailler's avatar
Sylvain Dailler committed
954
        | TSdone tid ->
955
          copy_rec c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr
Sylvain Dailler's avatar
Sylvain Dailler committed
956 957 958 959 960 961 962
        | _ -> ()
      in
      List.iter (fun x -> schedule_tr_with_same_arguments c x to_pn
          ~callback:(callback x) ~notification) from_tr_list
    | ATn from_tn, ATn to_tn ->
        let from_tn_list = get_sub_tasks s from_tn in
        let to_tn_list = get_sub_tasks s to_tn in
963 964 965 966 967 968 969 970
        let rec iter_copy l1 l2 =
          match l1,l2 with
          | x::r1, y::r2 ->
             copy_rec c (APn x) (APn y)
                      ~notification ~callback_pa ~callback_tr;
             iter_copy r1 r2
          | _ -> ()
        in iter_copy from_tn_list to_tn_list
Sylvain Dailler's avatar
Sylvain Dailler committed
971 972 973
    | _ -> raise BadCopyPaste


974 975
let copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
  let s = c.controller_session in
976 977
  if is_below s to_any from_any then
    raise BadCopyPaste;
978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993
  match from_any, to_any with
  | APn _, APn _ ->
     copy_rec ~notification ~callback_pa ~callback_tr c from_any to_any
  | ATn from_tn, APn to_pn ->
     let callback tr args st =
       callback_tr tr args st;
       match st with
       | TSdone tid ->
          copy_rec c (ATn from_tn) (ATn tid) ~notification ~callback_pa ~callback_tr
       | _ -> ()
     in
     schedule_tr_with_same_arguments c from_tn to_pn ~callback ~notification
  | _ -> raise BadCopyPaste



MARCHE Claude's avatar
MARCHE Claude committed
994 995 996 997 998 999 1000 1001





(***************** {2 replay} ****************)


1002
let debug_replay = Debug.register_flag "replay" ~desc:"Debug@ info@ for@ replay"
MARCHE Claude's avatar
MARCHE Claude committed
1003

1004
let find_prover notification c goal_id pr =
1005
  if Hprover.mem c.controller_provers pr then `Found pr else
1006
   match Whyconf.get_prover_upgrade_policy c.controller_config pr with
1007 1008
   | exception Not_found -> `Keep
   | Whyconf.CPU_keep -> `Keep
1009
   | Whyconf.CPU_remove -> `Remove
1010 1011 1012
   | Whyconf.CPU_upgrade new_pr ->
      (* does a proof using new_pr already exists ? *)
      if Hprover.mem (get_proof_attempt_ids c.controller_session goal_id) new_pr
1013
      then (* yes, then we remove the attempt *)
1014
        `Remove
1015 1016 1017 1018
      else
        begin
          (* we modify the prover in-place *)
          Session_itp.change_prover notification c.controller_session goal_id pr new_pr;
1019
          `Found new_pr
1020
        end
1021 1022 1023
   | Whyconf.CPU_duplicate new_pr ->
      (* does a proof using new_pr already exists ? *)
      if Hprover.mem (get_proof_attempt_ids c.controller_session goal_id) new_pr
1024
      then (* yes, then we do nothing *)
1025
        `Keep
1026 1027
      else
        begin
1028 1029
          (* we duplicate the proof attempt *)
          `Found new_pr
1030
        end
1031

1032 1033 1034 1035 1036

let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notification =
  (* The replay can be done on a different machine so we need
     to check more things before giving the attempt to the scheduler *)
  match find_prover notification c parid pr with
1037 1038
  | `Keep -> callback id (Uninstalled pr)
  | `Remove ->
1039 1040 1041
     (* it is necessary to call the callback before effectively removing the node, otherwise, a bad id will be used in the callback *)
      callback id (Removed pr);
      remove_proof_attempt c.controller_session parid pr
1042
  | `Found pr' ->
1043 1044
     try
       if pr' <> pr then callback id (UpgradeProver pr');
1045
       let _ = get_task c.controller_session parid in
1046
       schedule_proof_attempt ?save_to:None c parid pr' ~limit ~callback ~notification
1047 1048 1049 1050 1051
     with Not_found ->
       callback id Detached



1052 1053 1054 1055
type report =
  | Result of Call_provers.prover_result * Call_provers.prover_result
  (** Result(new_result,old_result) *)
  | CallFailed of exn
1056
  | Replay_interrupted
1057 1058 1059 1060 1061 1062 1063 1064 1065
  | Prover_not_installed
  | Edited_file_absent of string
  | No_former_result of Call_provers.prover_result

(* TODO find a better way to print it *)
let print_report fmt (r: report) =
  match r with
  | Result (new_r, old_r) ->
    Format.fprintf fmt "new_result = %a, old_result = %a@."
1066 1067
      (Call_provers.print_prover_result ~json_model:false) new_r
      (Call_provers.print_prover_result ~json_model:false) old_r
1068 1069 1070 1071
  | CallFailed e ->
    Format.fprintf fmt "Callfailed %a@." Exn_printer.exn_printer e
  | Replay_interrupted ->
    Format.fprintf fmt "Interrupted@."
1072 1073 1074 1075 1076 1077
  | Prover_not_installed ->
    Format.fprintf fmt "Prover not installed@."
  | Edited_file_absent _ ->
    Format.fprintf fmt "No edited file@."
  | No_former_result new_r ->
    Format.fprintf fmt</