STM: make -async-proofs on work from coqc too

4 files changed, 7 insertions, 15 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 2b917587c..bb623b7a1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -874,8 +874,8 @@ let start_library dir =
   Lib.add_frozen_state ()
 
 let end_library dir =
-  let prefix, lib_stack = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export dir in
+  let prefix, lib_stack = Lib.end_compilation dir in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
diff --git a/library/library.ml b/library/library.ml
index b75329a22..fd391344c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -373,8 +373,6 @@ module OpaqueTables = struct
  module FMap = Map.Make(Future.UUID)
  let f2t = ref FMap.empty
 
- let get_opaque_nolib _ i = (!local_opaque_table).(i)
-
  let get_opaque dp i =
    if DirPath.equal dp (Lib.library_dp ())
    then (!local_opaque_table).(i)
@@ -382,13 +380,11 @@ module OpaqueTables = struct
  
  let join_local_opaque dp i =
    if DirPath.equal dp (Lib.library_dp ()) then
-    Future.sink (!local_opaque_table).(i)
+    ignore(Future.force (!local_opaque_table).(i))
 
  let join_local_univ dp i =
    if DirPath.equal dp (Lib.library_dp ()) then
-    Future.sink (!local_univ_table).(i)
-
- let get_univ_nolib _ i = Some (!local_univ_table).(i)
+    ignore(Future.join (!local_univ_table).(i))
 
  let get_univ dp i =
    if DirPath.equal dp (Lib.library_dp ())
@@ -410,8 +406,8 @@ module OpaqueTables = struct
     local_discharge_table := t
   end;
   let c, u = Future.split2 ~greedy:true cu in
-  if Future.is_val u then ignore(Future.join u);
-  if Future.is_val c then ignore(Future.join c);
+  Future.sink u;
+  Future.sink c;
   (!local_opaque_table).(n) <- c;
   (!local_univ_table).(n) <- u;
   (!local_discharge_table).(n) <- d;
@@ -737,11 +733,6 @@ let save_library_to ?todo dir f =
         f ^ "i", (fun x -> Some (d x)),
           (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in
   Opaqueproof.reset_indirect_creator ();
-  (* HACK: end_library resets Lib and then joins the safe env.  To join the
-   * env one needs to access the futures stored in the tables.  Standard
-   * accessors use Lib.  Hence *)
-  Opaqueproof.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
-  Opaqueproof.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
   let cenv, seg, ast = Declaremods.end_library dir in
   let opaque_table, univ_table, disch_table, f2t_map =
     OpaqueTables.dump () in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 1f127b4a0..84bfaaa70 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1144,7 +1144,7 @@ let delegate_policy_check time =
     (!Flags.async_proofs_mode = Flags.APonParallel 0 ||
     !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0
   else if !Flags.compilation_mode = Flags.BuildVi then true
-  else !Flags.async_proofs_mode <> Flags.APoff
+  else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0
 
 let collect_proof cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 27509fcc0..e887204c3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -318,6 +318,7 @@ let compile verbosely f =
   match !Flags.compilation_mode with
   | BuildVo ->
       let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      Stm.set_compilation_hints long_f_dot_v;
       Aux_file.start_aux_file_for long_f_dot_v;
       Dumpglob.start_dump_glob long_f_dot_v;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");