autodetection.ml 21.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
(*****
1) For every block, for every executable call the prover using the
version switch and add the prover to the configuration if the version
match one of the version_ok or version_old but none of the version_bad
2) We consider that an executable name which appears in a block, but
which version isn't a version_ok, version_old or version_bad has an
unknown version
3) For every executable which have an unknown version, we add the
prover using the first block that contains it.

Don't use the family argument except when you add manualy one prover.

So the order of the block is used only when the version of an
executable appears in none of the block.

A block with more than one exec fields is now the same thing than if you
split the block into blocks containing one fields.

New message field that allows to print a message when a prover is
31
detected. If a message is not present, we print ", OK." if the version
32 33 34 35 36 37
is good (version_good) and not old, and " (it is an old version)." if
the version is old (version_old).

The field command can be missing in a block, in that case the block
defines a version known to be buggy: no prover config is generated.

38 39
The regexp must start with ^.

40 41
*)

42
open Format
43
open Wstdlib
44
open Whyconf
45
module Wc = Whyconf
46 47
open Rc

48
let debug = Debug.register_info_flag "autodetect"
Andrei Paskevich's avatar
Andrei Paskevich committed
49 50
  ~desc:"Print@ debugging@ messages@ about@ auto-detection@ \
         of@ external@ provers."
51 52 53 54 55 56 57 58

(* auto-detection of provers *)

type prover_kind = ATP | ITP
type prover_autodetection_data =
    { kind : prover_kind;
      prover_id : string;
      prover_name : string;
59
      prover_altern : string;
60
      support_library : string;
61 62 63
      execs : string list;
      version_switch : string;
      version_regexp : string;
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66
      versions_ok : (string * Str.regexp) list;
      versions_old : (string * Str.regexp) list;
      versions_bad : (string * Str.regexp) list;
67 68
      (** If none it's a fake prover (very bad version) *)
      prover_command : string option;
69
      prover_command_steps : string option;
70 71
      prover_driver : string;
      prover_editor : string;
72
      prover_in_place : bool;
73
      use_at_auto_level : int;
74
      message : string option;
75 76 77 78 79
    }

let prover_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
80
    ["name";"support_library";
81
     "exec";"version_switch";"version_regexp";
82
     "version_ok";"version_old";"version_bad";"command"; "command_steps";
83
     "editor";"driver";"in_place";"message";"alternative";"use_at_auto_level"]
84 85 86

let load_prover kind (id,section) =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
87
  let reg_map = List.rev_map (fun s -> (s,why3_regexp_of_string s)) in
88
  let prover = { kind = kind;
89 90
    prover_id = id;
    prover_name = get_string section "name";
91
    prover_altern = get_string section ~default:"" "alternative";
92
    support_library = get_string section ~default:"" "support_library";
93 94 95
    execs = get_stringl section "exec";
    version_switch = get_string section ~default:"" "version_switch";
    version_regexp = get_string section ~default:"" "version_regexp";
96 97 98
    versions_ok = reg_map (get_stringl section ~default:[] "version_ok");
    versions_old = reg_map (get_stringl section ~default:[] "version_old");
    versions_bad = reg_map (get_stringl section ~default:[] "version_bad");
99
    prover_command = get_stringo section "command";
100
    prover_command_steps = get_stringo section "command_steps";
101
    prover_driver = get_string section ~default:""  "driver";
102
    prover_editor = get_string section ~default:"" "editor";
103
    prover_in_place = get_bool section ~default:false "in_place";
104
    use_at_auto_level = get_int section ~default:0 "use_at_auto_level";
105
    message = get_stringo section "message";
106 107 108 109 110
  } in
  if prover.prover_command != None && prover.prover_driver = "" then
    invalid_arg
      (sprintf "In section prover %s command specified without driver" id);
  prover
111

112
(* dead code
113 114 115 116
let editor_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["command"]
117
*)
118 119 120

let load_editor section =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
121 122
  { editor_name = get_string section "name";
    editor_command = get_string section "command";
123 124 125
    editor_options = []
  }

126
(** returned in reverse order *)
127 128
let load rc =
  let atps = get_family rc "ATP" in
129
  let atps = List.rev_map (load_prover ATP) atps in
130
  let itps = get_family rc "ITP" in
131
  let tps = List.fold_left (Lists.cons (load_prover ITP)) atps itps in
132 133
  tps

134 135 136 137 138 139 140 141 142 143
let load_prover_shortcut acc (_, section) =
  let name = get_string section "name" in
  let version = get_stringo section "version" in
  let altern = get_stringo section "alternative" in
  let shortcuts = get_stringl section "shortcut" in
  let fp = mk_filter_prover ?version ?altern name in
  List.fold_left (fun acc shortcut ->
    (fp,shortcut)::acc
  ) acc shortcuts

144 145 146 147 148
module Hstr2 = Hashtbl.Make(struct
  type t = string * string
  let hash = Hashtbl.hash
  let equal = (=)
end)
François Bobot's avatar
François Bobot committed
149

150 151
type env =
  {
152
    (* memoization of (exec_name,version_switch)
153
        -> Some output | None doesn't exists *)
François Bobot's avatar
François Bobot committed
154
    prover_output : string option Hstr2.t;
155
    (* existing executable table:
François Bobot's avatar
François Bobot committed
156 157
        exec_name -> | Some (priority, id, prover_config)
                                  unknown version (neither good or bad)
158
                     | None               there is a good version *)
François Bobot's avatar
François Bobot committed
159
    prover_unknown_version :
MARCHE Claude's avatar
MARCHE Claude committed
160
      (prover_autodetection_data * int * string * config_prover) option Hstr.t;
161
    (* string -> priority * prover  *)
François Bobot's avatar
François Bobot committed
162
    prover_shortcuts : (int * prover) Hstr.t;
163 164 165 166
    mutable possible_prover_shortcuts : (filter_prover * string) list;
  }

let create_env shortcuts =
François Bobot's avatar
François Bobot committed
167 168 169
{ prover_output = Hstr2.create 10;
  prover_unknown_version = Hstr.create 10;
  prover_shortcuts = Hstr.create 5;
170 171 172
  possible_prover_shortcuts = shortcuts;
 }

François Bobot's avatar
François Bobot committed
173 174 175 176 177 178
let next_priority =
  let r = ref 0 in
  fun () -> decr r; !r

let highest_priority = 0

179
let read_auto_detection_data main =
180 181
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
182 183
  try
    let rc = Rc.from_file filename in
184 185 186
    let shortcuts =
      List.fold_left load_prover_shortcut [] (get_family rc "shortcut") in
    List.rev (load rc), create_env shortcuts
187 188
  with
    | Failure "lexing" ->
189
        Loc.errorm "Syntax error in provers-detection-data.conf@."
190
    | Not_found ->
191
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
192

193 194 195 196 197 198 199 200 201 202 203 204 205
let read_editors main =
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
  try
    let rc = Rc.from_file filename in
    List.fold_left (fun editors (id, section) ->
      Meditor.add id (load_editor section) editors
    ) Meditor.empty (get_family rc "editor")
  with
    | Failure "lexing" ->
        Loc.errorm "Syntax error in provers-detection-data.conf@."
    | Not_found ->
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
206

207
let make_command =
208
  let cmd_regexp = Str.regexp "%\\(.\\)" in
209 210 211 212 213 214
  fun exec com ->
    let replace s = match Str.matched_group 1 s with
      | "e" -> exec
      | c -> "%"^c
    in
    Str.global_substitute cmd_regexp replace com
215

216
(* dead code
217 218 219
let sanitize_exec =
  let first c = match c with
    | '_' | ' ' -> "_"
220
    | _ -> char_to_alpha c
221 222 223
  in
  let rest c = match c with
    | '+' | '-' | '.' -> String.make 1 c
224
    | _ -> char_to_alnumus c
225
  in
226
  sanitizer first rest
227
*)
228

229
let ask_prover_version exec_name version_switch =
230
  let out = Filename.temp_file "out" "" in
231
  let cmd = sprintf "%s %s" exec_name version_switch in
232
  let c = sprintf "(%s) > %s 2>&1" cmd out in
233
  Debug.dprintf debug "Run: %s@." c;
234 235 236 237 238 239 240 241
  try
    let ret = Sys.command c in
    let ch = open_in out in
    let c = Sysutil.channel_contents ch in
    close_in ch;
    Sys.remove out;
    if ret <> 0 then begin
      Debug.dprintf debug "command '%s' failed. Output:@\n%s@." cmd c;
242
      None
243 244 245 246
    end else Some c
  with Not_found | End_of_file | Sys_error _ ->
    Debug.dprintf debug "command '%s' failed@." cmd;
    None
247 248 249

let ask_prover_version env exec_name version_switch =
  try
François Bobot's avatar
François Bobot committed
250
    Hstr2.find env.prover_output (exec_name,version_switch)
251 252
  with Not_found ->
    let res = ask_prover_version exec_name version_switch in
François Bobot's avatar
François Bobot committed
253
    Hstr2.add env.prover_output (exec_name,version_switch) res;
254 255
    res

MARCHE Claude's avatar
MARCHE Claude committed
256
let check_version version (_,schema) = Str.string_match schema version 0
257 258

let known_version env exec_name =
François Bobot's avatar
François Bobot committed
259
  Hstr.replace env.prover_unknown_version exec_name None
260

MARCHE Claude's avatar
MARCHE Claude committed
261
let unknown_version env exec_name prover_id prover_config data priority =
François Bobot's avatar
François Bobot committed
262 263
  if not (Hstr.mem env.prover_unknown_version exec_name)
  then Hstr.replace env.prover_unknown_version exec_name
MARCHE Claude's avatar
MARCHE Claude committed
264
    (Some (data,priority,prover_id,prover_config))
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283


let empty_alt s = if s = "" then "alt" else s

let find_prover_altern provers prover_id =
  if not (Mprover.mem prover_id provers) then prover_id
  else
    let prover_id =
      {prover_id with
        Wc.prover_altern = empty_alt prover_id.Wc.prover_altern} in
    if not (Mprover.mem prover_id provers) then prover_id
    else
    let rec aux n =
      let prover_id_n = {prover_id with
        Wc.prover_altern = sprintf "%s_%i"
          (empty_alt prover_id.Wc.prover_altern) n} in
      if Mprover.mem prover_id_n provers
      then aux (n+1)
      else prover_id_n in
284 285 286
    (* start with 2 in order to have toto_alt, toto_alt2,
       toto_alt3,... and not toto_alt, toto_alt1 which can be
       confusing *)
287 288 289
    aux 2

let add_prover_with_uniq_id prover provers =
290
  (* find an unique prover triplet *)
291 292
  let prover_id = find_prover_altern provers prover.Wc.prover in
  let prover = {prover with Wc.prover = prover_id} in
293
  Mprover.add prover_id prover provers
294

295 296 297 298
let add_prover_shortcuts env prover =
  let rec aux = function
    | [] -> []
    | (fp,s)::l when filter_prover fp prover ->
François Bobot's avatar
François Bobot committed
299
      Hstr.replace env.prover_shortcuts s (highest_priority,prover);
300 301 302 303
      aux l
    | a::l -> a::(aux l) in
  env.possible_prover_shortcuts <- aux env.possible_prover_shortcuts

François Bobot's avatar
François Bobot committed
304
let add_id_prover_shortcut env id prover priority =
305
  match Hstr.find_opt env.prover_shortcuts id with
François Bobot's avatar
François Bobot committed
306
  | Some (p,_) when p >= priority -> ()
307
(*
308
  | Some _ -> assert false
309
 *)
François Bobot's avatar
François Bobot committed
310 311
  | _ -> Hstr.replace env.prover_shortcuts id (priority,prover)

312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
let prover_auto_levels = Hprover.create 5

let record_prover_for_auto_mode prover level =
  Hprover.replace prover_auto_levels prover (level,false)

let check_prover_auto_level prover =
  try
    let lev,_ = Hprover.find prover_auto_levels prover in
    Hprover.replace prover_auto_levels prover (lev,true)
  with Not_found -> ()

let generate_auto_strategies config =
  eprintf "Generating strategies:@.";
  Hprover.iter
    (fun p (lev,b) ->
327 328
     if b then eprintf "  Prover %a will be used in Auto level >= %d@."
                       Whyconf.print_prover p lev) prover_auto_levels;
329
  (* Split VCs *)
330
  let code = "t split_vc exit" in
331
  let split = {
332 333
      strategy_name = "Split_VC";
      strategy_desc = "Split@ the@ VC@ into@ subgoals";
334 335 336
      strategy_shortcut = "s";
      strategy_code = code }
  in
337
  (* Auto level 0 and 1 *)
338 339 340 341
  let provers_level1 =
    Hprover.fold
      (fun p (lev,b) acc ->
       if b && lev = 1 then
MARCHE Claude's avatar
MARCHE Claude committed
342
         let name = Whyconf.prover_parseable_format p in name :: acc
343 344
       else acc) prover_auto_levels []
  in
345 346 347
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
  let code = flush_str_formatter () in
  let auto0 = {
MARCHE Claude's avatar
MARCHE Claude committed
348
      strategy_name = "Auto_level_0";
349 350 351 352
      strategy_desc = "Automatic@ run@ of@ main@ provers";
      strategy_shortcut = "0";
      strategy_code = code }
  in
353 354
  fprintf str_formatter "start:@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
355
  fprintf str_formatter "t split_all_full start@\n";
356 357 358
  List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
  let code = flush_str_formatter () in
  let auto1 = {
MARCHE Claude's avatar
MARCHE Claude committed
359
      strategy_name = "Auto_level_1";
360 361 362 363 364 365 366 367 368
      strategy_desc = "Automatic@ run@ of@ main@ provers";
      strategy_shortcut = "1";
      strategy_code = code }
  in
  (* Auto level 2 *)
  let provers_level2 =
    Hprover.fold
      (fun p (lev,b) acc ->
       if b && lev >= 1 && lev <= 2 then
MARCHE Claude's avatar
MARCHE Claude committed
369
         let name = Whyconf.prover_parseable_format p in name :: acc
370 371 372 373
       else acc) prover_auto_levels []
  in
  fprintf str_formatter "start:@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level2;
374
  fprintf str_formatter "t split_all_full start@\n";
375 376 377 378
  List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2;
  fprintf str_formatter "t introduce_premises afterintro@\n";
  fprintf str_formatter "afterintro:@\n";
  fprintf str_formatter "t inline_goal afterinline@\n";
379
  fprintf str_formatter "g trylongertime@\n";
380
  fprintf str_formatter "afterinline:@\n";
381
  fprintf str_formatter "t split_all_full start@\n";
382
  fprintf str_formatter "trylongertime:@\n";
383 384 385
  List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
  let code = flush_str_formatter () in
  let auto2 = {
MARCHE Claude's avatar
MARCHE Claude committed
386
      strategy_name = "Auto_level_2";
387 388 389 390
      strategy_desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations";
      strategy_shortcut = "2";
      strategy_code = code }
  in
391 392
  add_strategy
    (add_strategy
393
       (add_strategy
394
          (add_strategy config split) auto0) auto1) auto2
395

396 397 398 399 400 401 402 403 404 405 406 407
let check_support_library data ver =
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace s = match Str.matched_group 1 s with
    | "l" -> Config.libdir
    | "d" -> Config.datadir
    | c -> c in
  let sl = Str.global_substitute cmd_regexp replace data.support_library in
  try
    let f = open_in sl in
    let support_ver = input_line f in
    close_in f;
    if support_ver = ver then true
408
    else if support_ver = "" then raise Not_found
409 410
    else begin
      eprintf
411
        "Found prover %s version %s, but the compiled Why3 library supports only version %s@."
412 413 414 415 416
        data.prover_name ver support_ver;
      false
    end
  with Sys_error _ | Not_found ->
    eprintf
417
      "Found prover %s version %s, but no Why3 libraries were compiled for it@."
418 419 420
      data.prover_name ver;
    false

421 422 423 424
exception Skip    (* prover is ignored *)
exception Discard (* prover is recognized, but unusable *)

let detect_exec env data exec_name =
425
  let s = ask_prover_version env exec_name data.version_switch in
426 427 428 429
  let s =
    match s with
    | None -> raise Skip
    | Some s -> s in
430 431
  let re = Str.regexp data.version_regexp in
  let ver =
432 433
    try
      ignore (Str.search_forward re s 0);
434
      Str.matched_group 1 s
435
    with Not_found ->
436
      Debug.dprintf debug "Warning: found prover %s but name/version not \
437
                       recognized by regexp `%s'@."
438 439 440
        data.prover_name data.version_regexp;
      Debug.dprintf debug "Answer was `%s'@." s;
      ""
441
  in
442
  (* bad here means not good, it is not the same thing as a version
443
     of a prover with known problems *)
444
  let bad = List.exists (check_version ver) data.versions_bad in
445 446 447 448
  if bad then raise Discard;
  let good = List.exists (check_version ver) data.versions_ok in
  let old  = List.exists (check_version ver) data.versions_old in
  let prover_command =
449 450
    match data.prover_command with
    | None ->
451 452
      (* empty prover: a matching version means known problems *)
      if not (good || old) then raise Skip;
453 454
      eprintf "Found prover %s version %s%s@."
        data.prover_name ver
455
        (Opt.get_def
456
           ". This version of the prover is known to have problems."
457
           data.message);
458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 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 509 510 511 512
      raise Discard
    | Some prover_command -> prover_command
  in
  (* create the prover config *)
  let c = make_command exec_name prover_command in
  let c_steps = Opt.map (make_command exec_name) data.prover_command_steps in
  let prover =
    { Wc.prover_name = data.prover_name;
      prover_version = ver;
      prover_altern = data.prover_altern } in
  let prover_config =
    { prover = prover;
      command = c;
      command_steps = c_steps;
      driver = data.prover_driver;
      editor = data.prover_editor;
      in_place = data.prover_in_place;
      interactive = (match data.kind with ITP -> true | ATP -> false);
      extra_options = [];
      extra_drivers = [] } in
  (* if unknown, temporarily put the prover away *)
  if not (good || old) then begin
    let priority = next_priority () in
    unknown_version env exec_name data.prover_id prover_config data priority;
    raise Skip
  end;
  (* check if this prover needs compile-time support *)
  if data.support_library <> "" && not (check_support_library data ver) then
    raise Discard;
  let priority = next_priority () in
  eprintf "Found prover %s version %s%s@."
    data.prover_name ver
    (Opt.get_def
       (if old then
	   " (old version, please consider upgrading)."
	else
	   if data.prover_altern <> "" then
	     " (alternative: " ^ data.prover_altern ^ ")"
	   else
	     ", OK.")
       data.message);
  add_prover_shortcuts env prover;
  add_id_prover_shortcut env data.prover_id prover priority;
  let level = data.use_at_auto_level in
  if level > 0 then record_prover_for_auto_mode prover level;
  prover_config

let detect_exec env data acc exec_name =
  try
    let prover_config = detect_exec env data exec_name in
    known_version env exec_name;
    add_prover_with_uniq_id prover_config acc
  with
  | Skip -> acc
  | Discard -> known_version env exec_name; acc
513

514 515
let detect_prover env acc data =
  List.fold_left (detect_exec env data) acc data.execs
516

MARCHE Claude's avatar
MARCHE Claude committed
517 518 519 520
let pp_versions =
  Pp.print_list Pp.comma
                (Pp.print_pair_delim Pp.nothing Pp.nothing Pp.nothing Pp.string Pp.nothing)

521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537
let detect_unknown env pc =
  let (data,priority,prover_id,prover_config) =
    match pc with
    | None -> raise Skip
    | Some pc -> pc in
  let prover = prover_config.prover in
  let ver = prover.prover_version in
  if data.support_library <> "" && not (check_support_library data ver) then raise Skip;
  Warning.emit "@[Prover %s version %s is not known to be supported.@\n\
                Known versions for this prover:@ %a@\n\
                Known old versions for this prover:@ %a@]@."
    prover.Wc.prover_name ver
    pp_versions data.versions_ok
    pp_versions data.versions_old;
  add_id_prover_shortcut env prover_id prover priority;
  prover_config

538
let detect_unknown env detected =
François Bobot's avatar
François Bobot committed
539
  Hstr.fold (fun _ pc acc ->
540 541
    try add_prover_with_uniq_id (detect_unknown env pc) acc
    with Skip -> acc)
542
    env.prover_unknown_version detected
543

544
let convert_shortcuts env =
François Bobot's avatar
François Bobot committed
545
  Hstr.fold (fun s (_,p) acc ->
546
    check_prover_auto_level p; Mstr.add s p acc
547 548
  ) env.prover_shortcuts Mstr.empty

549 550
let run_auto_detection config =
  let main = get_main config in
551
  let l,env = read_auto_detection_data main in
552
  let detected = List.fold_left (detect_prover env) Mprover.empty l in
553
  let length_recognized = Mprover.cardinal detected in
554
  let detected = detect_unknown env detected in
555 556 557 558 559 560 561
  let length_detected = Mprover.cardinal detected in
  if length_detected > length_recognized then
    eprintf
      "%d prover(s) added (including %d prover(s) with an unrecognized version)@."
      length_detected (length_detected - length_recognized)
  else
    eprintf "%d prover(s) added@." length_detected;
562
  let shortcuts = convert_shortcuts env in
563
  let config = generate_auto_strategies config in
564 565 566 567
  let config = set_editors config (read_editors main) in
  let config = set_prover_shortcuts config shortcuts in
  let config = set_provers config detected in
  config
568 569

let list_prover_ids () =
570
  let config = default_config "" in
571
  let main = get_main config in
572
  let l,_ = read_auto_detection_data main in
573 574 575
  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
  Sstr.elements s

576
let get_suffix id alt =
577 578
  let ilen = String.length id in
  let alen = String.length alt in
579
  let rec aux i =
580 581
    if i = alen then "alt" else
    if i = ilen then String.sub alt i (alen-i) else
582
    if id.[i] = alt.[i] then aux (i+1) else
583 584
    String.sub alt i (alen-i)
  in
585 586 587 588 589 590
  aux 0


let get_altern id path =
  let alt = Filename.basename path in
  get_suffix id alt
591

592 593
let add_existing_shortcuts env shortcuts =
  let aux shortcut prover =
François Bobot's avatar
François Bobot committed
594
    Hstr.replace env.prover_shortcuts shortcut (highest_priority,prover);
595
    env.possible_prover_shortcuts <-
François Bobot's avatar
François Bobot committed
596 597
      List.filter (fun (_,s) -> s = shortcut)
      env.possible_prover_shortcuts
598 599 600
  in
  Mstr.iter aux shortcuts

601 602
let add_prover_binary config id path =
  let main = get_main config in
603 604
  let l,env = read_auto_detection_data main in
  add_existing_shortcuts env (get_prover_shortcuts config);
605 606
  let l = List.filter (fun p -> p.prover_id = id) l in
  if l = [] then Loc.errorm "Unknown prover id: %s" id;
607
  let detected = List.fold_left
608
    (fun acc data -> detect_exec env data acc path) Mprover.empty l in
609 610 611
  let detected = detect_unknown env detected in
  if Mprover.is_empty detected then
    Loc.errorm "File %s does not correspond to the prover id %s" path id;
612
  let provers = get_provers config in
613
  let fold _ p provers =
614
    (* find a prover altern not used *)
615 616 617
    (* Is a prover with this name and version already in config? *)
    let prover_id =
      if not (Mprover.mem p.prover provers) then p.prover else
618 619 620
        let alt = match p.prover.Wc.prover_altern, get_altern id path with
          | "", s -> s | s, "" -> s | s1, s2 -> s1 ^ " " ^ s2 in
        let prover_id = { p.prover with Wc.prover_altern = alt } in
621
        find_prover_altern provers prover_id in
622 623
    let p = {p with prover = prover_id} in
    add_prover_with_uniq_id p provers in
624
  let provers = Mprover.fold fold detected provers in
625
  let shortcuts = convert_shortcuts env in
626
  let config = set_provers config ~shortcuts provers in
627
  config