STM: use sec vars in aux file if no Proof using when building .vi

If a proof has no "Proof using" but we are building a .vi and
the aux file contains such piece of info, we use it to process
the proof asynchronously.

3 files changed, 23 insertions, 0 deletions

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index f800b49fb9..f5cc9a8565 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1055,6 +1055,14 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
+let hints = ref Aux_file.empty_aux_file
+let set_compilation_hints h = hints := h
+let get_hint_ctx loc =
+  let s = Aux_file.get !hints loc "context_used" in
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.ghost, id) ids in
+  ids
+
 (* Runs all transactions needed to reach a state *)
 module Reach : sig
 
@@ -1089,6 +1097,17 @@ let collect_proof cur hd id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
         else `Sync `TooShort
+    | Some (parent, ({ expr = VernacProof(t,None)} as v)),
+      `Fork (_, hd', GuaranteesOpacity, ids) when
+       not (State.is_cached parent) &&
+       !Flags.compilation_mode = Flags.BuildVi ->
+        (try
+          let hint = get_hint_ctx loc in
+          assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
+          v.expr <- VernacProof(t, Some hint);
+          if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
+          else `Sync `TooShort
+        with Not_found -> `Sync `NoHint)
     | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `MaybeASync (parent, accn, ids)
@@ -1111,6 +1130,7 @@ let string_of_reason = function
   | `NestedProof -> "NestedProof"
   | `Immediate -> "Immediate"
   | `Alias -> "Alias"
+  | `NoHint -> "NoHint"
   | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
   | _ -> "Unknown Reason"
 
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index d821a2536a..4949845b58 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -52,6 +52,8 @@ val init : unit -> unit
 val slave_main_loop : unit -> unit
 val slave_init_stdout : unit -> unit
 
+val set_compilation_hints : Aux_file.aux_file -> unit
+
 (** read-eval-print loop compatible interface ****************************** **)
 
 (* Adds a new line to the document.  It replaces the core of Vernac.interp.
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 27735d2d9a..789f6bebb2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -365,6 +365,7 @@ let compile verbosely f =
   | BuildVi ->
       let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
       Dumpglob.noglob ();
+      Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();