asynchronous prover calls

Makefile.in

@@ -1097,6 +1097,9 @@ src/config.ml: src/config.sh
 doc/version.tex: doc/version.tex.in config.status
 	./config.status chmod --file $@
 
+share/provers-detection-data.conf: share/provers-detection-data.conf.in config.status
+	./config.status chmod --file $@
+
 config.status: configure Version
 	./config.status --recheck
 

share/provers-detection-data.conf.in

@@ -11,7 +11,7 @@ version_ok = "0.92"
 version_ok = "0.91"
 version_old = "0.9"
 version_old = "0.8"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/alt_ergo.drv"
 
 [ATP cvc3]
@@ -21,7 +21,7 @@ version_switch = "-version"
 version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
-command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t -lang smt %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t -lang smt %f"
 driver = "drivers/cvc3.drv"
 
 [ATP yices]
@@ -32,7 +32,7 @@ version_regexp = "[Yices ]*\\([^ \n]+\\)"
 version_ok = "1.0.27"
 version_old = "1.0.17"
 version_old = "1.0.24"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt"
 driver = "drivers/yices.drv"
 
 [ATP eprover]
@@ -40,7 +40,7 @@ name = "Eprover"
 exec = "eprover"
 version_switch = "--version"
 version_regexp = "E \\([^\n]+\\)"
-command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/tptp.drv"
 
 [ATP gappa]
@@ -54,7 +54,7 @@ version_old = "0.12.2"
 version_old = "0.12.1"
 version_old = "0.12.0"
 version_old = "0.11.2"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/gappa.drv"
 
 [ATP simplify]
@@ -67,7 +67,7 @@ version_switch = "-version"
 version_regexp = "Simplify version \\([^ \n,]+\\)"
 version_ok = "1.5.5"
 version_ok = "1.5.4"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/simplify.drv"
 
 [ATP spass]
@@ -75,7 +75,7 @@ name = "Spass"
 exec = "SPASS"
 version_switch = "-TPTP || true"
 version_regexp = "SPASS V \\([^ \n\t]+\\)"
-command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
 driver = "drivers/tptp.drv"
 
 [ATP verit]
@@ -84,7 +84,7 @@ exec = "veriT"
 exec = "verit"
 version_switch = "--help"
 version_regexp = "Version: \\([^ \n\r]+\\)"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/verit.drv"
 
 [ATP z3]
@@ -96,7 +96,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
 version_old = "1.3"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f 2>&1"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
 driver = "drivers/z3.drv"
 
 [ITP coq]

src/driver/autodetection.ml

@@ -159,7 +159,6 @@ let detect_prover main acc0 data =
               {name = data.prover_name;
                version = ver;
                command = c;
-               command_split = Cmdline.cmdline_split c;
                driver  = Filename.concat (datadir main) data.prover_driver;
                editor = data.prover_editor} acc
 	  with Not_found ->

src/driver/call_provers.ml

@@ -110,54 +110,57 @@ let rec grep out l = match l with
 
 let debug = Debug.register_flag "call_prover"
 
-let call_prover command opt_cout buffer =
-  let time = Unix.gettimeofday () in
-  let (cin,_) as p = match opt_cout with
-    | Some cout ->
-        Buffer.output_buffer cout buffer; close_out cout;
-        Unix.open_process command
-    | None ->
-        let (_,cout) as p = Unix.open_process command in
-        Buffer.output_buffer cout buffer; close_out cout;
-        p
-  in
-  let out = channel_contents cin in
-  let ret = Unix.close_process p in
-  let time = Unix.gettimeofday () -. time in
-  Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
-  ret, out, time
-
 type post_prover_call = unit -> prover_result
-
-type bare_prover_call = unit -> post_prover_call
+type prover_call = Unix.wait_flag list -> post_prover_call
+type pre_prover_call = unit -> prover_call
 
 let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
                    ~regexps ~timeregexps ~exitcodes ~filename buffer =
-  let on_stdin = ref true in
+
+  let arglist = Cmdline.cmdline_split command in
+  let command = List.hd arglist in
+  let fin,cin = Filename.open_temp_file "why_" ("_" ^ filename) in
+  Buffer.output_buffer cin buffer; close_out cin;
+
   let on_timelimit = ref false in
   let cmd_regexp = Str.regexp "%\\(.\\)" in
   let replace file s = match Str.matched_group 1 s with
     | "%" -> "%"
-    | "f" -> on_stdin := false; file
+    | "f" -> file
     | "t" -> on_timelimit := true; string_of_int timelimit
     | "m" -> string_of_int memlimit
     | "b" -> string_of_int (memlimit * 1024)
     | _ -> failwith "unknown format specifier, use %%f, %%t, %%m or %%b"
   in
-  let cmd = Str.global_substitute cmd_regexp (replace "") command in
-  let on_stdin = !on_stdin in
-  let cmd,fout,cout = if on_stdin then cmd, "", None else
-    let fout,cout = Filename.open_temp_file "why_" ("_" ^ filename) in
-    let cmd =
-      try Str.global_substitute cmd_regexp (replace fout) command
-      with e -> close_out cout; Sys.remove fout; raise e
-    in
-    cmd, fout, Some cout
+  let subst s =
+    try Str.global_substitute cmd_regexp (replace fin) s
+    with e -> Sys.remove fin; raise e
   in
+  let argarray = Array.of_list (List.map subst arglist) in
+
   fun () ->
-    let ret,out,time = call_prover cmd cout buffer in
+    let fd_in = Unix.openfile fin [Unix.O_RDONLY] 0 in
+    let fout,cout = Filename.open_temp_file (Filename.basename fin) ".out" in
+    let fd_out = Unix.descr_of_out_channel cout in
+    let time = Unix.gettimeofday () in
+    let pid = Unix.create_process command argarray fd_in fd_out fd_out in
+    Unix.close fd_in;
+    close_out cout;
+
+    fun wait_flags ->
+      (* TODO? check that we haven't given the result earlier *)
+      let res,ret = Unix.waitpid wait_flags pid in
+      if res = 0 then raise Exit;
+      let time = Unix.gettimeofday () -. time in
+      let cout = open_in fout in
+      let out = Sysutil.channel_contents cout in
+      close_in cout;
+
     fun () ->
-      if not on_stdin && Debug.nottest_flag debug then Sys.remove fout;
+      if Debug.nottest_flag debug then begin
+        Sys.remove fin;
+        Sys.remove fout;
+      end;
       let ans = match ret with
         | Unix.WSTOPPED n ->
             Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
@@ -169,6 +172,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
             Debug.dprintf debug "Call_provers: exited with status %d@." n;
             (try List.assoc n exitcodes with Not_found -> grep out regexps)
       in
+      Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
       let time = Util.default_option time (grep_time out timeregexps) in
       let ans = match ans with
         | HighFailure when !on_timelimit && timelimit > 0
@@ -179,3 +183,7 @@ let call_on_buffer ~command ?(timelimit=0) ?(memlimit=0)
         pr_output = out;
         pr_time   = time }
 
+let query_call call = try Some (call [Unix.WNOHANG]) with Exit -> None
+
+let wait_on_call call = call []
+

src/driver/call_provers.mli

@@ -63,14 +63,14 @@ val timeregexp : string -> timeregexp
 (** Converts a regular expression with special markers '%h','%m',
     '%s','%i' (for milliseconds) into a value of type [timeregexp] *)
 
-type post_prover_call = unit -> prover_result
-(** Thread-unsafe closure that processes a prover's output
-    and returns the final result. Once again: this closure
-    may use internal Why structures and is therefore not
-    thread-safe. *)
+type prover_call
+(** Type that represents a single prover run *)
+
+type pre_prover_call = unit -> prover_call
+(** Thread-safe closure that launches the prover *)
 
-type bare_prover_call = unit -> post_prover_call
-(** Thread-safe closure that executes a prover on a task. *)
+type post_prover_call = unit -> prover_result
+(** Thread-unsafe closure that interprets the prover's results *)
 
 val call_on_buffer :
   command     : string ->
@@ -80,7 +80,7 @@ val call_on_buffer :
   timeregexps : timeregexp list ->
   exitcodes   : (int * prover_answer) list ->
   filename    : string ->
-  Buffer.t -> bare_prover_call
+  Buffer.t -> pre_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
 
     @param timelimit : set the available time limit (def. 0 : unlimited)
@@ -101,7 +101,13 @@ val call_on_buffer :
     the second field is the answer. Exit codes are tested in the order
     of the list and before the regexps.
 
-    @param filename : if the prover doesn't accept stdin, a temporary
-    file is used. In this case the suffix of the temporary file is
-    [filename]. *)
+    @param filename : the suffix of the proof task's file, if the prover
+    doesn't accept stdin. *)
+
+val query_call : prover_call -> post_prover_call option
+(** Thread-unsafe non-blocking function that checks if the prover
+    has finished. *)
+
+val wait_on_call : prover_call -> post_prover_call
+(** Thread-unsafe blocking function that waits until the prover finishes. *)
 

src/driver/driver.mli

@@ -41,7 +41,7 @@ val call_on_buffer :
   command    : string ->
   ?timelimit : int ->
   ?memlimit  : int ->
-  driver -> Buffer.t -> Call_provers.bare_prover_call
+  driver -> Buffer.t -> Call_provers.pre_prover_call
 
 val print_task :
   ?old       : in_channel ->
@@ -52,5 +52,5 @@ val prove_task :
   ?timelimit : int ->
   ?memlimit  : int ->
   ?old       : in_channel ->
-  driver -> Task.task -> Call_provers.bare_prover_call
+  driver -> Task.task -> Call_provers.pre_prover_call
 

src/driver/whyconf.ml

@@ -28,7 +28,7 @@ open Rc
 
 If a configuration doesn't contain the actual magic number we don't use it.*)
 
-let magicnumber = 2
+let magicnumber = 3
 
 exception WrongMagicNumber
 
@@ -51,7 +51,6 @@ type config_prover = {
   driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
   version : string;   (* "v2.95" *)
   editor  : string;
-  command_split : string list;  (* "why3-cpulimit" "%t" "%m" "alt-ergo" "%f" *)
 }
 
 type main = {
@@ -176,7 +175,6 @@ let load_prover dirname provers (id,section) =
       driver  = absolute_filename dirname (get_string section "driver");
       version = get_string ~default:"" section "version";
       editor  = get_string ~default:"" section "editor";
-      command_split = Cmdline.cmdline_split (get_string section "command");
     } provers
 
 let load_main dirname section =

src/driver/whyconf.mli

@@ -88,7 +88,6 @@ type config_prover = {
   driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
   version : string;   (* "v2.95" *)
   editor  : string;   (* Interative theorem prover *)
-  command_split : string list;  (* "why3-cpulimit" "%t" "%m" "alt-ergo" "%f" *)
 }
 
 val get_provers : config  -> config_prover Mstr.t

src/ide/gconfig.ml

@@ -151,7 +151,6 @@ let save_config t =
         driver  = pr.driver_name;
         version = pr.prover_version;
         editor  = pr.editor;
-        command_split = Cmdline.cmdline_split pr.command;
       } acc in
   let config = t.config in
   let config = set_main config

src/ide/scheduler.ml

@@ -206,7 +206,10 @@ let new_external_proof =
               Format.eprintf "Task for prover: %a@."
               (Driver.print_task driver) goal;
             *)
-      Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
+      let pre_call =
+        Driver.prove_task ?old ~command ~timelimit ~memlimit driver goal
+      in
+      fun () -> Call_provers.wait_on_call (pre_call ())
     in
     ManyWorkers.add_work external_workers (call_prover,callback);
   with

src/main.ml

@@ -348,9 +348,8 @@ let fname_printer = ref (Ident.create_ident_printer [])
 let do_task drv fname tname (th : Why.Theory.theory) (task : Task.task) =
   match !opt_output, !opt_command with
     | None, Some command ->
-        let res =
-          Driver.prove_task ~command ~timelimit ~memlimit drv task () ()
-        in
+        let call = Driver.prove_task ~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

src/util/cmdline.ml

@@ -91,6 +91,7 @@ let cmdline_split s =
     | Normal ->
         assert false
     | Blank ->
+        if !argv = [] then raise EmptyCommandLine else
         List.rev !argv
     | Quote ->
         raise (UnclosedQuote s)