Make `-async-proofs on` effective with `coqc`

Before this patch, it had no effect.

3 files changed, 9 insertions, 4 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 0969eb0918..3ae6b3a03e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2643,13 +2643,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
      name by looking at the load path! *)
   List.iter Mltop.add_coq_path iload_path;
 
+  Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
+
   begin match doc_type with
     | Interactive ln ->
       let dp = match ln with
         | TopLogical dp -> dp
         | TopPhysical f -> dirpath_of_file f
       in
-      Safe_typing.allow_delayed_constants := true;
       Declaremods.start_library dp
 
     | VoDoc f ->
@@ -2660,7 +2661,6 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
       set_compilation_hints f
 
     | VioDoc f ->
-      Safe_typing.allow_delayed_constants := true;
       let ldir = dirpath_of_file f in
       check_coq_overwriting ldir;
       let () = Flags.verbosely Declaremods.start_library ldir in
diff --git a/stm/stm.mli b/stm/stm.mli
index 4db83a7359..b6071fa56b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -16,7 +16,9 @@ open Names
 module AsyncOpts : sig
 
   type cache = Force
-  type async_proofs = APoff | APonLazy | APon
+  type async_proofs = APoff
+                    | APonLazy (* Delays proof checking, but does it in master *)
+                    | APon
   type tac_error_filter = [ `None | `Only of string list | `All ]
 
   type stm_opt = {
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index fb6d07d6cf..b248b87880 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -119,7 +119,8 @@ let compile opts ~echo ~f_in ~f_out =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in
+      let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
+      let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -148,6 +149,8 @@ let compile opts ~echo ~f_in ~f_out =
          document anyways. *)
       let stm_options = let open Stm.AsyncOpts in
         { stm_options with
+          async_proofs_mode = APon;
+          async_proofs_n_workers = 0;
           async_proofs_cmd_error_resilience = false;
           async_proofs_tac_error_resilience = `None;
         } in