auto-detected provers

prover-detection-data.conf

@@ -18,7 +18,7 @@ version_old = "2.1"
 
 [ATP gappa]
 name = "Gappa"
-command = "gappa";
+command = "gappa"
 version_switch = "--version"
 version_regexp = "Gappa \\([^ ]*\\)"
 version_ok = "0.13.0"
@@ -45,20 +45,20 @@ command = "z3"
 command = "z3-2.2"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \r]+\\)"
-version_ok = 2.2
-version_old = 2.1
-version_old = 1.3
+version_ok = "2.2"
+version_old = "2.1"
+version_old = "1.3"
 
 [ITP coq]
 name = "Coq"
 command = "coqc"
-version_switch = "-v";
-version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)";
+version_switch = "-v"
+version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)"
 version_ok = "8.0"
 version_ok = "8.1"
 version_ok = "8.2"
 version_ok = "8.2pl1"
-version_old = "7.4";
+version_old = "7.4"
 
 
 

src/ide/gconfig.ml

@@ -2,6 +2,14 @@
 open Format
 open Why
 
+type prover_data =
+    { prover_id : string;
+      prover_name : string;
+      prover_version : string;
+      command : string;
+      driver : Why.Driver.driver;
+    }
+
 type t = 
     { mutable window_width : int;
       mutable window_height : int;
@@ -9,6 +17,7 @@ type t =
       mutable task_height : int;
       mutable time_limit : int;
       mutable max_running_processes : int;
+      mutable provers : prover_data list;
     }
 
 let default = 
@@ -18,10 +27,17 @@ let default =
     task_height = 384;
     time_limit = 2;
     max_running_processes = 2;
+    provers = [];
   }
 
 let conf_file = Filename.concat (Rc.get_home_dir ()) ".whyide.conf"
 
+let save_prover fmt p =
+  fprintf fmt "[prover]@\n";
+  fprintf fmt "id = \"%s\"@\n" p.prover_id;
+  fprintf fmt "version = \"%s\"@\n" p.prover_version;
+  fprintf fmt "@."
+
 let save_config config =
   let ch = open_out conf_file in
   let fmt = formatter_of_out_channel ch in
@@ -33,6 +49,7 @@ let save_config config =
   fprintf fmt "time_limit = %d@\n" config.time_limit;
   fprintf fmt "max_processes = %d@\n" config.max_running_processes;
   fprintf fmt "@.";
+  List.iter (save_prover fmt) config.provers; 
   close_out ch
 
 let load_main c (key, value) = 
@@ -45,20 +62,45 @@ let load_main c (key, value) =
     | "max_processes" -> c.max_running_processes <- Rc.int value
     | s -> 
         eprintf "Warning: ignore unknown key [%s] in whyide config file@." s
+
+
+
+let get_prover_data env config id ver = 
+  let pi = Util.Mstr.find id config.Whyconf.provers in
+  let d = Why.Driver.load_driver env pi.Whyconf.driver in
+  { prover_id = id ;
+    prover_name = pi.Whyconf.name;
+    prover_version = ver;
+    command = pi.Whyconf.command;
+    driver = d; 
+  }
+
+let load_prover env whyconfig l =
+  let id = ref "?" in
+  let v = ref "?" in
+  List.iter
+    (fun (key, value) -> 
+	match key with
+	  | "id" -> id := Rc.string value
+	  | "version" -> v := Rc.string value
+	  | s -> 
+            eprintf "Warning: ignore unknown key [%s] in prover data of whyide config file@." s)
+    l;
+  get_prover_data env whyconfig !id !v
         
-let load c (key, al) = 
+let load env whyconfig c (key, al) = 
   match key with
-    | "main" :: _ ->
-        List.iter (load_main c) al
+    | "main" :: _ -> List.iter (load_main c) al
+    | "prover" :: _ -> c.provers <- load_prover env whyconfig al :: c.provers
     | s :: _ -> 
         eprintf "Warning: ignored unknown section [%s] in whyide config file@." s
     | [] -> assert false
         
-let read_config () =
+let read_config env whyconfig =
   try
     let rc = Rc.from_file conf_file in
     let c = default in
-    List.iter (load c) rc;
+    List.iter (load env whyconfig c) rc;
     c
   with
     | Failure "lexing" -> 
@@ -311,7 +353,70 @@ let read_auto_detection_data () =
         exit 2
     
 
+let provers_found = ref 0
 
+let prover_tips_info = ref false
+
+
+let detect_prover env whyconfig acc data =
+  List.fold_left
+    (fun acc com ->
+	let out = Filename.temp_file "out" "" in
+        let cmd = com ^ " " ^ data.version_switch in
+	let c = cmd ^ " > " ^ out in
+	let ret = Sys.command c in
+	if ret <> 0 then
+	  begin
+	    eprintf "command '%s' failed@." cmd;
+	    acc
+	  end
+	else
+	  let s = 
+            try 
+              let ch = open_in out in
+              let s = ref (input_line ch) in
+              while !s = "" do s := input_line ch done;
+              close_in ch;
+	      Sys.remove out;
+              !s              
+            with Not_found | End_of_file  -> ""
+          in
+	  let re = Str.regexp data.version_regexp in
+	  if Str.string_match re s 0 then            
+	    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
+            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;
+	    get_prover_data env whyconfig data.prover_id ver :: acc
+	  else 
+	    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;
+(*
+	      p.command <- cmd;
+	      p.version <- "?";
+*)
+	      acc
+	    end)
+    acc
+    data.commands
+
+
+let run_auto_detection env whyconfig gconfig =
+  let l = read_auto_detection_data () in
+  let detect = List.fold_left (detect_prover env whyconfig) [] l in
+  gconfig.provers <- detect
+    
 
 (*
 Local Variables: 

src/ide/gconfig.mli

 
+open Why
+
+type prover_data =
+    { prover_id : string;
+      prover_name : string;
+      prover_version : string;
+      command : string;
+      driver : Driver.driver;
+    }
 
 type t = 
     { mutable window_width : int;
@@ -7,9 +16,10 @@ type t =
       mutable task_height : int;
       mutable time_limit : int;
       mutable max_running_processes : int;
+      mutable provers : prover_data list;
     }
 
-val read_config : unit -> t
+val read_config : Env.env -> Whyconf.config -> t
 
 val save_config : t -> unit
 
@@ -41,6 +51,8 @@ val show_legend_window : unit -> unit
 val show_about_window : unit -> unit
 val preferences : t -> unit
 
+val run_auto_detection : Env.env -> Whyconf.config -> t -> unit
+
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C ../.. bin/whyide.opt"

src/ide/gmain.ml

@@ -52,14 +52,6 @@ let timelimit =
 *)
 
 
-(********************************)
-(* loading WhyIDE configuration *)
-(********************************)
-
-let gconfig = 
-  eprintf "%s reading IDE config file@." pname;
-  read_config ()
-
 (***************************)
 (* parsing comand_line *)
 (***************************)
@@ -116,6 +108,15 @@ let source_text =
 
 let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
 
+(********************************)
+(* loading WhyIDE configuration *)
+(********************************)
+
+let gconfig = 
+  eprintf "%s reading IDE config file@." pname;
+  read_config env config
+
+
 
 (***********************)
 (* Parsing input file  *)
@@ -140,45 +141,26 @@ let theories : Theory.theory Theory.Mnm.t =
 let () = Db.init_base (fname ^ ".db")
 *)
 
-let get_driver name = 
-  let pi = Util.Mstr.find name config.provers in
-  Why.Driver.load_driver env pi.Whyconf.driver
-
-type prover_data =
-    { prover : string (* Db.prover *);
-      command : string;
-      driver : Why.Driver.driver;
-    }
-
-let provers_data =
-  printf "===============================@\nProvers: ";
-  let l = 
-    Util.Mstr.fold
-    (fun id conf acc ->
-       let name = conf.Whyconf.name in
-       printf " %s, " name;
-       { prover = (* Db.get_prover *) name;
-         command = conf.Whyconf.command;
-         driver = get_driver id; } :: acc
-    ) config.provers []
-  in
-  printf "@\n===============================@.";
-  l 
 
-let find_prover s =
+(*
+let find_prover s = 
   match
     List.fold_left
       (fun acc p ->
-         if (* Db.prover_name *) p.prover = s then Some p else acc)
-      None provers_data
+        if (* Db.prover_name *) p.prover_id = s then Some p else acc)
+      None gconfig.provers
   with
-    | None -> assert false
+    | None -> 
+      eprintf "prover id '%s' not found in Why config file@." s;
+      raise Not_found
     | Some p -> p
+*)
 
-let alt_ergo = find_prover "Alt-Ergo"
+(*
+let alt_ergo = find_prover "alt-ergo"
 let simplify = find_prover "simplify"
 let z3 = find_prover "Z3"
-
+*)
 
    
 (*
@@ -463,10 +445,10 @@ let () =
 
 let rec prover_on_goal p g =
   let row = g.Model.goal_row in
-  let name = p.prover in
+  let name = p.prover_name in
   let prover_row = goals_model#append ~parent:row () in
   goals_model#set ~row:prover_row ~column:Model.icon_column !image_prover;
-  goals_model#set ~row:prover_row ~column:Model.name_column ("prover: " ^name);
+  goals_model#set ~row:prover_row ~column:Model.name_column (name ^ " " ^ p.prover_version);
   goals_model#set ~row:prover_row ~column:Model.visible_column true;
   goals_view#expand_row (goals_model#get_path row);
   let callback result time =
@@ -480,7 +462,7 @@ let rec prover_on_goal p g =
   callback Scheduler.Scheduled 0.0;
   Scheduler.schedule_proof_attempt
     ~debug:false ~timelimit:gconfig.time_limit ~memlimit:0 
-    ~prover:p.prover ~command:p.command ~driver:p.driver 
+    ~prover:p.prover_id ~command:p.command ~driver:p.driver 
     ~callback
     g.Model.task;
   List.iter
@@ -572,6 +554,11 @@ let (_ : GMenu.image_menu_item) =
        Scheduler.maximum_running_proofs := gconfig.max_running_processes)
     () 
 
+let (_ : GMenu.image_menu_item) = 
+  file_factory#add_image_item ~label:"_Detect provers" ~callback:
+    (fun () -> Gconfig.run_auto_detection env config gconfig)
+    () 
+
 let (_ : GMenu.image_menu_item) = 
   file_factory#add_image_item ~key:GdkKeysyms._Q ~label:"_Quit" 
     ~callback:exit_function () 
@@ -681,11 +668,16 @@ let (_ : GMenu.check_menu_item) = view_factory#add_check_item
 let tools_menu = factory#add_submenu "_Tools" 
 let tools_factory = new GMenu.factory tools_menu ~accel_group 
 
-let (_ : GMenu.image_menu_item) = 
-  tools_factory#add_image_item ~key:GdkKeysyms._S
-    ~label:"Simplify on unproved goals" 
-    ~callback:(fun () -> prover_on_unproved_goals simplify ()) 
-    () 
+let () =
+  List.iter (fun p ->
+    let (_ : GMenu.image_menu_item) = 
+      let n = p.prover_name ^ " " ^ p.prover_version in
+      tools_factory#add_image_item ~label:(n ^ " on unproved goals") 
+	~callback:(fun () -> prover_on_unproved_goals p ()) 
+	()
+    in ()) gconfig.provers 
+
+(*
 
 let (_ : GMenu.image_menu_item) = 
   tools_factory#add_image_item ~key:GdkKeysyms._A 
@@ -698,7 +690,7 @@ let (_ : GMenu.image_menu_item) =
     ~label:"Z3 on unproved goals" 
     ~callback:(fun () -> prover_on_unproved_goals z3 ()) 
     () 
-  
+*)
 let (_ : GMenu.image_menu_item) = 
   tools_factory#add_image_item 
     ~label:"Split unproved goals"