replay.ml 21 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 ""
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
30
let opt_longtable = ref false
Asma Tafat's avatar
Asma Tafat committed
31
let opt_html = ref ""
32
let opt_force = ref false
33 34 35 36 37 38 39
let opt_smoke = ref Session.SD_None

let set_opt_smoke = function
  | "none" -> opt_smoke := Session.SD_None
  | "top" ->  opt_smoke := Session.SD_Top
  | "deep" ->  opt_smoke := Session.SD_Deep
  | _ -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
40 41 42 43 44

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
45 46
  ("-force",
   Arg.Set opt_force,
Asma Tafat's avatar
Asma Tafat committed
47
   " enforce saving of session even if replay failed") ;
48 49 50
  ("-smoke-detector",
   Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
   " try to detect if the context is self-contradicting") ;
51 52 53
  ("-s",
   Arg.Clear opt_stats,
   " do not print statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
  ("-v",
   Arg.Set opt_version,
   " print version information") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
57
  ("-latex",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
58
   Arg.Set_string opt_latex,
Asma Tafat's avatar
Asma Tafat committed
59
   " [Dir_output] produce latex statistics") ;
Asma Tafat's avatar
Asma Tafat committed
60
  ("-latex2",
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
61
   Arg.Set_string opt_latex2,
Asma Tafat's avatar
Asma Tafat committed
62
   " [Dir_output] produce latex statistics") ;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
63 64 65
  ("-longtable",
   Arg.Set opt_longtable,
   " produce latex statistics using longtable package") ;
Asma Tafat's avatar
Asma Tafat committed
66 67
  ("-html",
   Arg.Set_string opt_html,
Asma Tafat's avatar
Asma Tafat committed
68
   " [Dir_output] produce html statistics") ;
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
]

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

92 93 94 95 96 97
let () =
  if !opt_smoke <> Session.SD_None && !opt_force then begin
    Format.printf "You can't force when detecting smoke@.";
    exit 1
  end

MARCHE Claude's avatar
MARCHE Claude committed
98 99 100 101 102 103 104 105 106 107
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
108
  @ List.rev !includes
MARCHE Claude's avatar
MARCHE Claude committed
109

110
let env = Env.create_env loadpath
MARCHE Claude's avatar
MARCHE Claude committed
111

Andrei Paskevich's avatar
Andrei Paskevich committed
112 113
let () = Whyconf.load_plugins (Whyconf.get_main config)

MARCHE Claude's avatar
MARCHE Claude committed
114 115 116 117 118 119 120 121 122 123
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
124
     let create ?parent () =
MARCHE Claude's avatar
MARCHE Claude committed
125 126 127 128 129 130
       match parent with
         | None -> 0
         | Some  n -> n+1

     let remove _row = ()

MARCHE Claude's avatar
MARCHE Claude committed
131 132
     let reset () = ()

MARCHE Claude's avatar
MARCHE Claude committed
133 134 135 136 137 138 139 140 141 142
     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"

143
     let notify_timer_state w s r =
MARCHE Claude's avatar
MARCHE Claude committed
144
       Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
145

MARCHE Claude's avatar
MARCHE Claude committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
   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
172 173 174
        | None ->
            begin
              let ms =
MARCHE Claude's avatar
MARCHE Claude committed
175
                match !timeout_handler with
176
                  | None -> 100.0 (* raise Exit *)
MARCHE Claude's avatar
MARCHE Claude committed
177 178 179 180
                  | Some(ms,_) -> ms
              in
              usleep (ms -. time)
            end
MARCHE Claude's avatar
MARCHE Claude committed
181
        | Some f ->
MARCHE Claude's avatar
MARCHE Claude committed
182 183 184 185 186 187 188 189 190
            let b = f () in
            if b then () else
              begin
                idle_handler := None;
              end
  done

open Format

191
(*
MARCHE Claude's avatar
MARCHE Claude committed
192
let model_index = Hashtbl.create 257
193
*)
MARCHE Claude's avatar
MARCHE Claude committed
194

MARCHE Claude's avatar
MARCHE Claude committed
195
let init =
196
(*
MARCHE Claude's avatar
MARCHE Claude committed
197
  let cpt = ref 0 in
198
*)
MARCHE Claude's avatar
MARCHE Claude committed
199
  fun _row any ->
200
(*
MARCHE Claude's avatar
MARCHE Claude committed
201 202
    incr cpt;
    Hashtbl.add model_index !cpt any;
203
*)
204
    let _name =
MARCHE Claude's avatar
MARCHE Claude committed
205 206 207 208
      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
209
        | M.Proof_attempt a ->
210 211 212
            begin
              match a.M.prover with
                | M.Detected_prover p ->
213
                    p.Session.prover_name ^ " " ^ p.Session.prover_version
214 215
                | M.Undetected_prover s -> s
            end
MARCHE Claude's avatar
MARCHE Claude committed
216 217
        | M.Transformation tr -> Session.transformation_id tr.M.transf
    in
MARCHE Claude's avatar
MARCHE Claude committed
218 219
    (* eprintf "Item '%s' loaded@." name *)
    ()
MARCHE Claude's avatar
MARCHE Claude committed
220

MARCHE Claude's avatar
MARCHE Claude committed
221
(*
MARCHE Claude's avatar
MARCHE Claude committed
222
let string_of_result result =
MARCHE Claude's avatar
MARCHE Claude committed
223 224 225 226 227 228
  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
229 230 231 232 233 234
        | 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
235

MARCHE Claude's avatar
MARCHE Claude committed
236
let print_result fmt res =
MARCHE Claude's avatar
MARCHE Claude committed
237 238
  let t = match res with
    | Session.Done { Call_provers.pr_time = time } ->
239
        Format.sprintf "(%.1f)" time
MARCHE Claude's avatar
MARCHE Claude committed
240 241 242
    | _ -> ""
  in
  fprintf fmt "%s%s" (string_of_result res) t
MARCHE Claude's avatar
MARCHE Claude committed
243 244
*)

MARCHE Claude's avatar
MARCHE Claude committed
245

MARCHE Claude's avatar
MARCHE Claude committed
246 247
let print_result fmt
    {Call_provers.pr_answer=ans; Call_provers.pr_output=out;
248 249
     Call_provers.pr_time=t} =
(**)
MARCHE Claude's avatar
MARCHE Claude committed
250
  fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
251 252
(**)
(*
253
  fprintf fmt "%a" Call_provers.print_prover_answer ans;
254
*)
MARCHE Claude's avatar
MARCHE Claude committed
255 256
  if ans == Call_provers.HighFailure then
    fprintf fmt "@\nProver output:@\n%s@." out
MARCHE Claude's avatar
MARCHE Claude committed
257

258 259
let notify _any = ()
(*
MARCHE Claude's avatar
MARCHE Claude committed
260 261
  match any with
    | M.Goal g ->
262
        printf "Goal '%s' proved: %b@." (M.goal_expl g) (M.goal_proved g)
MARCHE Claude's avatar
MARCHE Claude committed
263
    | M.Theory th ->
264
        printf "Theory '%s' verified: %b@." (M.theory_name th) (M.verified th)
MARCHE Claude's avatar
MARCHE Claude committed
265
    | M.File file ->
266
        printf "File '%s' verified: %b@." (Filename.basename file.M.file_name)
MARCHE Claude's avatar
MARCHE Claude committed
267 268 269
          file.M.file_verified
    | M.Proof_attempt a ->
        let p = a.M.prover in
270 271
        printf "Proof with '%s %s' gives %a@."
          p.Session.prover_name p.Session.prover_version
MARCHE Claude's avatar
MARCHE Claude committed
272 273
          print_result a.M.proof_state
    | M.Transformation tr ->
274
        printf "Transformation '%s' proved: %b@."
MARCHE Claude's avatar
MARCHE Claude committed
275
          (Session.transformation_id tr.M.transf) tr.M.transf_proved
276
*)
MARCHE Claude's avatar
MARCHE Claude committed
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299

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"

300 301 302 303 304
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
305
  ((th,goals,n1,m1)::ths,n+n1,m+m1)
306 307 308

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

let print_statistics files =
François Bobot's avatar
François Bobot committed
312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
  let print_goal g =
      printf "         +--goal %s not proved@." (M.goal_name g)
  in
  let print_theory (th,goals,n,m) =
    if n<m then begin
      printf "      +--theory %s: %d/%d@." (M.theory_name th) n m;
      List.iter print_goal (List.rev goals)
    end
  in
  let print_file (f,ths,n,m) =
    if n<m then begin
      printf "   +--file %s: %d/%d@." f.M.file_name n m;
      List.iter print_theory (List.rev ths)
    end
  in
  List.iter print_file (List.rev files)
MARCHE Claude's avatar
MARCHE Claude committed
328

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
329
(* Statistics in LaTeX*)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
330

Asma Tafat's avatar
Asma Tafat committed
331
let rec transf_depth tr =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
332 333
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (tr.M.subgoals)
and goal_depth g =
Asma Tafat's avatar
Asma Tafat committed
334
  Hashtbl.fold
François Bobot's avatar
François Bobot committed
335 336
    (fun _st tr depth -> max depth (1 + transf_depth tr))
    (M.transformations g) 0
Asma Tafat's avatar
Asma Tafat committed
337 338

let theory_depth t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
339
  List.fold_left (fun depth g -> max depth (goal_depth g)) 0 (M.goals t)
Asma Tafat's avatar
Asma Tafat committed
340 341

let rec provers_latex_stats provers g =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
342
  let proofs = M.external_proofs g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
343
  Hashtbl.iter (fun p a-> Hashtbl.replace provers p a.M.prover) proofs;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
344
  let tr = M.transformations g in
Asma Tafat's avatar
Asma Tafat committed
345
  Hashtbl.iter (fun _st tr ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
346
    let goals = tr.M.subgoals in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347
    List.iter (provers_latex_stats provers) goals) tr
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
348

Asma Tafat's avatar
Asma Tafat committed
349
let prover_name a =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
350
  match a with
François Bobot's avatar
François Bobot committed
351 352
      M.Detected_prover d ->
        d.Session.prover_name ^ " " ^ d.Session.prover_version
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
353
    | M.Undetected_prover s -> s
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
354

Asma Tafat's avatar
Asma Tafat committed
355 356 357 358
let protect s =
  let b = Buffer.create 7 in
  for i = 0 to String.length s - 1 do
    match s.[i] with
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
359 360 361 362 363
	'_' -> Buffer.add_string b "\\_"
      | c -> Buffer.add_char b c
  done;
  Buffer.contents b

Asma Tafat's avatar
Asma Tafat committed
364 365

let column n depth provers =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
366
  if n == 1 then
Asma Tafat's avatar
Asma Tafat committed
367 368 369 370
    if depth > 1 then
      (List.length provers) + depth
    else
      (List.length provers) + depth + 1
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
371
  else
Asma Tafat's avatar
Asma Tafat committed
372 373 374
    (List.length provers) +  1


Asma Tafat's avatar
Asma Tafat committed
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
let print_result_prov proofs prov fmt=
  List.iter (fun (p, _pr) ->
  try
    let pr = Hashtbl.find proofs p in
    let s = pr.M.proof_state in
      match s with
	  Session.Done res ->
	    begin
	      match res.Call_provers.pr_answer with
		  Call_provers.Valid ->
                    fprintf fmt "& \\valid{%.2f} " res.Call_provers.pr_time
		| Call_provers.Invalid -> fprintf fmt "& \\invalid "
		| Call_provers.Timeout -> fprintf fmt "& \\timeout "
		| Call_provers.Unknown _s -> fprintf fmt "& \\unknown "
		| _ -> fprintf fmt "& \\failure "
	    end
	| _ -> fprintf fmt "& Undone"
  with Not_found -> fprintf fmt "& \\noresult") prov;
  fprintf fmt "\\\\ @."


Asma Tafat's avatar
Asma Tafat committed
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410
let rec goal_latex_stat fmt prov depth depth_max subgoal g =
  let column = column 1 depth prov
  in
    if depth > 0 then
      if subgoal > 0 then
	fprintf fmt "\\cline{%d-%d} @." (depth + 1) column
      else ()
    else
      fprintf fmt "\\hline @.";
    if depth_max > 1 then
      begin
	if subgoal > 0 then
	  begin
	    if(depth < depth_max)  then
	      for i = 1 to depth do
François Bobot's avatar
François Bobot committed
411
                fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat's avatar
Asma Tafat committed
412 413 414 415 416 417 418 419
              done
	    else
	      for i = 1 to depth - 1 do
                fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
              done
	  end
	else
	  if(depth < depth_max) then
François Bobot's avatar
François Bobot committed
420 421
	    if depth > 0 then
              fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
Asma Tafat's avatar
Asma Tafat committed
422 423 424 425 426 427 428 429 430 431 432 433
      end
    else
      begin
	if subgoal > 0  then
	  for i = 1 to depth  do
	    fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " " done
	else
	  if depth > 0 then
	    fprintf fmt "\\explanation{%s}& \\explanation{%s}" " " " "
      end;
    if (depth <= 1) then
      fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
Asma Tafat's avatar
Asma Tafat committed
434 435
    else
      fprintf fmt "\\explanation{%s}"  " ";
Asma Tafat's avatar
Asma Tafat committed
436 437
    let proofs = M.external_proofs g in
      if (Hashtbl.length proofs) > 0 then
Asma Tafat's avatar
Asma Tafat committed
438 439 440 441 442 443 444 445 446 447 448
	begin
	  if depth_max <= 1 then
	    begin
	      if depth > 0 then
		for i = depth to (depth_max - depth) do
                  fprintf fmt "& \\explanation{%s}" " " done
	      else
		for i = depth to (depth_max - depth - 1) do
                  fprintf fmt "& \\explanation{%s}" " " done
	    end
	  else
Asma Tafat's avatar
Asma Tafat committed
449 450
	    if depth > 0 then
	      for i = depth to (depth_max - depth - 1) do
Asma Tafat's avatar
Asma Tafat committed
451 452 453 454 455
		fprintf fmt "& \\explanation{%s}" " " done
	    else
	      for i = depth to (depth_max - depth - 2) do
		fprintf fmt "& \\explanation{%s}" " " done;
	  print_result_prov proofs prov fmt;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
456
	end;
Asma Tafat's avatar
Asma Tafat committed
457 458
      let tr = M.transformations g in
	if Hashtbl.length tr > 0 then
Asma Tafat's avatar
Asma Tafat committed
459 460 461 462 463 464 465 466
	  if Hashtbl.length proofs > 0 then
	    fprintf fmt "\\cline{%d-%d} @." (depth + 2) column;
	Hashtbl.iter (fun _st tr ->
          let goals = tr.M.subgoals in
	  let _ = List.fold_left (fun subgoal g ->
              goal_latex_stat fmt prov (depth + 1) depth_max (subgoal) g;
               subgoal + 1) 0 goals in
	    () ) tr
Asma Tafat's avatar
Asma Tafat committed
467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482


let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
  let column = column 2 depth prov
  in
    if depth > 0 then
      fprintf fmt "\\cline{%d-%d} @." 2 column
    else
      fprintf fmt "\\hline @.";
    for i = 1 to depth do fprintf fmt "\\quad" done;
    if (depth <= 1) then
      fprintf fmt "\\explanation{%s} " (protect (M.goal_expl g))
    else
      fprintf fmt "\\explanation{%d} " (subgoal + 1);
    let proofs = M.external_proofs g in
      if (Hashtbl.length proofs) > 0 then
Asma Tafat's avatar
Asma Tafat committed
483
	print_result_prov proofs prov fmt;
Asma Tafat's avatar
Asma Tafat committed
484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508
      let tr = M.transformations g in
	if Hashtbl.length tr > 0 then
	  begin
	    if (Hashtbl.length proofs == 0) then
	      fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @." (List.length prov);
	    Hashtbl.iter (fun _st tr ->
		let goals = tr.M.subgoals in
		let _ = List.fold_left (fun subgoal g ->
				goal_latex2_stat fmt prov (depth + 1) depth_max (subgoal) g;
				subgoal + 1) 0 goals in
		  () ) tr
	  end
	else
	  if (Hashtbl.length proofs) == 0 then
	    fprintf fmt "\\\\ @."


let print_head n depth provers fmt =
  if n == 1 then
    if (depth > 1) then
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        depth
    else
      fprintf fmt "\\hline \\multicolumn{%d}{|c|}{Proof obligations } "
        (depth + 1)
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
509
  else
Asma Tafat's avatar
Asma Tafat committed
510 511 512
    fprintf fmt "\\hline Proof obligations ";
  List.iter (fun (_, a) -> fprintf fmt "& \\provername{%s} " a) provers;
  fprintf fmt "\\\\ @."
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
513

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
514

Asma Tafat's avatar
Asma Tafat committed
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
let latex_tabular n fmt depth provers t =
fprintf fmt "\\begin{tabular}";
fprintf fmt "{| l |";
  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
  fprintf fmt "}@.";
  print_head n depth provers fmt;
  if n == 1 then
    List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t)
  else
    List.iter (goal_latex2_stat fmt provers 0 depth  0) (M.goals t);
  fprintf fmt "\\hline \\end{tabular}@."


let latex_longtable n fmt depth name provers t=
  fprintf fmt "\\begin{longtable}";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
530 531
  fprintf fmt "{| l |";
  for i = 0 to (List.length provers) + depth do fprintf fmt "c |" done;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
532
  fprintf fmt "}@.";
533
  (** First head *)
Asma Tafat's avatar
Asma Tafat committed
534
  print_head n depth provers fmt;
Asma Tafat's avatar
Asma Tafat committed
535
  fprintf fmt "\\hline \\endfirsthead @.";
536
  (** Other heads : "Continued... " added *)
François Bobot's avatar
François Bobot committed
537 538
  fprintf fmt "\\multicolumn{%d}{r}{\\textit{Continued from previous page}} \
\\\\ @." (List.length provers + 1) ;
Asma Tafat's avatar
Asma Tafat committed
539
  fprintf fmt "\\hline @.";
Asma Tafat's avatar
Asma Tafat committed
540
  print_head n depth provers fmt;
Asma Tafat's avatar
Asma Tafat committed
541
  fprintf fmt "\\hline \\endhead @.";
542
  (** Other foots : "Continued..." added *)
François Bobot's avatar
François Bobot committed
543 544
  fprintf fmt "\\hline \\multicolumn{%d}{r}{\\textit{Continued on next page}} \
\\\\ @." (List.length provers);
545
  (** Last foot : nothing *)
Asma Tafat's avatar
Asma Tafat committed
546
  fprintf fmt "\\endfoot \\endlastfoot @.";
Asma Tafat's avatar
Asma Tafat committed
547 548 549 550 551 552
  if n == 1 then
    List.iter (goal_latex_stat fmt provers 0 depth 0) (M.goals t)
  else
    List.iter (goal_latex2_stat fmt provers 0 depth  0) (M.goals t);
  fprintf fmt "\\hline \\caption{%s statistics} @." (protect name);
  fprintf fmt "\\label{%s} \\end{longtable}@." (protect name)
Asma Tafat's avatar
Asma Tafat committed
553

Asma Tafat's avatar
Asma Tafat committed
554 555 556 557 558 559 560 561 562 563 564 565 566

let theory_latex_stat n table dir t =
  let provers = Hashtbl.create 9 in
  List.iter (provers_latex_stats provers) (M.goals t);
  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
    if table = "tabular" then
Asma Tafat's avatar
Asma Tafat committed
567
      begin
Asma Tafat's avatar
Asma Tafat committed
568
      latex_tabular n fmt depth provers t
Asma Tafat's avatar
Asma Tafat committed
569
      end
Asma Tafat's avatar
Asma Tafat committed
570
    else
Asma Tafat's avatar
Asma Tafat committed
571 572
      latex_longtable n fmt depth name provers t;
    close_out ch
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
573

Asma Tafat's avatar
Asma Tafat committed
574 575
let file_latex_stat n table  dir f =
   List.iter (theory_latex_stat n table dir) f.M.theories
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
576

Asma Tafat's avatar
Asma Tafat committed
577
let print_latex_statistics n table dir =
578
  let files = M.get_all_files () in
Asma Tafat's avatar
Asma Tafat committed
579
  List.iter (file_latex_stat n table dir) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
580

MARCHE Claude's avatar
MARCHE Claude committed
581
let print_report (g,p,r) =
582 583
  printf "   goal '%s', prover '%s': " g p;
  match r with
MARCHE Claude's avatar
MARCHE Claude committed
584
  | M.Wrong_result(new_res,old_res) ->
585 586 587 588 589 590 591
    begin match !opt_smoke with
      | Session.SD_None ->
        printf "%a instead of %a@."
          print_result new_res print_result old_res
      | _ ->
        printf "Smoke detected!!!@."
    end
592 593 594 595 596 597 598
  | 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@."

599
let add_to_check_no_smoke found_obs =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
600
      let callback report =
601
        eprintf "@.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
602 603 604
	let files,n,m =
          List.fold_left file_statistics ([],0,0) (M.get_all_files ())
	in
605
      match report with
606
        | [] ->
607 608
            if found_obs then
              if n=m then
François Bobot's avatar
François Bobot committed
609 610
                printf " %d/%d (replay OK, all proved: obsolete session \
updated)@." n m
611
              else
612
                if !opt_force then
François Bobot's avatar
François Bobot committed
613 614
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session updated since -force was given)@." n m
615
                else
François Bobot's avatar
François Bobot committed
616 617
                  printf " %d/%d (replay OK, but not all proved: obsolete \
session NOT updated)@." n m
618 619
            else
              printf " %d/%d@." n m ;
620
            if !opt_stats && n<m then print_statistics files;
621
            eprintf "Everything replayed OK.@.";
MARCHE Claude's avatar
MARCHE Claude committed
622
            if found_obs && (n=m || !opt_force) then
623 624 625 626 627
              begin
                eprintf "Updating obsolete session...@?";
                M.save_session ();
                eprintf " done@."
              end;
628 629
            exit 0
        | _ ->
630
            printf " %d/%d (replay failed)@." n m ;
631
            List.iter print_report report;
632
            eprintf "Replay failed.@.";
633
            exit 1
634
    in
635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674
    M.check_all ~callback

let add_to_check_smoke () =
  let callback report =
    eprintf "@.";
    match report with
      | [] ->
        eprintf "No smoke detected.@.";
        exit 0
      | _ ->
        List.iter print_report report;
        eprintf "Smoke detected.@.";
        exit 1
  in
  M.check_all ~callback

let add_to_check found_obs =
  match !opt_smoke with
    | Session.SD_None -> add_to_check_no_smoke found_obs;
    | _ -> assert (not found_obs); add_to_check_smoke ()


let () =
  try
    eprintf "Opening session...@?";
    let found_obs =
      M.open_session ~allow_obsolete:true
        ~env ~config ~init ~notify project_dir
    in
    if found_obs then begin
      if !opt_smoke <> Session.SD_None then begin
        eprintf
          "[Error] I can't run the smoke detector if the session is obsolete";
        exit 1
      end;
      eprintf "[Warning] session is obsolete@.";
    end;
    M.maximum_running_proofs :=
      Whyconf.running_provers_max (Whyconf.get_main config);
    M.smoke_detector := !opt_smoke;
Asma Tafat's avatar
Asma Tafat committed
675 676
    eprintf " done.";
    if !opt_longtable && !opt_latex == "" && !opt_latex2 == "" then
677
      begin
Asma Tafat's avatar
Asma Tafat committed
678 679 680
	eprintf
	  "[Error] I can't use option longtable without latex ou latex2@.";
	exit 1
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
681
      end;
Asma Tafat's avatar
Asma Tafat committed
682 683 684 685 686
    if !opt_latex <> "" then
      if !opt_longtable then
	print_latex_statistics 1 "longtable" !opt_latex
      else
	print_latex_statistics 1 "tabular" !opt_latex
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
687
    else
Asma Tafat's avatar
Asma Tafat committed
688 689 690 691
      if !opt_latex2 <> "" then
	if !opt_longtable then
	  print_latex_statistics 2 "longtable" !opt_latex2
	else
Asma Tafat's avatar
Asma Tafat committed
692
	  print_latex_statistics 2 "tabular" !opt_latex2
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
693 694 695 696 697 698
      else
	begin
          add_to_check found_obs;
          try main_loop ()
          with Exit -> eprintf "main replayer exited unexpectedly@."
	end
699 700
  with
    | M.OutdatedSession ->
701
        eprintf "The session database '%s' is outdated, cannot replay@."
702 703 704 705
          project_dir;
        eprintf "Aborting...@.";
        exit 1
    | e when not (Debug.test_flag Debug.stack_trace) ->
706
        eprintf "Error while opening session with database '%s' : %a@."
707 708 709 710
          project_dir
          Exn_printer.exn_printer e;
        eprintf "Aborting...@.";
        exit 1
MARCHE Claude's avatar
MARCHE Claude committed
711 712


713 714 715 716 717
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)