replay.ml 16 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
19 20


21
open Why3
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26


let includes = ref []
let file = ref None
let opt_version = ref false
27
let opt_stats = ref true
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
28 29
let opt_latex = ref ""
let opt_latex2 = ref ""
30
let opt_force = ref false
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
36 37 38
  ("-force",
   Arg.Set opt_force,
   "enforce saving of session even if replay failed") ;
39 40 41
  ("-s",
   Arg.Clear opt_stats,
   " do not print statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44
  ("-v",
   Arg.Set opt_version,
   " print version information") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
45
  ("-latex",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
46
   Arg.Set_string opt_latex,
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
47
   " produce latex statistics") ;
Asma Tafat's avatar
Asma Tafat committed
48
  ("-latex2",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
49
   Arg.Set_string opt_latex2,
Asma Tafat's avatar
Asma Tafat committed
50
   " produce latex statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
51 52 53 54 55 56 57 58 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
]

let version_msg = Format.sprintf "Why3 replayer, version %s (build date: %s)"
  Config.version Config.builddate

let usage_str = Format.sprintf
  "Usage: %s [options] [<file.why>|<project directory>]"
  (Filename.basename Sys.argv.(0))

let set_file f = match !file with
  | Some _ ->
      raise (Arg.Bad "only one parameter")
  | None ->
      file := Some f

let () = Arg.parse spec set_file usage_str

let () =
  if !opt_version then begin
    Format.printf "%s@." version_msg;
    exit 0
  end

let fname = match !file with
  | None ->
      Arg.usage spec usage_str;
      exit 1
  | Some f ->
      f

let config = Whyconf.read_config None

let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
MARCHE Claude's avatar
MARCHE Claude committed
84
  @ List.rev !includes
MARCHE Claude's avatar
MARCHE Claude committed
85

Andrei Paskevich's avatar
Andrei Paskevich committed
86
let env = Env.create_env_of_loadpath loadpath
MARCHE Claude's avatar
MARCHE Claude committed
87

MARCHE Claude's avatar
MARCHE Claude committed
88
let provers = Whyconf.get_provers config
MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102

let provers =
  Util.Mstr.fold (Session.get_prover_data env) provers Util.Mstr.empty

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


let idle_handler = ref None
let timeout_handler = ref None

module M = Session.Make
  (struct
     type key = int

MARCHE Claude's avatar
MARCHE Claude committed
103
     let create ?parent () =
MARCHE Claude's avatar
MARCHE Claude committed
104 105 106 107 108 109
       match parent with
         | None -> 0
         | Some  n -> n+1

     let remove _row = ()

MARCHE Claude's avatar
MARCHE Claude committed
110 111
     let reset () = ()

MARCHE Claude's avatar
MARCHE Claude committed
112 113 114 115 116 117 118 119 120 121
     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"

122 123
     let notify_timer_state _ _ _ = ()

MARCHE Claude's avatar
MARCHE Claude committed
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
   end)



let main_loop () =
  let last = ref (Unix.gettimeofday ()) in
  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
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153
        | None ->
            begin
              let ms =
MARCHE Claude's avatar
MARCHE Claude committed
154
                match !timeout_handler with
155
                  | None -> 100.0 (* raise Exit *)
MARCHE Claude's avatar
MARCHE Claude committed
156 157 158 159
                  | Some(ms,_) -> ms
              in
              usleep (ms -. time)
            end
MARCHE Claude's avatar
MARCHE Claude committed
160
        | Some f ->
MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164 165 166 167 168 169
            let b = f () in
            if b then () else
              begin
                idle_handler := None;
              end
  done

open Format

170
(*
MARCHE Claude's avatar
MARCHE Claude committed
171
let model_index = Hashtbl.create 257
172
*)
MARCHE Claude's avatar
MARCHE Claude committed
173

MARCHE Claude's avatar
MARCHE Claude committed
174
let init =
175
(*
MARCHE Claude's avatar
MARCHE Claude committed
176
  let cpt = ref 0 in
177
*)
MARCHE Claude's avatar
MARCHE Claude committed
178
  fun _row any ->
179
(*
MARCHE Claude's avatar
MARCHE Claude committed
180 181
    incr cpt;
    Hashtbl.add model_index !cpt any;
182
*)
183
    let _name =
MARCHE Claude's avatar
MARCHE Claude committed
184 185 186 187
      match any with
        | M.Goal g -> M.goal_expl g
        | M.Theory th -> M.theory_name th
        | M.File f -> Filename.basename f.M.file_name
MARCHE Claude's avatar
MARCHE Claude committed
188
        | M.Proof_attempt a ->
189 190 191
            begin
              match a.M.prover with
                | M.Detected_prover p ->
192
                    p.Session.prover_name ^ " " ^ p.Session.prover_version
193 194
                | M.Undetected_prover s -> s
            end
MARCHE Claude's avatar
MARCHE Claude committed
195 196
        | M.Transformation tr -> Session.transformation_id tr.M.transf
    in
MARCHE Claude's avatar
MARCHE Claude committed
197 198
    (* eprintf "Item '%s' loaded@." name *)
    ()
MARCHE Claude's avatar
MARCHE Claude committed
199

MARCHE Claude's avatar
MARCHE Claude committed
200
(*
MARCHE Claude's avatar
MARCHE Claude committed
201
let string_of_result result =
MARCHE Claude's avatar
MARCHE Claude committed
202 203 204 205 206 207
  match result with
    | Session.Undone -> "undone"
    | Session.Scheduled -> "scheduled"
    | Session.Running -> "running"
    | Session.InternalFailure _ -> "internal failure"
    | Session.Done r -> match r.Call_provers.pr_answer with
208 209 210 211 212 213
        | Call_provers.Valid -> "valid"
        | Call_provers.Invalid -> "invalid"
        | Call_provers.Timeout -> "timeout"
        | Call_provers.Unknown _ -> "unknown"
        | Call_provers.Failure _ -> "failure"
        | Call_provers.HighFailure -> "high failure"
MARCHE Claude's avatar
MARCHE Claude committed
214

MARCHE Claude's avatar
MARCHE Claude committed
215
let print_result fmt res =
MARCHE Claude's avatar
MARCHE Claude committed
216 217
  let t = match res with
    | Session.Done { Call_provers.pr_time = time } ->
218
        Format.sprintf "(%.1f)" time
MARCHE Claude's avatar
MARCHE Claude committed
219 220 221
    | _ -> ""
  in
  fprintf fmt "%s%s" (string_of_result res) t
MARCHE Claude's avatar
MARCHE Claude committed
222 223
*)

MARCHE Claude's avatar
MARCHE Claude committed
224

MARCHE Claude's avatar
MARCHE Claude committed
225 226
let print_result fmt
    {Call_provers.pr_answer=ans; Call_provers.pr_output=out;
227 228
     Call_provers.pr_time=_t} =
(*
MARCHE Claude's avatar
MARCHE Claude committed
229
  fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
230 231
*)
  fprintf fmt "%a" Call_provers.print_prover_answer ans;
MARCHE Claude's avatar
MARCHE Claude committed
232 233
  if ans == Call_provers.HighFailure then
    fprintf fmt "@\nProver output:@\n%s@." out
MARCHE Claude's avatar
MARCHE Claude committed
234

235 236
let notify _any = ()
(*
MARCHE Claude's avatar
MARCHE Claude committed
237 238
  match any with
    | M.Goal g ->
239
        printf "Goal '%s' proved: %b@." (M.goal_expl g) (M.goal_proved g)
MARCHE Claude's avatar
MARCHE Claude committed
240
    | M.Theory th ->
241
        printf "Theory '%s' verified: %b@." (M.theory_name th) (M.verified th)
MARCHE Claude's avatar
MARCHE Claude committed
242
    | M.File file ->
243
        printf "File '%s' verified: %b@." (Filename.basename file.M.file_name)
MARCHE Claude's avatar
MARCHE Claude committed
244 245 246
          file.M.file_verified
    | M.Proof_attempt a ->
        let p = a.M.prover in
247 248
        printf "Proof with '%s %s' gives %a@."
          p.Session.prover_name p.Session.prover_version
MARCHE Claude's avatar
MARCHE Claude committed
249 250
          print_result a.M.proof_state
    | M.Transformation tr ->
251
        printf "Transformation '%s' proved: %b@."
MARCHE Claude's avatar
MARCHE Claude committed
252
          (Session.transformation_id tr.M.transf) tr.M.transf_proved
253
*)
MARCHE Claude's avatar
MARCHE Claude committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276

let project_dir =
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
          eprintf "Info: found directory '%s' for the project@." fname;
          fname
        end
      else
        begin
          eprintf "Info: found regular file '%s'@." fname;
          let d =
            try Filename.chop_extension fname
            with Invalid_argument _ -> fname
          in
          eprintf "Info: using '%s' as directory for the project@." d;
          d
        end
    end
  else
    failwith "file does not exist"

277 278 279 280 281
let goal_statistics (goals,n,m) g =
  if M.goal_proved g then (goals,n+1,m+1) else (g::goals,n,m+1)

let theory_statistics (ths,n,m) th =
  let goals,n1,m1 = List.fold_left goal_statistics ([],0,0) (M.goals th) in
282
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
283 284 285

let file_statistics (files,n,m) f =
  let ths,n1,m1 = List.fold_left theory_statistics ([],0,0) f.M.theories in
286
  ((f,ths,n1,m1)::files,n+n1,m+m1)
287 288

let print_statistics files =
MARCHE Claude's avatar
MARCHE Claude committed
289
  List.iter
290 291
    (fun (f,ths,n,m) ->
       if n<m then
292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
         begin
           printf "   +--file %s: %d/%d@." f.M.file_name n m;
           List.iter
             (fun (th,goals,n,m) ->
                if n<m then
                  begin
                    printf "      +--theory %s: %d/%d@."
                      (M.theory_name th) n m;
                    List.iter
                      (fun g ->
                         printf "         +--goal %s not proved@." (M.goal_name g))
                      (List.rev goals)
                  end)
             (List.rev ths)
         end)
307
    (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
308

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
309
(* Statistics in LaTeX*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
310

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
311 312 313 314 315 316 317 318 319 320
let rec transf_depth tr = 
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (tr.M.subgoals)
and goal_depth g =
  Hashtbl.fold 
    (fun _st tr depth -> max depth (1 + transf_depth tr)) (M.transformations g) 0
 
let theory_depth t = 
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (M.goals t)
 
let rec provers_latex_stats provers g = 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
321
  let proofs = M.external_proofs g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
322
  Hashtbl.iter (fun p a-> Hashtbl.replace provers p a.M.prover) proofs;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
323
  let tr = M.transformations g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
324 325
  Hashtbl.iter (fun _st tr -> 
    let goals = tr.M.subgoals in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
326
    List.iter (provers_latex_stats provers) goals) tr
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
327

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
328 329 330 331 332

let prover_name a = 
  match a with
      M.Detected_prover d -> d.Session.prover_name ^ " " ^ d.Session.prover_version
    | M.Undetected_prover s -> s
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
333

Asma Tafat's avatar
Asma Tafat committed
334
let rec goal_latex_stat n fmt prov depth depth_max column subgoal subgoals_max first g =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
335 336
  if(n ==1) then 
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
337 338 339 340 341 342 343 344 345
      if depth_max > 1 then 
	begin
	  if not first then
	    begin
	      if(depth < depth_max)  then
		for i = 1 to depth do fprintf fmt "&" done
	      else
		for i = 1 to depth - 1 do fprintf fmt "&" done
	    end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
346
	  else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347 348 349 350 351 352 353 354 355 356 357 358 359
	    if(depth < depth_max) then
	      if depth > 0 then fprintf fmt "&"
	end
      else
	begin
	  if not first then
	    for i = 1 to depth  do fprintf fmt "&" done
	  else
	    if depth > 0 then fprintf fmt "&"
	end
    end
  else 
    for i = 1 to depth do fprintf fmt "\\quad" done;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
360 361
  if (depth <= 1) then 
    fprintf fmt "\\verb|%s| " (M.goal_expl g);
Asma Tafat's avatar
Asma Tafat committed
362
 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
363 364 365
  let proofs = M.external_proofs g in
  if (Hashtbl.length proofs) > 0 then 
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
366 367
      if (n == 1) then 
	begin 
Asma Tafat's avatar
Asma Tafat committed
368 369 370 371 372 373 374
	  if (depth_max <= 1) then 
	    begin
	      if depth > 0 then	
		for i = depth to (depth_max - depth) do fprintf fmt "&" done
	      else 
		for i = depth to (depth_max - depth - 1) do fprintf fmt "&" done
	    end
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
375
	  else 
Asma Tafat's avatar
Asma Tafat committed
376
		for i = depth to (depth_max - depth - 1) do fprintf fmt "&" done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
377 378
	end;
      List.iter (fun (p, _pr) -> 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
379 380 381 382
	try 
	  let pr = Hashtbl.find proofs p in
	  let s = pr.M.proof_state in
	  match s with
Asma Tafat's avatar
Asma Tafat committed
383 384 385 386
	      Session.Done res -> 
		begin
		  match res.Call_provers.pr_answer with
		      Call_provers.Valid -> fprintf fmt "& %.2f " res.Call_provers.pr_time
Asma Tafat's avatar
Asma Tafat committed
387
		    | Call_provers.Invalid -> fprintf fmt "& - "
Asma Tafat's avatar
Asma Tafat committed
388 389 390 391 392
		    | Call_provers.Timeout -> fprintf fmt "& timeout "
		    | Call_provers.Unknown _s -> fprintf fmt "& ? "
		    | _ -> fprintf fmt "& "
		end
	    | _ -> fprintf fmt "& "
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
393
	with Not_found -> fprintf fmt "&") prov;
Asma Tafat's avatar
Asma Tafat committed
394 395 396 397 398 399 400 401 402
      if depth > 0 then
	begin
	  if (!subgoal < subgoals_max) then
	    fprintf fmt "\\\\ \\cline{%d-%d} @." (depth+1) column
	  else 
	    fprintf fmt "\\\\ \\cline{%d-%d} @." depth column
	end
      else 
	fprintf fmt "\\\\ \\hline @."
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
403 404 405
    end
  else begin
    let tr = M.transformations g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
406 407 408 409 410
    if (n == 2) then 
      begin 
	for i = 1 to (List.length prov) do fprintf fmt "&" done;
      fprintf fmt "\\\\ \\hline @."
      end;
Asma Tafat's avatar
Asma Tafat committed
411
    Hashtbl.iter (fun _st tr ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
412
      let goals = tr.M.subgoals in
Asma Tafat's avatar
Asma Tafat committed
413
      let subgoal = ref 0 in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
414
      let _ = List.fold_left (fun first g -> 
Asma Tafat's avatar
Asma Tafat committed
415 416
	subgoal := !subgoal + 1;
	goal_latex_stat n fmt prov (depth + 1) depth_max column (subgoal) (List.length goals) first g; false) true goals in 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
417 418 419
    () ) tr
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
420
let theory_latex_stat n dir t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
421
  let provers = Hashtbl.create 9 in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
422
  List.iter (provers_latex_stats provers) (M.goals t);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
423 424 425 426 427 428 429 430 431 432 433
  let provers = Hashtbl.fold (fun p pr acc -> (p, prover_name pr) :: acc) provers [] in 
  let provers = 
    List.sort (fun (_p1, n1) (_p2, n2) -> String.compare n1 n2) provers in 
  let depth = theory_depth  t in
  let name = M.theory_name t in 
  let ch = open_out (Filename.concat dir(name^".tex")) in 
  let fmt = formatter_of_out_channel ch in 
      fprintf fmt "\\begin{tabular}";
  fprintf fmt "{| l |";
  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
  fprintf fmt "} \n \\hline@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
434
  if (n == 1) then 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
435 436 437 438
    if (depth > 1) then 
      fprintf fmt " \\multicolumn{%d}{|c|}{Proof obligations } "  depth
      else
      fprintf fmt " \\multicolumn{%d}{|c|}{Proof obligations } " (depth + 1)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
439 440 441 442
  else 
    fprintf fmt " Proof obligations ";
  List.iter (fun (_, a) -> fprintf fmt "& %s " a) provers;
  fprintf fmt "\\\\\\hline@.";
Asma Tafat's avatar
Asma Tafat committed
443 444 445 446
  if (depth > 1) then
    List.iter (goal_latex_stat n fmt provers 0 depth ((List.length provers) + depth) (ref 0) 0 true) (M.goals t)
  else
    List.iter (goal_latex_stat n fmt provers 0 depth ((List.length provers) + depth + 1) (ref 0) 0 true) (M.goals t);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
447 448 449 450 451 452 453
  fprintf fmt "\\end{tabular}@.";
  close_out ch

let file_latex_stat n dir f =
   List.iter (theory_latex_stat n dir) f.M.theories

let print_latex_statistics n dir =
454
  let files = M.get_all_files () in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
455
  List.iter (file_latex_stat n dir) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
456

MARCHE Claude's avatar
MARCHE Claude committed
457
let print_report (g,p,r) =
458 459
  printf "   goal '%s', prover '%s': " g p;
  match r with
MARCHE Claude's avatar
MARCHE Claude committed
460
  | M.Wrong_result(new_res,old_res) ->
461
      printf "%a instead of %a@."
MARCHE Claude's avatar
MARCHE Claude committed
462
        print_result new_res print_result old_res
463 464 465 466 467 468 469 470
  | M.No_former_result ->
      printf "no former result available@."
  | M.CallFailed msg ->
      printf "internal failure '%a'@." Exn_printer.exn_printer msg;
  | M.Prover_not_installed ->
      printf "not installed@."

let () =
MARCHE Claude's avatar
MARCHE Claude committed
471 472
  try
    eprintf "Opening session...@?";
473 474 475 476 477 478
    let found_obs =
      M.open_session ~allow_obsolete:true
        ~env ~config ~init ~notify project_dir
    in
    if found_obs then
      eprintf "[Warning] session is obsolete@.";
MARCHE Claude's avatar
MARCHE Claude committed
479
    M.maximum_running_proofs :=
MARCHE Claude's avatar
MARCHE Claude committed
480 481
      Whyconf.running_provers_max (Whyconf.get_main config);
    eprintf " done@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
482 483 484 485 486 487 488 489
    if !opt_latex <> "" then print_latex_statistics 1 !opt_latex
    else 
    if !opt_latex2 <> "" then print_latex_statistics 2 !opt_latex2
    else 
      let callback report =
	let files,n,m =
          List.fold_left file_statistics ([],0,0) (M.get_all_files ())
	in
490
      match report with
491
        | [] ->
492 493 494 495
            if found_obs then
              if n=m then
                printf " %d/%d (replay OK, all proved: obsolete session updated)@." n m
              else
496 497 498 499
                if !opt_force then
                  printf " %d/%d (replay OK, but not all proved: obsolete session updated since -force was given)@." n m
                else
                  printf " %d/%d (replay OK, but not all proved: obsolete session NOT updated)@." n m
500 501
            else
              printf " %d/%d@." n m ;
502
            if !opt_stats && n<m then print_statistics files;
503
            eprintf "Everything replayed OK.@.";
MARCHE Claude's avatar
MARCHE Claude committed
504
            if found_obs && (n=m || !opt_force) then
505 506 507 508 509
              begin
                eprintf "Updating obsolete session...@?";
                M.save_session ();
                eprintf " done@."
              end;
510 511
            exit 0
        | _ ->
512
            printf " %d/%d (replay failed)@." n m ;
513
            List.iter print_report report;
514
            eprintf "Replay failed.@.";
515
            exit 1
516 517
    in
    M.check_all ~callback;
518
    try main_loop ()
519
    with Exit -> eprintf "main replayer exited unexpectedly@."
520 521
  with
    | M.OutdatedSession ->
522
        eprintf "The session database '%s' is outdated, cannot replay@."
523 524 525 526
          project_dir;
        eprintf "Aborting...@.";
        exit 1
    | e when not (Debug.test_flag Debug.stack_trace) ->
527
        eprintf "Error while opening session with database '%s' : %a@."
528 529 530 531
          project_dir
          Exn_printer.exn_printer e;
        eprintf "Aborting...@.";
        exit 1
MARCHE Claude's avatar
MARCHE Claude committed
532 533


534 535 536 537 538
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)