replay.ml 15.2 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 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
     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"

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

open Format

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

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

MARCHE Claude's avatar
MARCHE Claude committed
198
(*
MARCHE Claude's avatar
MARCHE Claude committed
199
let string_of_result result =
MARCHE Claude's avatar
MARCHE Claude committed
200 201 202 203 204 205
  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
206 207 208 209 210 211
        | 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
212

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

MARCHE Claude's avatar
MARCHE Claude committed
222

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

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

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"

275 276 277 278 279
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
280
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
281 282 283

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

let print_statistics files =
MARCHE Claude's avatar
MARCHE Claude committed
287
  List.iter
288 289
    (fun (f,ths,n,m) ->
       if n<m then
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304
         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)
305
    (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
306

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
307
(* Statistics in LaTeX*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
308

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
309 310 311 312 313 314 315 316 317 318
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
319
  let proofs = M.external_proofs g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
320
  Hashtbl.iter (fun p a-> Hashtbl.replace provers p a.M.prover) proofs;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
321
  let tr = M.transformations g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
322 323
  Hashtbl.iter (fun _st tr -> 
    let goals = tr.M.subgoals in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
324
    List.iter (provers_latex_stats provers) goals) tr
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
325

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
326 327 328 329 330

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
331

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
332
let rec goal_latex_stat n fmt prov depth depth_max first g =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
333 334
  if(n ==1) then 
    begin
Asma Tafat's avatar
Asma Tafat committed
335
    if not first then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
336 337 338 339 340 341
      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's avatar
Asma Tafat committed
342
    else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
343 344
       if(depth < depth_max) then
	if depth > 0 then fprintf fmt "&"
Asma Tafat's avatar
Asma Tafat committed
345
  end;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
346 347
  if (depth <= 1) then 
    fprintf fmt "\\verb|%s| " (M.goal_expl g);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
348 349 350
  let proofs = M.external_proofs g in
  if (Hashtbl.length proofs) > 0 then 
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
351 352
      if (n == 1) then 
	begin 
Asma Tafat's avatar
Asma Tafat committed
353 354 355 356 357 358 359
	  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
360
	  else 
Asma Tafat's avatar
Asma Tafat committed
361
		for i = depth to (depth_max - depth - 1) do fprintf fmt "&" done
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
362 363
	end;
      List.iter (fun (p, _pr) -> 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
364 365 366 367
	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
368 369 370 371 372 373 374 375 376 377
	      Session.Done res -> 
		begin
		  match res.Call_provers.pr_answer with
		      Call_provers.Valid -> fprintf fmt "& %.2f " res.Call_provers.pr_time
		    | Call_provers.Invalid -> fprintf fmt "& _ "
		    | 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
378 379
	with Not_found -> fprintf fmt "&") prov;
      fprintf fmt "\\\\ \\hline @.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
380 381 382
    end
  else begin
    let tr = M.transformations g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
383 384 385 386 387
    if (n == 2) then 
      begin 
	for i = 1 to (List.length prov) do fprintf fmt "&" done;
      fprintf fmt "\\\\ \\hline @."
      end;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
388 389 390
    Hashtbl.iter (fun _st tr -> 
      let goals = tr.M.subgoals in
      let _ = List.fold_left (fun first g -> 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
391
	goal_latex_stat n fmt prov (depth + 1) depth_max first g; false) true  goals in 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
392 393 394
    () ) tr
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
395
let theory_latex_stat n dir t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
396
  let provers = Hashtbl.create 9 in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
397
  List.iter (provers_latex_stats provers) (M.goals t);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
398 399 400 401 402 403 404 405 406 407 408
  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
409
  if (n == 1) then 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
410 411 412 413
    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
414 415 416 417 418 419 420 421 422 423 424 425
  else 
    fprintf fmt " Proof obligations ";
  List.iter (fun (_, a) -> fprintf fmt "& %s " a) provers;
  fprintf fmt "\\\\\\hline@.";
  List.iter (goal_latex_stat n fmt provers 0 depth true) (M.goals t);
  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 =
426
  let files = M.get_all_files () in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
427
  List.iter (file_latex_stat n dir) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
428

MARCHE Claude's avatar
MARCHE Claude committed
429
let print_report (g,p,r) =
430 431
  printf "   goal '%s', prover '%s': " g p;
  match r with
MARCHE Claude's avatar
MARCHE Claude committed
432
  | M.Wrong_result(new_res,old_res) ->
433
      printf "%a instead of %a@."
MARCHE Claude's avatar
MARCHE Claude committed
434
        print_result new_res print_result old_res
435 436 437 438 439 440 441 442
  | 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
443 444
  try
    eprintf "Opening session...@?";
445 446 447 448 449 450
    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
451
    M.maximum_running_proofs :=
MARCHE Claude's avatar
MARCHE Claude committed
452 453
      Whyconf.running_provers_max (Whyconf.get_main config);
    eprintf " done@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
454 455 456 457 458 459 460 461
    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
462
      match report with
463
        | [] ->
464 465 466 467
            if found_obs then
              if n=m then
                printf " %d/%d (replay OK, all proved: obsolete session updated)@." n m
              else
468 469 470 471
                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
472 473
            else
              printf " %d/%d@." n m ;
474
            if !opt_stats && n<m then print_statistics files;
475
            eprintf "Everything replayed OK.@.";
MARCHE Claude's avatar
MARCHE Claude committed
476
            if found_obs && (n=m || !opt_force) then
477 478 479 480 481
              begin
                eprintf "Updating obsolete session...@?";
                M.save_session ();
                eprintf " done@."
              end;
482 483
            exit 0
        | _ ->
484
            printf " %d/%d (replay failed)@." n m ;
485
            List.iter print_report report;
486
            eprintf "Replay failed.@.";
487
            exit 1
488 489
    in
    M.check_all ~callback;
490
    try main_loop ()
491
    with Exit -> eprintf "main replayer exited unexpectedly@."
492 493
  with
    | M.OutdatedSession ->
494
        eprintf "The session database '%s' is outdated, cannot replay@."
495 496 497 498
          project_dir;
        eprintf "Aborting...@.";
        exit 1
    | e when not (Debug.test_flag Debug.stack_trace) ->
499
        eprintf "Error while opening session with database '%s' : %a@."
500 501 502 503
          project_dir
          Exn_printer.exn_printer e;
        eprintf "Aborting...@.";
        exit 1
MARCHE Claude's avatar
MARCHE Claude committed
504 505


506 507 508 509 510
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)