internal: handle CTRL+C properly w.r.t. Why3 server

For that purpose, we now start Why3 manually and connect to it
as if it were an external Why3 server instance.

The Why3 server is put in its own process groups and does not receive
the signals (SIGINT, SIGTERM e.g.) directly received by EasyCrypt.

The Why3 server is started s.t. it shutdowns itself gracefully
when EasyCrypt disconnects from it.

src/dune

@@ -12,6 +12,7 @@
 (library 
  (name ecLib)
  (public_name easycrypt.ecLib)
+ (foreign_stubs (language c) (names eunix))
  (modules :standard \ ec)
  (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith)
 )

src/ecProvers.ml

@@ -421,64 +421,128 @@ let dft_prover_names = ["Z3"; "CVC4"; "Alt-Ergo"; "Eprover"; "Yices"]
 (* -------------------------------------------------------------------- *)
 type notify = EcGState.loglevel -> string Lazy.t -> unit
 
+(* -------------------------------------------------------------------- *)
+let maybe_start_why3_server_ (pi : prover_infos) =
+  if not (Prove_client.is_connected ()) then begin
+    let sockname = Filename.temp_file "easycrypt.why3server." ".socket" in
+    let exec = Filename.concat (Whyconf.libdir (Config.main ())) "why3server" in
+    let pid = ref (-1) in
+
+    begin
+      let rd, wr = Unix.pipe ~cloexec:true () in
+
+      EcUtils.try_finally (fun () ->
+        pid := Unix.fork ();
+
+        if !pid = 0 then begin
+          Unix.close rd;
+          EUnix.setpgid 0 0;
+          Unix.chdir (Filename.get_temp_dir_name ());
+          Unix.execvp exec [|
+            exec; "--socket"; sockname; "--single-client";
+            "-j"; string_of_int pi.pr_maxprocs
+          |]
+        end else begin
+          Unix.close wr;
+          ignore (Unix.select [rd] [] [] (-1.0))
+        end)
+      (fun () ->
+        (try Unix.close rd with Unix.Unix_error _ -> ());
+        (try Unix.close wr with Unix.Unix_error _ -> ()))
+    end;
+
+    let connected = ref false in
+
+    EcUtils.try_finally (fun () ->
+      let n, d = ref 5, ref 0.1 in
+
+      while 0 < !n && not !connected do
+        if Sys.file_exists sockname then begin
+          try
+            Prove_client.connect_external sockname;
+            connected := true
+          with Prove_client.ConnectionError _ -> ()
+        end;
+        if not !connected then begin
+          ignore (Unix.select [] [] [] !d);
+          n := !n - 1;
+          d := 2.0 *. !d
+        end
+      done)
+
+    (fun () ->
+      if not !connected then begin
+        try
+          Unix.kill !pid Sys.sigkill
+        with Unix.Unix_error _ -> ()
+      end);
+
+    if not !connected then
+      raise (Prove_client.ConnectionError "cannot start & connect to why3server")
+  end
+
+(* -------------------------------------------------------------------- *)
+
+let maybe_start_why3_server (pi : prover_infos) =
+  let sigdef = Sys.signal Sys.sigint Sys.Signal_ignore in
+
+  EcUtils.try_finally
+    (fun () -> maybe_start_why3_server_ pi)
+    (fun () -> ignore (Sys.signal Sys.sigint sigdef : Sys.signal_behavior))
+
+(* -------------------------------------------------------------------- *)
 let run_prover
   ?(notify : notify option) (pi : prover_infos) (prover : string) task
 =
-(*  let sigdef = Sys.signal Sys.sigint Sys.Signal_ignore in*)
-
-  EcUtils.try_finally (fun () ->
-    try
-      let { pr_config = pr; pr_driver = dr; } = get_prover prover in
+  maybe_start_why3_server pi;
 
-      let pc =
-        let command = pr.Whyconf.command in
-
-        let limit = { Call_provers.empty_limit with
-          Call_provers.limit_time =
-            let limit = pi.pr_timelimit * pi.pr_cpufactor in
-            if limit <= 0 then 0. else float_of_int limit;
-        } in
+  try
+    let { pr_config = pr; pr_driver = dr; } = get_prover prover in
 
-        let rec doit gcdone =
-          try
-            Driver.prove_task
-              ~config:(Config.main ())
-              ~command ~limit dr task
-          with Unix.Unix_error (Unix.ENOMEM, "fork", _) when not gcdone ->
-            Gc.compact (); doit true
-        in
-
-        if EcUtils.is_some (Os.getenv "EC_SMT_DEBUG") then begin
-          let stream = open_out (Printf.sprintf "%s.smt" prover) in
-          let fmt = Format.formatter_of_out_channel stream in
-          EcUtils.try_finally
-            (fun () -> Format.fprintf fmt "%a@." (Driver.print_task dr) task)
-            (fun () -> close_out stream)
-        end;
+    let pc =
+      let command = pr.Whyconf.command in
 
-        doit false
+      let limit = { Call_provers.empty_limit with
+        Call_provers.limit_time =
+          let limit = pi.pr_timelimit * pi.pr_cpufactor in
+          if limit <= 0 then 0. else float_of_int limit;
+      } in
 
+      let rec doit gcdone =
+        try
+          Driver.prove_task
+            ~config:(Config.main ())
+            ~command ~limit dr task
+        with Unix.Unix_error (Unix.ENOMEM, "fork", _) when not gcdone ->
+          Gc.compact (); doit true
       in
-        Some (prover, pc)
 
-    with e ->
-      notify |> oiter (fun notify -> notify `Warning (lazy (
-        let buf = Buffer.create 0 in
-        let fmt = Format.formatter_of_buffer buf in
-        Format.fprintf fmt "error when starting `%s': %a%!"
-          prover EcPException.exn_printer e;
-        Buffer.contents buf)));
-      None)
+      if EcUtils.is_some (Os.getenv "EC_SMT_DEBUG") then begin
+        let stream = open_out (Printf.sprintf "%s.smt" prover) in
+        let fmt = Format.formatter_of_out_channel stream in
+        EcUtils.try_finally
+          (fun () -> Format.fprintf fmt "%a@." (Driver.print_task dr) task)
+          (fun () -> close_out stream)
+      end;
+
+      doit false
 
-  (fun () -> ()) (*
-     let _ : Sys.signal_behavior = Sys.signal Sys.sigint sigdef in ()) *)
+    in
+      Some (prover, pc)
+
+  with e ->
+    notify |> oiter (fun notify -> notify `Warning (lazy (
+      let buf = Buffer.create 0 in
+      let fmt = Format.formatter_of_buffer buf in
+      Format.fprintf fmt "error when starting `%s': %a%!"
+        prover EcPException.exn_printer e;
+      Buffer.contents buf)));
+    None
 
 (* -------------------------------------------------------------------- *)
 let execute_task ?(notify : notify option) (pi : prover_infos) task =
   let module CP = Call_provers in
 
-  Prove_client.set_max_running_provers pi.pr_maxprocs;
-
   let pcs = Array.make pi.pr_maxprocs None in
 
   (* Run process, ignoring prover failing to start *)

src/system/EUnix.ml

@@ -0,0 +1,2 @@
+(* -------------------------------------------------------------------- *)
+external setpgid : int -> int -> unit = "caml_eunix_setpgid"

src/system/EUnix.mli

@@ -0,0 +1,3 @@
+
+(* -------------------------------------------------------------------- *)
+val setpgid : int -> int -> unit

src/system/eunix.c

@@ -0,0 +1,14 @@
+/* -------------------------------------------------------------------- */
+#include <caml/mlvalues.h>
+#include <caml/memory.h>
+#include <caml/unixsupport.h>
+
+#include <unistd.h>
+
+/* -------------------------------------------------------------------- */
+CAMLprim value caml_eunix_setpgid(value pid, value pgid) {
+  CAMLparam2(pid, pgid);
+  if (setpgid(Int_val(pid), Int_val(pgid)) != 0)
+    uerror("setpgid", Nothing);
+  CAMLreturn(Val_unit);
+}