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

20
open Format
21
open Why3
22 23
open Util
open Whyconf
24
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
25
open Task
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
open Driver
27
open Trans
28

29 30
let usage_msg = sprintf
  "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
31
  (Filename.basename Sys.argv.(0))
32

33 34 35
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
  Config.version Config.builddate

36
let opt_queue = Queue.create ()
37

38 39
let opt_input = ref None
let opt_theory = ref None
40
let opt_trans = ref []
41
let opt_metas = ref []
42

43 44
let add_opt_file x =
  let tlist = Queue.create () in
45
  Queue.push (Some x, tlist) opt_queue;
46
  opt_input := Some tlist
47

48 49 50
let add_opt_theory =
  let rdot = (Str.regexp "\\.") in fun x ->
  let l = Str.split rdot x in
51 52 53 54 55 56
  let p, t = match List.rev l with
    | t::p -> List.rev p, t
    | _ -> assert false
  in
  match !opt_input, p with
  | None, [] ->
57
      eprintf "Option '-T'/'--theory' with a non-qualified \
58 59 60 61
        argument requires an input file.@.";
      exit 1
  | Some tlist, [] ->
      let glist = Queue.create () in
62
      Queue.push (x, p, t, glist) tlist;
63 64 65
      opt_theory := Some glist
  | _ ->
      let tlist = Queue.create () in
66
      Queue.push (None, tlist) opt_queue;
67 68
      opt_input := None;
      let glist = Queue.create () in
69
      Queue.push (x, p, t, glist) tlist;
70 71 72 73
      opt_theory := Some glist

let add_opt_goal x = match !opt_theory with
  | None ->
74
      eprintf "Option '-G'/'--goal' requires a theory.@.";
75 76 77
      exit 1
  | Some glist ->
      let l = Str.split (Str.regexp "\\.") x in
78
      Queue.push (x, l) glist
79 80

let add_opt_trans x = opt_trans := x::!opt_trans
81

82
let add_opt_meta meta =
83
  let meta_name, meta_arg =
84 85 86
    let index = String.index meta '=' in
    (String.sub meta 0 index),
    (String.sub meta (index+1) (String.length meta - (index + 1))) in
87 88
  opt_metas := (meta_name,meta_arg)::!opt_metas

89
let opt_config = ref None
90
let opt_parser = ref None
91
let opt_prover = ref None
92
let opt_loadpath = ref []
93 94
let opt_driver = ref None
let opt_output = ref None
95 96
let opt_timelimit = ref None
let opt_memlimit = ref None
97
let opt_command = ref None
98
let opt_task = ref None
99
let opt_realize = ref false
100
let opt_bisect = ref false
101

102 103 104
let opt_print_libdir = ref false
let opt_print_datadir = ref false

105 106 107 108
let opt_print_theory = ref false
let opt_print_namespace = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
109
let opt_list_provers = ref false
110
let opt_list_formats = ref false
111
let opt_list_metas = ref false
112

113
let opt_token_count = ref false
114 115
let opt_parse_only = ref false
let opt_type_only = ref false
116
let opt_version = ref false
117 118 119 120

let option_list = Arg.align [
  "-", Arg.Unit (fun () -> add_opt_file "-"),
      " Read the input file from stdin";
121
  "-T", Arg.String add_opt_theory,
122 123
      "<theory> Select <theory> in the input file or in the library";
  "--theory", Arg.String add_opt_theory,
124 125
      " same as -T";
  "-G", Arg.String add_opt_goal,
126 127
      "<goal> Select <goal> in the last selected theory";
  "--goal", Arg.String add_opt_goal,
128
      " same as -G";
129 130 131 132 133
  "-C", Arg.String (fun s -> opt_config := Some s),
      "<file> Read configuration from <file>";
  "--config", Arg.String (fun s -> opt_config := Some s),
      " same as -C";
  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
134
      "<dir> Add <dir> to the library search path";
135 136 137 138 139 140 141 142
  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L";
  "-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
      " same as -L (obsolete)";
  "-P", Arg.String (fun s -> opt_prover := Some s),
      "<prover> Prove or print (with -o) the selected goals";
  "--prover", Arg.String (fun s -> opt_prover := Some s),
      " same as -P";
143
  "-F", Arg.String (fun s -> opt_parser := Some s),
144
      "<format> Select input format (default: \"why\")";
145 146
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
147
  "-t", Arg.Int (fun i -> opt_timelimit := Some i),
148 149
      "<sec> Set the prover's time limit (default=10, no limit=0)";
  "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
150 151
      " same as -t";
  "-m", Arg.Int (fun i -> opt_memlimit := Some i),
152 153
      "<MiB> Set the prover's memory limit (default: no limit)";
  "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
154
      " same as -m";
155 156 157 158
  "-a", Arg.String add_opt_trans,
      "<transformation> Apply a transformation to every task";
  "--apply-transform", Arg.String add_opt_trans,
      " same as -a";
159
  "-M", Arg.String add_opt_meta,
160
      "<meta_name>=<string> Add a string meta to every task";
161 162
  "--meta", Arg.String add_opt_meta,
      " same as -M";
163
  "-D", Arg.String (fun s -> opt_driver := Some s),
164
      "<file> Specify a prover's driver (conflicts with -P)";
165 166 167 168 169 170
  "--driver", Arg.String (fun s -> opt_driver := Some s),
      " same as -D";
  "-o", Arg.String (fun s -> opt_output := Some s),
      "<dir> Print the selected goals to separate files in <dir>";
  "--output", Arg.String (fun s -> opt_output := Some s),
      " same as -o";
171 172
  "--realize", Arg.Set opt_realize,
      " Realize selected theories from the library";
173
  "--bisect", Arg.Set opt_bisect,
174 175
      " Reduce the set of needed axioms which prove a goal, \
        and output the resulting task";
176
  "--print-theory", Arg.Set opt_print_theory,
177
      " Print selected theories";
178
  "--print-namespace", Arg.Set opt_print_namespace,
179
      " Print namespaces of selected theories";
180
  "--list-transforms", Arg.Set opt_list_transforms,
181
      " List known transformations";
182
  "--list-printers", Arg.Set opt_list_printers,
183
      " List known printers";
184
  "--list-provers", Arg.Set opt_list_provers,
185
      " List known provers";
186
  "--list-formats", Arg.Set opt_list_formats,
187
      " List known input formats";
188
  "--list-metas", Arg.Set opt_list_metas,
189
      " List known metas";
190
  Debug.Opt.desc_debug_list;
191 192
  "--token-count", Arg.Set opt_token_count,
      " Only lexing, and give numbers of tokens in spec vs in program";
193 194 195 196 197
  Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
  Debug.Opt.desc_shortcut
    "type_only" "--type-only" " Stop after type checking";
  Debug.Opt.desc_debug_all;
  Debug.Opt.desc_debug;
198 199 200 201
  "--print-libdir", Arg.Set opt_print_libdir,
      " Print location of binary components (plugins, etc)";
  "--print-datadir", Arg.Set opt_print_datadir,
      " Print location of non-binary data (theories, modules, etc)";
202 203
  "--version", Arg.Set opt_version,
      " Print version information" ]
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204

205
let () = try
206 207
  Arg.parse option_list add_opt_file usage_msg;

208 209 210 211
  if !opt_version then begin
    printf "%s@." version_msg;
    exit 0
  end;
212 213 214 215 216 217 218 219
  if !opt_print_libdir then begin
    printf "%s@." Config.libdir;
    exit 0
  end;
  if !opt_print_datadir then begin
    printf "%s@." Config.datadir;
    exit 0
  end;
220

François Bobot's avatar
François Bobot committed
221
  (** Configuration *)
222
  let config = read_config !opt_config in
François Bobot's avatar
François Bobot committed
223 224 225
  let main = get_main config in
  Whyconf.load_plugins main;

226 227
  Debug.Opt.set_flags_selected ();

François Bobot's avatar
François Bobot committed
228 229
  (** listings*)

230
  let opt_list = ref false in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
231
  if !opt_list_transforms then begin
232 233
    opt_list := true;
    printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
234
      (Pp.print_list Pp.newline Pp.string)
235
      (List.sort String.compare (Trans.list_transforms ()));
236
    printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
237
      (Pp.print_list Pp.newline Pp.string)
238
      (List.sort String.compare (Trans.list_transforms_l ()))
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
239
  end;
240
  if !opt_list_printers then begin
241 242
    opt_list := true;
    printf "@[<hov 2>Known printers:@\n%a@]@\n@."
243
      (Pp.print_list Pp.newline Pp.string)
244
      (List.sort String.compare (Printer.list_printers ()))
245 246
  end;
  if !opt_list_formats then begin
247
    opt_list := true;
248
    let print1 fmt s = fprintf fmt "%S" s in
249
    let print fmt (p, l) =
250 251
      fprintf fmt "%s [%a]" p (Pp.print_list Pp.comma print1) l
    in
252
    printf "@[<hov 2>Known input formats:@\n%a@]@."
253 254 255
      (Pp.print_list Pp.newline print)
      (List.sort Pervasives.compare (Env.list_formats ()))
  end;
256
  if !opt_list_provers then begin
257
    opt_list := true;
258
    let config = read_config !opt_config in
259 260
    let print fmt prover pc = fprintf fmt "%s (%a)@\n"
      pc.id print_prover prover in
261
    let print fmt m = Mprover.iter (print fmt) m in
262 263
    let provers = get_provers config in
    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
264
  end;
265
  if !opt_list_metas then begin
266
    opt_list := true;
267 268 269
    let print fmt m = fprintf fmt "@[%s %s%a@]"
      (let s = m.meta_name in
        if String.contains s ' ' then "\"" ^ s ^ "\"" else s)
François Bobot's avatar
François Bobot committed
270
      (if m.meta_excl then "(flag) " else "")
271
      (Pp.print_list Pp.space Pretty.print_meta_arg_type) m.meta_type
272
    in
273 274 275
    let cmp m1 m2 = Pervasives.compare m1.meta_name m2.meta_name in
    printf "@[<hov 2>Known metas:@\n%a@]@\n@."
      (Pp.print_list Pp.newline print) (List.sort cmp (Theory.list_metas ()))
276
  end;
277
  opt_list :=  Debug.Opt.option_list () || !opt_list;
278
  if !opt_list then exit 0;
279 280 281 282 283 284

  if Queue.is_empty opt_queue then begin
    Arg.usage option_list usage_msg;
    exit 1
  end;

285 286 287
  if !opt_prover <> None && !opt_driver <> None then begin
    eprintf "Options '-P'/'--prover' and \
      '-D'/'--driver' cannot be used together.@.";
288 289
    exit 1
  end;
290 291 292 293 294 295 296

  if !opt_prover = None then begin
    if !opt_driver = None && !opt_output <> None then begin
      eprintf "Option '-o'/'--output' requires a prover or a driver.@.";
      exit 1
    end;
    if !opt_timelimit <> None then begin
297
      eprintf "Option '-t'/'--timelimit' requires a prover.@.";
298 299 300
      exit 1
    end;
    if !opt_memlimit <> None then begin
301
      eprintf "Option '-m'/'--memlimit' requires a prover.@.";
302 303
      exit 1
    end;
304 305 306 307
    if !opt_bisect then begin
      eprintf "Option '--bisect' requires a prover.@.";
      exit 1
    end;
308 309
    if !opt_driver = None && not !opt_print_namespace then
      opt_print_theory := true
310 311
  end;

312 313 314 315 316
  if !opt_bisect && !opt_output = None then begin
    eprintf "Option '--bisect' require a directory to output the result.@.";
    exit 1
  end;

317 318 319
  opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
  if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
  if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
320
  begin match !opt_prover with
321
  | Some s ->
322 323 324
    let prover = Whyconf.prover_by_id config s in
    opt_command := Some prover.command;
    opt_driver := Some prover.driver
325
  | None ->
326 327
      ()
  end;
328
  let add_meta task (meta,s) =
329
    let meta = lookup_meta meta in
330 331
    add_meta task meta [MAstr s]
  in
332
  opt_task := List.fold_left add_meta !opt_task !opt_metas
333

334 335 336
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
337 338

let timelimit = match !opt_timelimit with
339 340 341
  | None -> 10
  | Some i when i <= 0 -> 0
  | Some i -> i
342

343
let memlimit = match !opt_memlimit with
344 345 346 347
  | None -> 0
  | Some i when i <= 0 -> 0
  | Some i -> i

348
let print_th_namespace fmt th =
349
  Pretty.print_namespace fmt th.th_name.Ident.id_string th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350

351
let fname_printer = ref (Ident.create_ident_printer [])
MARCHE Claude's avatar
MARCHE Claude committed
352

353 354 355
let output_task drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
356
    try Filename.chop_extension fname with _ -> fname in
357 358 359 360 361 362 363 364 365 366 367 368 369
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task drv (formatter_of_out_channel cout) task;
  close_out cout

let output_task_prepared drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
370
    try Filename.chop_extension fname with _ -> fname in
371 372 373 374 375 376 377 378 379 380
  let tname = th.th_name.Ident.id_string in
  let dest = Driver.file_of_task drv fname tname task in
  (* Uniquify the filename before the extension if it exists*)
  let i = try String.rindex dest '.' with _ -> String.length dest in
  let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
  let ext = String.sub dest i (String.length dest - i) in
  let cout = open_out (Filename.concat dir (name ^ ext)) in
  Driver.print_task_prepared drv (formatter_of_out_channel cout) task;
  close_out cout

381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
let output_theory drv fname _tname th task dir =
  let fname = Filename.basename fname in
  let fname =
    try Filename.chop_extension fname with _ -> fname in
  let dest = Driver.file_of_theory drv fname th in
  let file = Filename.concat dir dest in
  let old =
    if Sys.file_exists file then begin
      let backup = file ^ ".bak" in
      Sys.rename file backup;
      Some (open_in backup)
    end else None in
  let cout = open_out file in
  Driver.print_task ?old drv (formatter_of_out_channel cout) task;
  close_out cout
396

397
let do_task env drv fname tname (th : Theory.theory) (task : Task.task) =
398
  match !opt_output, !opt_command with
399 400 401 402 403 404 405 406 407 408
    | Some dir, _ when !opt_realize ->
        output_theory drv fname tname th task dir
    | None, _ when !opt_realize ->
        (* FIXME: we should be able to realize other formats *)
        let file,ich = Env.find_channel env "why" th.th_path in
        let dir = try Filename.chop_extension file with _ ->
          eprintf "File %s does not have an extension.@." file;
          exit 1 in
        close_in ich;
        output_theory drv fname tname th task dir
409
    | Some dir, Some command when !opt_bisect ->
410 411 412 413 414 415 416 417 418 419 420
        let test task =
          let call = Driver.prove_task_prepared
            ~command ~timelimit ~memlimit drv task in
          let res = Call_provers.wait_on_call (call ()) () in
          printf "%s %s %s : %a@." fname tname
            (task_goal task).Decl.pr_name.Ident.id_string
            Call_provers.print_prover_result res;
          res.Call_provers.pr_answer = Call_provers.Valid in
        let prepared_task = Driver.prepare_task drv task in
        if not (test prepared_task)
        then printf "I can't bisect %s %s %s which is not valid@." fname tname
421
          (task_goal task).Decl.pr_name.Ident.id_string
422 423 424
        else
          let prepared_task = Task.bisect test prepared_task in
          output_task_prepared drv fname tname th prepared_task dir
425
    | None, Some command ->
Andrei Paskevich's avatar
Andrei Paskevich committed
426 427
        let call = Driver.prove_task ~command ~timelimit ~memlimit drv task in
        let res = Call_provers.wait_on_call (call ()) () in
428
        printf "%s %s %s : %a@." fname tname
429
          (task_goal task).Decl.pr_name.Ident.id_string
430 431
          Call_provers.print_prover_result res
    | None, None ->
432
        Driver.print_task drv std_formatter task
433
    | Some dir, _ -> output_task drv fname tname th task dir
434

435
let do_tasks env drv fname tname th task =
436
  let lookup acc t =
437 438
    (try Trans.singleton (Trans.lookup_transform t env) with
       Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) :: acc
439
  in
440
  let trans = List.fold_left lookup [] !opt_trans in
441
  let apply tasks tr =
442
    List.rev (List.fold_left (fun acc task ->
443
      List.rev_append (Trans.apply tr task) acc) [] tasks)
444
  in
445
  let tasks = List.fold_left apply [task] trans in
446
  List.iter (do_task env drv fname tname th) tasks
447

448
let do_theory env drv fname tname th glist =
449 450 451 452
  if !opt_print_theory then
    printf "%a@." Pretty.print_theory th
  else if !opt_print_namespace then
    printf "%a@." print_th_namespace th
453 454 455 456 457 458 459 460 461 462 463 464
  else if !opt_realize then
    if th.th_path = [] then begin
      eprintf "Theory %s is not from the library.@." tname;
      exit 1
    end else if not (Queue.is_empty glist) then begin
      eprintf "Cannot realize individual goals.@.";
      exit 1
    end else begin
      let drv = Util.of_option drv in
      let task = Task.use_export None th in
      do_tasks env drv fname tname th task
    end
465
  else begin
466
    let add acc (x,l) =
467 468 469 470
      let pr = try ns_find_pr th.th_export l with Not_found ->
        eprintf "Goal '%s' not found in theory '%s'.@." x tname;
        exit 1
      in
471
      Decl.Spr.add pr acc
472 473
    in
    let drv = Util.of_option drv in
474 475 476 477
    let prs = Queue.fold add Decl.Spr.empty glist in
    let sel = if Decl.Spr.is_empty prs then None else Some prs in
    let tasks = List.rev (split_theory th sel !opt_task) in
    List.iter (do_tasks env drv fname tname th) tasks
478
  end
MARCHE Claude's avatar
MARCHE Claude committed
479

480
let do_global_theory env drv (tname,p,t,glist) =
481 482 483
  let th = try Env.find_theory env p t with Env.TheoryNotFound _ ->
    eprintf "Theory '%s' not found.@." tname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
484
  in
485
  do_theory env drv "lib" tname th glist
MARCHE Claude's avatar
MARCHE Claude committed
486

487
let do_local_theory env drv fname m (tname,_,t,glist) =
488
  let th = try Mstr.find t m with Not_found ->
489 490
    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
491
  in
492
  do_theory env drv fname tname th glist
493

494 495 496
let total_annot_tokens = ref 0
let total_program_tokens = ref 0

497
let do_input env drv = function
498
  | None, _ when !opt_parse_only || !opt_type_only ->
499
      ()
500
  | None, tlist ->
MARCHE Claude's avatar
MARCHE Claude committed
501
      Queue.iter (do_global_theory env drv) tlist
502
  | Some f, tlist ->
503 504 505 506
      let fname, cin = match f with
        | "-" -> "stdin", stdin
        | f   -> f, open_in f
      in
507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
      if !opt_token_count then
        let lb = Lexing.from_channel cin in
        let a,p = Lexer.token_counter lb in
        close_in cin;
        if a = 0 then
          begin
            (* hack: we assume it is a why file and not a mlw *)
            total_annot_tokens := !total_annot_tokens + p;
            Format.printf "File %s: %d tokens@." f p;
          end
        else
          begin
            total_program_tokens := !total_program_tokens + p;
            total_annot_tokens := !total_annot_tokens + a;
            Format.printf "File %s: %d tokens in annotations@." f a;
            Format.printf "File %s: %d tokens in programs@." f p
          end
524
      else
525 526 527 528
        let m = Env.read_channel ?format:!opt_parser env fname cin in
        close_in cin;
        if !opt_type_only then
          ()
MARCHE Claude's avatar
MARCHE Claude committed
529
        else
530 531 532 533 534 535 536
          if Queue.is_empty tlist then
            let glist = Queue.create () in
            let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
            let do_th _ (t,th) = do_theory env drv fname t th glist in
            Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
          else
            Queue.iter (do_local_theory env drv fname m) tlist
MARCHE Claude's avatar
MARCHE Claude committed
537

538 539
let () =
  try
540
    let env = Env.create_env !opt_loadpath in
541
    let drv = Util.option_map (load_driver env) !opt_driver in
542 543 544 545 546
    Queue.iter (do_input env drv) opt_queue;
    if !opt_token_count then
      Format.printf "Total: %d annot/%d programs, ratio = %.3f@." 
        !total_annot_tokens !total_program_tokens
        ((float !total_annot_tokens) /. (float !total_program_tokens))
547
  with e when not (Debug.test_flag Debug.stack_trace) ->
548
    eprintf "%a@." Exn_printer.exn_printer e;
549
    exit 1
550

551
(*
552
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
553
compile-command: "unset LANG; make -C .. byte"
554
End:
555
*)