[stm] move par: implementation to vernac/comTactic and stm/partac

The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).

This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

5 files changed, 131 insertions, 3 deletions

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 496b1a43d1..1a355c5c5d 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