autodetection : simplify the semantics of the file provers-detection-data.conf

* all the provers with the same prover_id are threated as one prover,
* the first description of a prover in the file pdd.conf which have an
  executable with a good version is used,
* the order used to test the executable (exec) inside a prover description
  is not specified,
* a version_bad allows to forbid a version.
* a version_ok matches no warning is printed
* a version_old matches a warning is printed
* if no version matches a warning is printed

share/provers-detection-data.conf.in

-[ATP alt-ergo-old]
-name = "Alt-Ergo (no arrays)"
-exec = "ergo"
+[ATP alt-ergo]
+name = "Alt-Ergo"
 exec = "alt-ergo"
-exec = "alt-ergo-0.91"
 version_switch = "-version"
 version_regexp = ".*Ergo \\([^ \n]*\\)"
-version_old = "0.92.2"
-version_old = "0.92.1"
-version_old = "0.92"
-version_old = "0.91"
-version_old = "0.9"
-version_old = "0.8"
+version_ok = "0.93"
+version_bad = "0.92.3"
+version_bad = "0.92.2"
+version_bad = "0.92.1"
+version_bad = "0.92"
+version_bad = "0.91"
+version_bad = "0.9"
+version_bad = "0.8"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
-driver = "drivers/alt_ergo.drv"
+driver = "drivers/alt_ergo_trunk.drv"
 
 [ATP alt-ergo]
-name = "Alt-Ergo"
+name = "Alt-Ergo (no arrays)"
+exec = "ergo"
 exec = "alt-ergo"
+exec = "alt-ergo-0.91"
 version_switch = "-version"
 version_regexp = ".*Ergo \\([^ \n]*\\)"
-version_ok = "0.93"
-version_old = "0.92.3"
 version_old = "0.92.2"
 version_old = "0.92.1"
 version_old = "0.92"
@@ -28,7 +28,7 @@ version_old = "0.91"
 version_old = "0.9"
 version_old = "0.8"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
-driver = "drivers/alt_ergo_trunk.drv"
+driver = "drivers/alt_ergo.drv"
 
 [ATP cvc3]
 name = "CVC3"

src/driver/autodetection.ml

@@ -36,6 +36,7 @@ type prover_autodetection_data =
       version_regexp : string;
       versions_ok : string list;
       versions_old : string list;
+      versions_bad : string list;
       prover_command : string;
       prover_driver : string;
       prover_editor : string;
@@ -45,7 +46,7 @@ let prover_keys =
   let add acc k = Sstr.add k acc in
   List.fold_left add Sstr.empty
     ["name";"exec";"version_switch";"version_regexp";
-     "version_ok";"version_old";"command";
+     "version_ok";"version_old";"version_bad";"command";
      "editor";"driver"]
 
 let load_prover kind (id,section) =
@@ -58,14 +59,16 @@ let load_prover kind (id,section) =
     version_regexp = get_string section ~default:"" "version_regexp";
     versions_ok = get_stringl section ~default:[] "version_ok";
     versions_old = get_stringl section ~default:[] "version_old";
+    versions_bad = get_stringl section ~default:[] "version_bad";
     prover_command = get_string section "command";
     prover_driver = get_string section "driver";
     prover_editor = get_string section ~default:"" "editor";
   }
 
+(** returned in reverse order *)
 let load rc =
   let atps = get_family rc "ATP" in
-  let atps = List.map (load_prover ATP) atps in
+  let atps = List.rev_map (load_prover ATP) atps in
   let itps = get_family rc "ITP" in
   let tps = List.fold_left (cons (load_prover ITP)) atps itps in
   tps
@@ -109,85 +112,82 @@ let sanitize_exec =
   in
   Ident.sanitizer first rest
 
-let detect_prover main acc0 data =
-  let keys = Queue.create () in
-  let acc = List.fold_left
-    (fun acc com ->
-	let out = Filename.temp_file "out" "" in
-        let cmd = sprintf "%s %s" com data.version_switch in
-	let c = sprintf "(%s) > %s 2>&1" cmd out in
-        Debug.dprintf debug "Run : %s@." c;
-	let ret = Sys.command c in
-	if ret <> 0 then
-	  begin
-	    Debug.dprintf debug "command '%s' failed@." cmd;
-	    acc
-	  end
-	else
-	  let s =
-            try
-              let ch = open_in out in
-              let c = Sysutil.channel_contents ch in
-              close_in ch;
-	      Sys.remove out;
-              c
-            with Not_found | End_of_file  -> ""
-          in
-	  let re = Str.regexp data.version_regexp in
-	  try
-            ignore (Str.search_forward re s 0);
-	    let nam = data.prover_name in
-	    let ver = Str.matched_group 1 s in
-            if List.mem ver data.versions_ok then
-	      eprintf "Found prover %s version %s, OK.@." nam ver
+let detect_exec main data com =
+  let out = Filename.temp_file "out" "" in
+  let cmd = sprintf "%s %s" com data.version_switch in
+  let c = sprintf "(%s) > %s 2>&1" cmd out in
+  Debug.dprintf debug "Run : %s@." c;
+  let ret = Sys.command c in
+  if ret <> 0 then
+    begin
+      Debug.dprintf debug "command '%s' failed@." cmd;
+      None
+    end
+  else
+    let s =
+      try
+        let ch = open_in out in
+        let c = Sysutil.channel_contents ch in
+        close_in ch;
+	Sys.remove out;
+        c
+      with Not_found | End_of_file  -> ""
+    in
+    let re = Str.regexp data.version_regexp in
+    try
+      ignore (Str.search_forward re s 0);
+      let nam = data.prover_name in
+      let ver = Str.matched_group 1 s in
+      if List.mem ver data.versions_bad then
+        None
+      else begin
+        if List.mem ver data.versions_ok then
+	  eprintf "Found prover %s version %s, OK.@." nam ver
+        else
+          begin
+            prover_tips_info := true;
+            if List.mem ver data.versions_old then
+              eprintf "Warning: prover %s version %s is quite old, please \
+                     consider upgrading to a newer version.@."
+                nam ver
             else
-              begin
-                prover_tips_info := true;
-                if List.mem ver data.versions_old then
-                  eprintf "Warning: prover %s version %s is quite old, please \
-                           consider upgrading to a newer version.@."
-                    nam ver
-                else
-                  eprintf "Warning: prover %s version %s is not known to be \
-                           supported, use it at your own risk!@." nam ver
-              end;
-            incr provers_found;
-            let c = make_command com data.prover_command in
-            let key = sanitize_exec com in
-            Queue.add key keys;
-            Mstr.add key
-              {name = data.prover_name;
-               version = ver;
-               command = c;
-               driver  = Filename.concat (datadir main) data.prover_driver;
-               editor = data.prover_editor} acc
-	  with Not_found ->
-	    begin
-              prover_tips_info := true;
-	      eprintf "Warning: found prover %s but name/version not \
+              eprintf "Warning: prover %s version %s is not known to be \
+                     supported, use it at your own risk!@." nam ver
+          end;
+        let c = make_command com data.prover_command in
+        Some {name = data.prover_name;
+              version = ver;
+              command = c;
+              driver  = Filename.concat (datadir main) data.prover_driver;
+              editor = data.prover_editor}
+      end
+    with Not_found ->
+      begin
+        prover_tips_info := true;
+	eprintf "Warning: found prover %s but name/version not \
                        recognized by regexp `%s'@."
-                data.prover_name data.version_regexp;
-	      eprintf "Answer was `%s'@." s;
-	      acc
-	    end)
-    acc0
-    data.execs
-  in
-  let acc = if Queue.length keys = 1 then
-      let key = Queue.take keys in
-      let prv = Mstr.find key acc in
-      let acc = Mstr.remove key acc in
-      Mstr.add data.prover_id prv acc
-    else
-      acc in
-  (** If the accumulator has not been touched we warn
-      that we don't find the prover *)
-  if acc == acc0 then eprintf "Prover %s not found.@." data.prover_name;
-  acc
+          data.prover_name data.version_regexp;
+	eprintf "Answer was `%s'@." s;
+	None
+      end
+
+let detect_prover main acc l =
+  let prover_id = (List.hd l).prover_id in
+  try
+    let detect_execs data =
+      try Some (Util.list_first (detect_exec main data) data.execs)
+      with Not_found -> None in
+    let prover = Util.list_first detect_execs l in
+    Mstr.add prover_id prover acc
+  with Not_found ->
+    eprintf "Prover %s not found.@." prover_id;
+    acc
 
 let run_auto_detection config =
   let main = get_main config in
   let l = read_auto_detection_data main in
+  let cmp p q = String.compare p.prover_id q.prover_id in
+  let l = Util.list_part cmp l in
   let detect = List.fold_left (detect_prover main) Mstr.empty l in
   let length = Mstr.cardinal detect in
   eprintf "%d provers detected.@." length;

src/util/rc.mll

@@ -107,7 +107,7 @@ let empty_section = Mstr.empty
 
 let make_t tl =
   let add_key acc (key,value) =
-    let l = try Mstr.find key acc with Not_found -> [] in
+    let l = Mstr.find_default key [] acc in
     Mstr.add key (value::l) acc in
   let add_section t (args,sectionl) =
     let sname,arg = match args with
@@ -117,7 +117,7 @@ let make_t tl =
       | sname::_     -> raise (ExtraParameters sname) in
     let m = List.fold_left add_key empty_section sectionl in
     let m = Mstr.map List.rev m in
-    let l = try Mstr.find sname t with Not_found -> [] in
+    let l = Mstr.find_default sname [] t in
     Mstr.add sname ((arg,m)::l) t in
   List.fold_left add_section empty tl
 

src/util/util.ml

@@ -126,6 +126,23 @@ let list_compare cmp l1 l2 = match l1,l2 with
 let list_flatten_rev fl =
   List.fold_left (fun acc l -> List.rev_append l acc) [] fl
 
+let list_part cmp l =
+  let l = List.stable_sort cmp l in
+  match l with
+    | [] -> []
+    | e::l ->
+      let rec aux acc curr last = function
+        | [] -> ((last::curr)::acc)
+        | a::l when cmp last a = 0 -> aux acc (last::curr) a l
+        | a::l -> aux ((last::curr)::acc) [] a l in
+      aux [] [] e l
+
+let rec list_first f = function
+  | [] -> raise Not_found
+  | a::l -> match f a with
+      | None -> list_first f l
+      | Some r -> r
+
 (* boolean fold accumulators *)
 
 exception FoldSkip

src/util/util.mli

@@ -95,6 +95,15 @@ val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
 
 val list_flatten_rev : 'a list list -> 'a list
 
+val list_part : ('a -> 'a -> int) -> 'a list -> 'a list list
+(** [list_part cmp l] returns the list of the congruence classes with
+    respect to [cmp]. They are returned in reverse order *)
+
+val list_first : ('a -> 'b option) -> 'a list -> 'b
+(** [list_first f l] returns the first result of the application of
+    [f] to an element of [l] which doesn't return [None]. [raise
+    Not_found] if all the element of [l] return [None] *)
+
 (* boolean fold accumulators *)
 
 exception FoldSkip