Merge PR #13088: [stm] move par: to comTactic

Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego

18 files changed, 387 insertions, 307 deletions

diff --git a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
new file mode 100644
index 0000000000..4108a1aed1
--- /dev/null
+++ b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13088" ] || [ "$CI_BRANCH" = "par-to-tactic" ]; then
+
+    mtac2_CI_REF=par-to-tactic
+    mtac2_CI_GITURL=https://github.com/gares/Mtac2
+
+fi
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index be0d71ad46..6cf5d30a95 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram
 open Stdarg
 open Tacarg
 open Vernacextend
-open Goptions
 open Libnames
 
-let print_info_trace =
-  declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
-
-let vernac_solve ~pstate n info tcom b =
-  let open Goal_select in
-  let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
-      let with_end_tac = if b then Some etac else None in
-      let global = match n with SelectAll | SelectList _ -> true | _ -> false in
-      let info = Option.append info (print_info_trace ()) in
-      let (p,status) =
-        Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
-      in
-      (* in case a strict subtree was completed,
-         go back to the top of the prooftree *)
-      let p = Proof.maximal_unfocus Vernacentries.command_focus p in
-      p,status) pstate in
-  if not status then Feedback.feedback Feedback.AddedAxiom;
-  pstate
-
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
 }
@@ -409,34 +389,34 @@ END
 
 {
 
-let is_anonymous_abstract = function
-  | TacAbstract (_,None) -> true
-  | TacSolve [TacAbstract (_,None)] -> true
-  | _ -> false
 let rm_abstract = function
-  | TacAbstract (t,_) -> t
-  | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
-  | x -> x
+  | TacAbstract (t,_) -> t, true
+  | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true
+  | x -> x, false
 let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
 }
 
 VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
-    vernac_solve g n t def
+    let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
+    let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+    ComTactic.solve g ~info t ~with_end_tac
   }
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+END
+
+VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
+| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
     {
-      let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
-      let parallel = `Yes (solving_tac,anon_abstracting_tac) in
       let pbr = if solving_tac then Some "par" else None in
-      VtProofStep{ parallel = parallel; proof_block_detection = pbr }
+      VtProofStep{ proof_block_detection = pbr }
     } -> {
-      let t = rm_abstract t in
-      vernac_solve Goal_select.SelectAll n t def
+      let t, abstract = rm_abstract t in
+      let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+      ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
     }
 END
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff6a36a049..eaeae50254 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1996,16 +1996,20 @@ let interp_tac_gen lfun avoid_ids debug t =
 
 let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
 
+(* MUST be marshallable! *)
+type tactic_expr = {
+  global: bool;
+  ast:  Tacexpr.raw_tactic_expr;
+}
+
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 (* [global] means that [t] should be internalized outside of goals. *)
-let hide_interp global t ot =
+let hide_interp {global;ast} =
   let hide_interp env =
     let ist = Genintern.empty_glob_sign env in
-    let te = intern_pure_tactic ist t in
+    let te = intern_pure_tactic ist ast in
     let t = eval_tactic te in
-    match ot with
-    | None -> t
-    | Some t' -> Tacticals.New.tclTHEN t t'
+    t
   in
   if global then
     Proofview.tclENV >>= fun env ->
@@ -2015,6 +2019,8 @@ let hide_interp global t ot =
       hide_interp (Proofview.Goal.env gl)
     end
 
+let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+
 (***************************************************************************)
 (** Register standard arguments *)
 
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index cbb17bf0fa..01d7306c9d 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
 val interp : raw_tactic_expr -> unit Proofview.tactic
 
 (** Hides interpretation for pretty-print *)
+type tactic_expr = {
+  global: bool;
+  ast:  Tacexpr.raw_tactic_expr;
+}
 
-val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+val hide_interp : tactic_expr ComTactic.tactic_interpreter
 
 (** Internals that can be useful for syntax extensions. *)
 
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index a8088dae36..4f04b9fe1c 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -386,3 +386,8 @@ end
 
 module MakeQueue(T : Task) () = struct include Make(T) () end
 module MakeWorker(T : Task) () = struct include Make(T) () end
+
+exception RemoteException of Pp.t
+let _ = CErrors.register_handler (function
+  | RemoteException ppcmd -> Some ppcmd
+  | _ -> None)
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index cf174d0c93..a1fa6f7268 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -220,3 +220,6 @@ module MakeWorker(T : Task) () : sig
   val main_loop : unit -> unit
 
 end
+
+(** convenience exception to marshall to master *)
+exception RemoteException of Pp.t
diff --git a/stm/partac.ml b/stm/partac.ml
new file mode 100644
index 0000000000..8232b017f9
--- /dev/null
+++ b/stm/partac.ml
@@ -0,0 +1,178 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+
+let stm_pr_err s  = Format.eprintf "%s] %s\n%!"     (Spawned.process_id ()) s
+
+module TacTask : sig
+
+  type output = (Constr.constr * UState.t) option
+  type task = {
+    t_state    : Vernacstate.t;
+    t_assign   : output Future.assignment -> unit;
+    t_ast      : ComTactic.interpretable;
+    t_goalno   : int;
+    t_goal     : Goal.goal;
+    t_kill     : unit -> unit;
+    t_name     : string }
+
+  include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
+
+  let forward_feedback { Feedback.doc_id = did; span_id = id; route; contents } =
+    Feedback.feedback ~did ~id ~route contents
+
+  type output = (Constr.constr * UState.t) option
+
+  type task = {
+    t_state    : Vernacstate.t;
+    t_assign   : output Future.assignment -> unit;
+    t_ast      : ComTactic.interpretable;
+    t_goalno   : int;
+    t_goal     : Goal.goal;
+    t_kill     : unit -> unit;
+    t_name     : string }
+
+  type request = {
+    r_state    : Vernacstate.t option;
+    r_ast      : ComTactic.interpretable;
+    r_goalno   : int;
+    r_goal     : Goal.goal;
+    r_name     : string }
+
+  type response =
+    | RespBuiltSubProof of (Constr.constr * UState.t)
+    | RespError of Pp.t
+    | RespNoProgress
+
+  let name = ref "tacticworker"
+  let extra_env () = [||]
+  type competence = unit
+  type worker_status = Fresh | Old of competence
+
+  let task_match _ _ = true
+
+  (* run by the master, on a thread *)
+  let request_of_task age { t_state; t_ast; t_goalno; t_goal; t_name } =
+    Some {
+      r_state    = if age <> Fresh then None else Some t_state;
+      r_ast      = t_ast;
+      r_goalno   = t_goalno;
+      r_goal     = t_goal;
+      r_name     = t_name }
+
+  let use_response _ { t_assign; t_kill } resp =
+    match resp with
+    | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
+    | RespNoProgress ->
+        t_assign (`Val None);
+        t_kill ();
+        `Stay ((),[])
+    | RespError msg ->
+        let e = (AsyncTaskQueue.RemoteException msg, Exninfo.null) in
+        t_assign (`Exn e);
+        t_kill ();
+        `Stay ((),[])
+
+  let on_marshal_error err { t_name } =
+    stm_pr_err ("Fatal marshal error: " ^ t_name );
+    flush_all (); exit 1
+
+  let on_task_cancellation_or_expiration_or_slave_death = function
+    | Some { t_kill } -> t_kill ()
+    | _ -> ()
+
+  let command_focus = Proof.new_focus_kind ()
+  let focus_cond = Proof.no_cond command_focus
+
+  let state = ref None
+  let receive_state = function
+    | None -> ()
+    | Some st -> state := Some st
+
+  let perform { r_state = st; r_ast = tactic; r_goal; r_goalno } =
+    receive_state st;
+    Vernacstate.unfreeze_interp_state (Option.get !state);
+    try
+      Vernacstate.LemmaStack.with_top (Option.get (Option.get !state).Vernacstate.lemmas) ~f:(fun pstate ->
+          let pstate =
+            Declare.Proof.map pstate ~f:(Proof.focus focus_cond () r_goalno) in
+          let pstate =
+            ComTactic.solve ~pstate
+              Goal_select.SelectAll ~info:None tactic ~with_end_tac:false in
+          let { Proof.sigma } = Declare.Proof.fold pstate ~f:Proof.data in
+          match Evd.(evar_body (find sigma r_goal)) with
+          | Evd.Evar_empty -> RespNoProgress
+          | Evd.Evar_defined t ->
+              let t = Evarutil.nf_evar sigma t in
+              let evars = Evarutil.undefined_evars_of_term sigma t in
+              if Evar.Set.is_empty evars then
+                let t = EConstr.Unsafe.to_constr t in
+                RespBuiltSubProof (t, Evd.evar_universe_context sigma)
+              else
+                CErrors.user_err ~hdr:"STM"
+                  Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++
+                      str" solves the goal and leaves no unresolved existential variables. The following" ++
+                      str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars))
+       )
+    with e when CErrors.noncritical e ->
+      RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int r_goalno ++ str ")")
+
+  let name_of_task { t_name } = t_name
+  let name_of_request { r_name } = r_name
+
+end (* }}} *)
+
+module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
+
+let assign_tac ~abstract res : unit Proofview.tactic =
+  Proofview.(Goal.enter begin fun g ->
+  let gid = Goal.goal g in
+  let g_solution =
+    try List.assoc gid res
+    with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
+  if not (Future.is_over g_solution) then
+    tclUNIT ()
+  else
+    let open Notations in
+    match Future.join g_solution with
+    | Some (pt, uc) ->
+        let push_state ctx =
+            Proofview.tclEVARMAP >>= fun sigma ->
+            Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx)
+        in
+        (if abstract then Abstract.tclABSTRACT None else (fun x -> x))
+            (push_state uc <*> Tactics.exact_no_check (EConstr.of_constr pt))
+    | None -> tclUNIT ()
+  end)
+
+let enable_par ~nworkers = ComTactic.set_par_implementation
+  (fun ~pstate ~info t_ast ~abstract ~with_end_tac ->
+    let t_state = Vernacstate.freeze_interp_state ~marshallable:true in
+    TaskQueue.with_n_workers nworkers CoqworkmgrApi.High (fun queue ->
+    Declare.Proof.map pstate ~f:(fun p ->
+    let open TacTask in
+    let results = (Proof.data p).Proof.goals |> CList.map_i (fun i g ->
+      let g_solution, t_assign =
+      Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i)
+          (fun x -> x) in
+      TaskQueue.enqueue_task queue
+      ~cancel_switch:(ref false)
+      { t_state; t_assign; t_ast;
+          t_goalno = i; t_goal = g; t_name = Goal.uid g;
+          t_kill = (fun () -> TaskQueue.cancel_all queue) };
+      g, g_solution) 1 in
+    TaskQueue.join queue;
+    let p,_,() =
+      Proof.run_tactic (Global.env())
+      (assign_tac ~abstract results) p in
+    p)))
diff --git a/stm/partac.mli b/stm/partac.mli
new file mode 100644
index 0000000000..a206b2e5d8
--- /dev/null
+++ b/stm/partac.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val enable_par : nworkers:int -> unit
+
+module TacTask : AsyncTaskQueue.Task
diff --git a/stm/stm.ml b/stm/stm.ml
index 4ca0c365bf..85f889c879 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -159,9 +159,9 @@ type cmd_t = {
   cids : Names.Id.t list;
   cblock : proof_block_name option;
   cqueue : [ `MainQueue
-           | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch
-           | `QueryQueue of AsyncTaskQueue.cancel_switch
-           | `SkipQueue ] }
+           | `QueryQueue
+           | `SkipQueue ];
+  cancel_switch : AsyncTaskQueue.cancel_switch; }
 type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list
 type qed_t = {
   qast : aast;
@@ -190,10 +190,10 @@ type step =
 type visit = { step : step; next : Stateid.t }
 
 let mkTransTac cast cblock cqueue =
-  Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+  Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false; cancel_switch = ref false }
 
 let mkTransCmd cast cids ceff cqueue =
-  Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
+  Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff; cancel_switch = ref false }
 
 type cached_state =
   | EmptyState
@@ -742,8 +742,7 @@ end = struct (* {{{ *)
     Stateid.Set.iter (fun id ->
         match (Vcs_aux.visit old_vcs id).step with
         | `Qed ({ fproof = Some (_, cancel_switch) }, _)
-        | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) }
-        | `Cmd { cqueue = `QueryQueue cancel_switch } ->
+        | `Cmd { cancel_switch } ->
              cancel_switch := true
         | _ -> ())
       erased_nodes;
@@ -1222,11 +1221,6 @@ let record_pb_time ?loc proof_name time =
     hints := Aux_file.set !hints proof_name proof_build_time
   end
 
-exception RemoteException of Pp.t
-let _ = CErrors.register_handler (function
-  | RemoteException ppcmd -> Some ppcmd
-  | _ -> None)
-
 (****************** proof structure for error recovery ************************)
 (******************************************************************************)
 
@@ -1429,7 +1423,7 @@ end = struct (* {{{ *)
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
         feedback (InProgress ~-1);
         let info = Stateid.add ~valid Exninfo.null e_error_at in
-        let e = (RemoteException e_msg, info) in
+        let e = (AsyncTaskQueue.RemoteException e_msg, info) in
         t_assign (`Exn e);
         `Stay(t_states,[States e_safe_states])
     | _ -> assert false
@@ -1440,7 +1434,7 @@ end = struct (* {{{ *)
     | Some (BuildProof { t_start = start; t_assign }) ->
         let s = "Worker dies or task expired" in
         let info = Stateid.add ~valid:start Exninfo.null start in
-        let e = (RemoteException (Pp.strbrk s), info) in
+        let e = (AsyncTaskQueue.RemoteException (Pp.strbrk s), info) in
         t_assign (`Exn e);
         execution_error start (Pp.strbrk s);
         feedback (InProgress ~-1)
@@ -1792,225 +1786,6 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
-and TacTask : sig
-
-  type output = (Constr.constr * UState.t) option
-  type task = {
-    t_state    : Stateid.t;
-    t_state_fb : Stateid.t;
-    t_assign   : output Future.assignment -> unit;
-    t_ast      : int * aast;
-    t_goal     : Goal.goal;
-    t_kill     : unit -> unit;
-    t_name     : string }
-
-  include AsyncTaskQueue.Task with type task := task
-
-end = struct (* {{{ *)
-
-  type output = (Constr.constr * UState.t) option
-
-  let forward_feedback msg = Hooks.(call forward_feedback msg)
-
-  type task = {
-    t_state    : Stateid.t;
-    t_state_fb : Stateid.t;
-    t_assign   : output Future.assignment -> unit;
-    t_ast      : int * aast;
-    t_goal     : Goal.goal;
-    t_kill     : unit -> unit;
-    t_name     : string }
-
-  type request = {
-    r_state    : Stateid.t;
-    r_state_fb : Stateid.t;
-    r_document : VCS.vcs option;
-    r_ast      : int * aast;
-    r_goal     : Goal.goal;
-    r_name     : string }
-
-  type response =
-    | RespBuiltSubProof of (Constr.constr * UState.t)
-    | RespError of Pp.t
-    | RespNoProgress
-
-  let name = ref "tacticworker"
-  let extra_env () = [||]
-  type competence = unit
-  type worker_status = Fresh | Old of competence
-
-  let task_match _ _ = true
-
-  (* run by the master, on a thread *)
-  let request_of_task age { t_state; t_state_fb; t_ast; t_goal; t_name } =
-    try Some {
-      r_state    = t_state;
-      r_state_fb = t_state_fb;
-      r_document =
-        if age <> Fresh then None
-        else Some (VCS.slice ~block_start:t_state ~block_stop:t_state);
-      r_ast      = t_ast;
-      r_goal     = t_goal;
-      r_name     = t_name }
-    with VCS.Expired -> None
-
-  let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
-    match resp with
-    | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[])
-    | RespNoProgress ->
-        t_assign (`Val None);
-        t_kill ();
-        `Stay ((),[])
-    | RespError msg ->
-        let e = (RemoteException msg, Exninfo.null) in
-        t_assign (`Exn e);
-        t_kill ();
-        `Stay ((),[])
-
-  let on_marshal_error err { t_name } =
-    stm_pr_err ("Fatal marshal error: " ^ t_name );
-    flush_all (); exit 1
-
-  let on_task_cancellation_or_expiration_or_slave_death = function
-    | Some { t_kill } -> t_kill ()
-    | _ -> ()
-
-  let command_focus = Proof.new_focus_kind ()
-  let focus_cond = Proof.no_cond command_focus
-
-  let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
-    Option.iter VCS.restore vcs;
-    try
-      Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
-      State.purify (fun () ->
-       let Proof.{sigma=sigma0} = Proof.data (PG_compat.give_me_the_proof ()) in
-       let g = Evd.find sigma0 r_goal in
-       let is_ground c = Evarutil.is_ground_term sigma0 c in
-       if not (
-         is_ground Evd.(evar_concl g) &&
-         List.for_all (Context.Named.Declaration.for_all is_ground)
-                      Evd.(evar_context g))
-       then
-         CErrors.user_err ~hdr:"STM" Pp.(strbrk("The par: goal selector does not support goals with existential variables"))
-       else begin
-        let (i, ast) = r_ast in
-        PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p);
-        (* STATE SPEC:
-         * - start : id
-         * - return: id
-         * => captures state id in a future closure, which will
-           discard execution state but for the proof + univs.
-        *)
-        let st = Vernacstate.freeze_interp_state ~marshallable:false in
-        ignore(stm_vernac_interp r_state_fb st ast);
-        let Proof.{sigma} = Proof.data (PG_compat.give_me_the_proof ()) in
-        match Evd.(evar_body (find sigma r_goal)) with
-        | Evd.Evar_empty -> RespNoProgress
-        | Evd.Evar_defined t ->
-            let t = Evarutil.nf_evar sigma t in
-            let evars = Evarutil.undefined_evars_of_term sigma t in
-            if Evar.Set.is_empty evars then
-              let t = EConstr.Unsafe.to_constr t in
-              RespBuiltSubProof (t, Evd.evar_universe_context sigma)
-            else
-              CErrors.user_err ~hdr:"STM"
-                Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++
-                    str" solves the goal and leaves no unresolved existential variables. The following" ++
-                    str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars))
-       end) ()
-    with e when CErrors.noncritical e ->
-      RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int (fst r_ast) ++ str ")")
-
-  let name_of_task { t_name } = t_name
-  let name_of_request { r_name } = r_name
-
-end (* }}} *)
-
-and Partac : sig
-
-  val vernac_interp :
-    solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch ->
-    int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit
-
-end = struct (* {{{ *)
-
-  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
-
-  let stm_fail ~st fail f =
-    if fail then
-      Vernacinterp.with_fail ~st f
-    else
-      f ()
-
-  let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id
-    { indentation; verbose; expr = e; strlen } : unit
-  =
-    let cl, time, batch, fail =
-      let rec find ~time ~batch ~fail cl = match cl with
-        | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl
-        | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl
-        | ControlFail :: cl -> find ~time ~batch ~fail:true cl
-        | cl -> cl, time, batch, fail in
-      find ~time:false ~batch:false ~fail:false e.CAst.v.control in
-    let e = CAst.map (fun cmd -> { cmd with control = cl }) e in
-    let st = Vernacstate.freeze_interp_state ~marshallable:false in
-    stm_fail ~st fail (fun () ->
-    (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
-    TaskQueue.with_n_workers nworkers priority (fun queue ->
-    PG_compat.map_proof (fun p ->
-      let Proof.{goals} = Proof.data p in
-      let open TacTask in
-      let res = CList.map_i (fun i g ->
-        let f, assign =
-          Future.create_delegate
-            ~name:(Printf.sprintf "subgoal %d" i)
-            (State.exn_on id ~valid:safe_id) in
-        let t_ast = (i, { indentation; verbose; expr = e; strlen }) in
-        let t_name = Goal.uid g in
-        TaskQueue.enqueue_task queue
-          { t_state = safe_id; t_state_fb = id;
-            t_assign = assign; t_ast; t_goal = g; t_name;
-            t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) }
-           ~cancel_switch;
-        g,f)
-        1 goals in
-      TaskQueue.join queue;
-      let assign_tac : unit Proofview.tactic =
-        Proofview.(Goal.enter begin fun g ->
-        let gid = Goal.goal g in
-        let f =
-          try List.assoc gid res
-          with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
-        if not (Future.is_over f) then
-          (* One has failed and cancelled the others, but not this one *)
-          if solve then Tacticals.New.tclZEROMSG
-            (str"Interrupted by the failure of another goal")
-          else tclUNIT ()
-        else
-          let open Notations in
-          match Future.join f with
-          | Some (pt, uc) ->
-            let sigma, env = PG_compat.get_current_context () in
-            let push_state ctx =
-              Proofview.tclEVARMAP >>= fun sigma ->
-              Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx)
-            in
-            stm_pperr_endline (fun () -> hov 0 (
-              str"g=" ++ int (Evar.repr gid) ++ spc () ++
-              str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
-              str"uc=" ++ Termops.pr_evar_universe_context uc));
-            (if abstract then Abstract.tclABSTRACT None else (fun x -> x))
-              (push_state uc <*>
-              Tactics.exact_no_check (EConstr.of_constr pt))
-          | None ->
-            if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
-        end)
-      in
-      let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in
-      p))) ())
-
-end (* }}} *)
-
 and QueryTask : sig
 
   type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
@@ -2361,15 +2136,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
             reach view.next), cache, true
-      | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } ->
-          (fun () ->
-            resilient_tactic id cblock (fun () ->
-              reach ~cache:true view.next;
-              Partac.vernac_interp ~solve ~abstract ~cancel_switch
-                !cur_opt.async_proofs_n_tacworkers
-                !cur_opt.async_proofs_worker_priority view.next id x)
-          ), cache, true
-      | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
+      | `Cmd { cast = x; cqueue = `QueryQueue; cancel_switch }
         when async_proofs_is_master !cur_opt -> (fun () ->
             reach view.next;
             Query.vernac_interp ~cancel_switch view.next id x
@@ -2377,7 +2144,6 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
       | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
             resilient_tactic id cblock (fun () ->
               reach view.next;
-              (* State resulting from reach *)
               let st = Vernacstate.freeze_interp_state ~marshallable:false in
               ignore(stm_vernac_interp id st x)
             )
@@ -2588,6 +2354,7 @@ let doc_type_module_name (std : stm_doc_type) =
 
 let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
+  if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers;
   State.register_root_state ()
 
 let dirpath_of_file f =
@@ -2938,12 +2705,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
           VCS.set_parsing_state id head_parsing;
           Backtrack.record (); `Ok
 
-      | VtProofStep { parallel; proof_block_detection = cblock } ->
+      | VtProofStep { proof_block_detection = cblock } ->
           let id = VCS.new_node ~id:newtip proof_mode () in
-          let queue =
-            match parallel with
-            | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
-            | `No -> `MainQueue in
+          let queue = `MainQueue in
           VCS.commit id (mkTransTac x cblock queue);
           (* Static proof block detection delayed until an error really occurs.
              If/when and UI will make something useful with this piece of info,
diff --git a/stm/stm.mli b/stm/stm.mli
index 9780c96512..097bcbe0ca 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -195,7 +195,6 @@ val set_perspective : doc:doc -> Stateid.t list -> unit
 (** workers **************************************************************** **)
 
 module ProofTask : AsyncTaskQueue.Task
-module TacTask   : AsyncTaskQueue.Task
 module QueryTask : AsyncTaskQueue.Task
 
 (** document structure customization *************************************** **)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 4b254e8113..831369625f 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -6,6 +6,7 @@ WorkerPool
 Vernac_classifier
 CoqworkmgrApi
 AsyncTaskQueue
+Partac
 Stm
 ProofBlockDelimiter
 Vio_checking
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f89fb9f52d..3996c64b67 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -15,11 +15,6 @@ open CAst
 open Vernacextend
 open Vernacexpr
 
-let string_of_parallel = function
-  | `Yes (solve,abs) ->
-       "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
-  | `No -> ""
-
 let string_of_vernac_when = function
   | VtLater -> "Later"
   | VtNow -> "Now"
@@ -30,9 +25,8 @@ let string_of_vernac_classification = function
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
   | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
   | VtQed VtDrop -> "Qed(drop)"
-  | VtProofStep { parallel; proof_block_detection } ->
-      "ProofStep " ^ string_of_parallel parallel ^
-        Option.default "" proof_block_detection
+  | VtProofStep {  proof_block_detection } ->
+      "ProofStep " ^ Option.default "" proof_block_detection
   | VtQuery -> "Query"
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
@@ -80,12 +74,11 @@ let classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ ->
-        VtProofStep { parallel = `No; proof_block_detection = None }
+        VtProofStep { proof_block_detection = None }
     | VernacBullet _ ->
-        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }
+        VtProofStep { proof_block_detection = Some "bullet" }
     | VernacEndSubproof ->
-        VtProofStep { parallel = `No;
-                      proof_block_detection = Some "curly" }
+        VtProofStep { proof_block_detection = Some "curly" }
     (* StartProof *)
     | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
@@ -213,7 +206,7 @@ let classify_vernac e =
       (match static_classifier ~atts:v.attrs v.expr with
          | VtQuery | VtProofStep _ | VtSideff _
          | VtMeta as x -> x
-         | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
+         | VtQed _ -> VtProofStep { proof_block_detection = None }
          | VtStartProof _ | VtProofMode _ -> VtQuery)
     else
       static_classifier ~atts:v.attrs v.expr
diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml
index 252c8faa05..706554e025 100644
--- a/topbin/coqtacticworker_bin.ml
+++ b/topbin/coqtacticworker_bin.ml
@@ -8,6 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
+module W = AsyncTaskQueue.MakeWorker(Partac.TacTask) ()
 
 let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker"
diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml
new file mode 100644
index 0000000000..8a9a412362
--- /dev/null
+++ b/vernac/comTactic.ml
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Goptions
+
+module Dyn = Dyn.Make()
+
+module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end)
+
+let interp_map = ref DMap.empty
+
+type 'a tactic_interpreter = 'a Dyn.tag
+type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+
+let register_tactic_interpreter na f =
+  let t = Dyn.create na in
+  interp_map := DMap.add t f !interp_map;
+  t
+
+let interp_tac (I (tag,t)) =
+  let f = DMap.find tag !interp_map in
+  f t
+
+type parallel_solver =
+  pstate:Declare.Proof.t ->
+  info:int option ->
+  interpretable ->
+  abstract:bool ->
+  with_end_tac:bool ->
+  Declare.Proof.t
+
+let print_info_trace =
+  declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
+
+let solve_core ~pstate n ~info t ~with_end_tac:b =
+  let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
+      let with_end_tac = if b then Some etac else None in
+      let info = Option.append info (print_info_trace ()) in
+      let (p,status) = Proof.solve n info t ?with_end_tac p in
+      (* in case a strict subtree was completed,
+         go back to the top of the prooftree *)
+      let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+      p,status) pstate in
+  if not status then Feedback.feedback Feedback.AddedAxiom;
+  pstate
+
+let solve ~pstate n ~info t ~with_end_tac =
+  let t = interp_tac t in
+  solve_core ~pstate n ~info t ~with_end_tac
+
+let check_par_applicable pstate =
+  Declare.Proof.fold pstate ~f:(fun p ->
+    (Proof.data p).Proof.goals |> List.iter (fun goal ->
+    let is_ground =
+      let { Proof.sigma = sigma0 } = Declare.Proof.fold pstate ~f:Proof.data in
+      let g = Evd.find sigma0 goal in
+      let concl, hyps = Evd.evar_concl g, Evd.evar_context g in
+      Evarutil.is_ground_term sigma0 concl &&
+      List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) hyps in
+    if not is_ground then
+      CErrors.user_err
+        Pp.(strbrk("The par: goal selector does not support goals with existential variables"))))
+
+let par_implementation = ref (fun ~pstate ~info t ~abstract ~with_end_tac ->
+  let t = interp_tac t in
+  let t = Proofview.Goal.enter (fun _ ->
+    if abstract then Abstract.tclABSTRACT None ~opaque:true t else t) 
+  in
+  solve_core ~pstate Goal_select.SelectAll ~info t ~with_end_tac)
+
+let set_par_implementation f = par_implementation := f
+
+let solve_parallel ~pstate ~info t ~abstract ~with_end_tac =
+  check_par_applicable pstate;
+  !par_implementation ~pstate ~info t ~abstract ~with_end_tac
diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli
new file mode 100644
index 0000000000..f1a75e1b6a
--- /dev/null
+++ b/vernac/comTactic.mli
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Tactic interpreters have to register their interpretation function *)
+type 'a tactic_interpreter
+type interpretable = I : 'a tactic_interpreter * 'a -> interpretable
+
+(** ['a] should be marshallable if ever used with [par:] *)
+val register_tactic_interpreter :
+  string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter
+
+(** Entry point for toplevel tactic expression execution. It calls Proof.solve
+    after having interpreted the tactic, and after the tactic runs it
+    unfocus as much as needed to put a goal under focus. *)
+val solve :
+  pstate:Declare.Proof.t ->
+  Goal_select.t ->
+  info:int option ->
+  interpretable ->
+  with_end_tac:bool ->
+  Declare.Proof.t
+
+(** [par: tac] runs tac on all goals, possibly in parallel using a worker pool.
+    If tac is [abstract tac1], then [abstract] is passed
+    explicitly to the solver and [tac1] passed to worker since it is up to
+    master to opacify the sub proofs produced by the workers. *)
+type parallel_solver =
+  pstate:Declare.Proof.t ->
+  info:int option ->
+  interpretable ->
+  abstract:bool -> (* the tactic result has to be opacified as per abstract *)
+  with_end_tac:bool ->
+  Declare.Proof.t
+
+(** Entry point when the goal selector is par: *)
+val solve_parallel : parallel_solver
+
+(** By default par: is implemented with all: (sequential).
+    The STM and LSP document manager provide "more parallel" implementations *)
+val set_par_implementation : parallel_solver -> unit
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 994592a88a..cd0dd5e9a6 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -43,4 +43,5 @@ Topfmt
 Loadpath
 ComArguments
 Vernacentries
+ComTactic
 Vernacinterp
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index eacb7fe6cb..ed63332861 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -30,7 +30,6 @@ type vernac_classification =
   | VtQed of vernac_qed_type
   (* A proof step *)
   | VtProofStep of {
-      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
   (* Queries are commands assumed to be "pure", that is to say, they
@@ -124,7 +123,7 @@ let declare_vernac_classifier name f =
 
 let classify_as_query = VtQuery
 let classify_as_sideeff = VtSideff ([], VtLater)
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}
+let classify_as_proofstep = VtProofStep { proof_block_detection = None}
 
 type (_, _) ty_sig =
 | TyNil : (vernac_command, vernac_classification) ty_sig
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 5ef137cfc0..e1e3b4cfe5 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -46,7 +46,6 @@ type vernac_classification =
   | VtQed of vernac_qed_type
   (* A proof step *)
   | VtProofStep of {
-      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
       proof_block_detection : proof_block_name option
     }
   (* Queries are commands assumed to be "pure", that is to say, they