STM: check with the kernel proof terms on the worker too

Before this commit the worker was sending back a proof term
as built by tactics.  The master receives the proof terms and
eventually (when one clicks on the gears in CoqIDE) check it
with the kernel.  This meant that errors like the ones produced
by the "fix" tactics were discovered very late.

Now a worker checks with its kernel the proof term before sending it
back.  The term is also checked by the master, eventually, but the
error is signaled early.

1 files changed, 22 insertions, 7 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 6558252a7..fe5d43ff4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1013,12 +1013,26 @@ end = struct (* {{{ *)
     try
       VCS.restore document;
       VCS.print ();
-      let rc, time =
+      let proof, future_proof, time =
         let wall_clock = Unix.gettimeofday () in
-        let l = Future.force (build_proof_here exn_info loc stop) in
-        l, Unix.gettimeofday () -. wall_clock in
-      VCS.print ();
-      RespBuiltProof(rc,time)
+        let fp = build_proof_here exn_info loc stop in
+        let proof = Future.force fp in
+        proof, fp, Unix.gettimeofday () -. wall_clock in
+      (* We typecheck the proof with the kernel (in the worker) to spot
+       * the few errors tactics don't catch, like the "fix" tactic building
+       * a bad fixpoint *)
+      let fix_exn = Future.fix_exn_of future_proof in
+      let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+        let pobject, _ =
+          Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+        let terminator = (* The one sent by master is an InvalidKey *)
+          Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+        vernac_interp stop
+          ~proof:(pobject, terminator)
+          { verbose = false; loc;
+            expr = (VernacEndProof (Proved (true,None))) }) in
+      ignore(Future.join checked_proof);
+      RespBuiltProof(proof,time)
     with
     | e when Errors.noncritical e ->
         let (e, info) = Errors.push e in
@@ -1027,10 +1041,11 @@ end = struct (* {{{ *)
         let e_error_at, e_safe_id = match Stateid.get info with
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
+        let e_msg = iprint (e, info) in
         prerr_endline "failed with the following exception:";
-        prerr_endline (string_of_ppcmds (print e));
+        prerr_endline (string_of_ppcmds e_msg);
         let e_safe_states = List.filter State.is_cached my_states in
-        RespError { e_error_at; e_safe_id; e_msg = iprint (e, info); e_safe_states }
+        RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
   
   let perform_states query =
     assert(query <> []);