Merge PR #9072: Clean stm flags

4 files changed, 23 insertions, 28 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index a74a67c935..c078dbae56 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -44,7 +44,6 @@ module AsyncOpts = struct
     async_proofs_mode : async_proofs;
 
     async_proofs_private_flags : string option;
-    async_proofs_full : bool;
     async_proofs_never_reopen_branch : bool;
 
     async_proofs_tac_error_resilience : tac_error_filter;
@@ -61,7 +60,6 @@ module AsyncOpts = struct
     async_proofs_mode = APoff;
 
     async_proofs_private_flags = None;
-    async_proofs_full = false;
     async_proofs_never_reopen_branch = false;
 
     async_proofs_tac_error_resilience = `Only [ "curly" ];
@@ -1442,11 +1440,14 @@ end = struct (* {{{ *)
   let perspective = ref []
   let set_perspective l = perspective := l
 
+  let is_inside_perspective st = true
+    (* This code is now disabled. If an IDE needs this feature, make it accessible again.
+    List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st
+    *)
+
   let task_match age t =
     match age, t with
-    | Fresh, BuildProof { t_states } ->
-        not !cur_opt.async_proofs_full ||
-        List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states
+    | Fresh, BuildProof { t_states } -> is_inside_perspective t_states
     | Old my_states, States l ->
         List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
     | _ -> false
@@ -1482,8 +1483,7 @@ end = struct (* {{{ *)
         feedback (InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time ?loc:t_loc t_name time;
-        if !cur_opt.async_proofs_full || t_drop
-        then `Stay(t_states,[States t_states])
+        if t_drop then `Stay(t_states,[States t_states])
         else `End
     | Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
@@ -2126,8 +2126,7 @@ end = struct (* {{{ *)
     TaskQueue.enqueue_task (Option.get !queue)
       QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
 
-  let init () = queue := Some (TaskQueue.create
-    (if !cur_opt.async_proofs_full then 1 else 0))
+  let init () = queue := Some (TaskQueue.create 0)
 
 end (* }}} *)
 
@@ -2150,7 +2149,6 @@ let async_policy () =
 let delegate name =
      get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold
   || VCS.is_vio_doc ()
-  || !cur_opt.async_proofs_full
 
 let collect_proof keep cur hd brkind id =
  stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
@@ -2257,8 +2255,7 @@ let collect_proof keep cur hd brkind id =
      else
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
-       else if (is_vtkeep keep) &&
-          (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full)
+       else if (is_vtkeep keep) && (not(State.is_cached_and_valid id))
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -2646,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 ->
@@ -2663,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
@@ -2869,11 +2866,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       | VtQuery, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue =
-            if !cur_opt.async_proofs_full then `QueryQueue (ref false)
-            else if VCS.is_vio_doc () &&
-                    VCS.((get_branch head).kind = `Master) &&
-                    may_pierce_opaque (Vernacprop.under_control x.expr)
-                 then `SkipQueue
+            if VCS.is_vio_doc () &&
+               VCS.((get_branch head).kind = `Master) &&
+               may_pierce_opaque (Vernacprop.under_control x.expr)
+            then `SkipQueue
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
           Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
@@ -3206,8 +3202,7 @@ let edit_at ~doc id =
     VCS.delete_boxes_of id;
     VCS.gc ();
     VCS.print ();
-    if not !cur_opt.async_proofs_full then
-      Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
+    Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 0c0e19ce5c..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 = {
@@ -27,7 +29,6 @@ module AsyncOpts : sig
     async_proofs_mode : async_proofs;
 
     async_proofs_private_flags : string option;
-    async_proofs_full : bool;
     async_proofs_never_reopen_branch : bool;
 
     async_proofs_tac_error_resilience : tac_error_filter;
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
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 2f84eb9851..b98535b201 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -543,10 +543,6 @@ let parse_args arglist : coq_cmdopts * string list =
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
-    |"-async-proofs-full" ->
-      { oval with stm_flags = { oval.stm_flags with
-        Stm.AsyncOpts.async_proofs_full = true;
-      }}
     |"-async-proofs-never-reopen-branch" ->
       { oval with stm_flags = { oval.stm_flags with
         Stm.AsyncOpts.async_proofs_never_reopen_branch = true