replay.ml 14.8 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's avatar
Asma Tafat committed
333 334
  if(n ==1) then begin
    if not first then
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
335
      for i = 1 to depth do fprintf fmt "&" done
Asma Tafat's avatar
Asma Tafat committed
336
    else
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
337
      if depth > 0 then fprintf fmt "&"
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
338
  end
Asma Tafat's avatar
Asma Tafat committed
339
  else begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
340
    for i = 1 to depth do fprintf fmt "\\quad" done
Asma Tafat's avatar
Asma Tafat committed
341
  end;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
342 343
  if (depth <= 1) then 
    fprintf fmt "\\verb|%s| " (M.goal_expl g);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
344 345 346
  let proofs = M.external_proofs g in
  if (Hashtbl.length proofs) > 0 then 
    begin
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
347 348
      if (n == 1) then 
	begin 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
349 350 351 352
	  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;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
353 354
	end;
      List.iter (fun (p, _pr) -> 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
355 356 357 358 359 360
	try 
	  let pr = Hashtbl.find proofs p in
	  let s = pr.M.proof_state in
	  match s with
	      Session.Done res ->
		if res.Call_provers.pr_answer = Call_provers.Valid
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
361 362 363 364 365
		then  fprintf fmt "& %.2f " res.Call_provers.pr_time
		else fprintf fmt "& - "
	    | _ -> fprintf fmt "& " 
	with Not_found -> fprintf fmt "&") prov;
      fprintf fmt "\\\\ \\hline @.";
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
366 367 368
    end
  else begin
    let tr = M.transformations g in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
369 370 371 372 373
    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
374 375 376
    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
377
	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
378 379 380
    () ) tr
  end

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
381
let theory_latex_stat n dir t =
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
382
  let provers = Hashtbl.create 9 in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
383
  List.iter (provers_latex_stats provers) (M.goals t);
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
384 385 386 387 388 389 390 391 392 393 394
  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
395
  if (n == 1) then 
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
396 397 398 399
    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
400 401 402 403 404 405 406 407 408 409 410 411
  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 =
412
  let files = M.get_all_files () in
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
413
  List.iter (file_latex_stat n dir) files
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
414

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


492 493 494 495 496
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
End:
*)