par: like all: but in parallel

This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.

`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.

`par: abstract tac` runs abstract on the generated proof terms.  Nested
abstract calls are not supported.

7 files changed, 149 insertions, 49 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 722249191..5ba3c308a 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -209,6 +209,8 @@ is understood as
 \\
 \selector & ::= &
         [{\ident}]\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}\\
 & $|$ & {\integer}\\
 & $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
           {\tt ,}
@@ -393,6 +395,22 @@ all selected goals.
     In this variant, {\tacexpr} is applied globally to the subset
     of goals described by the given ranges. You can write a single
     $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
+
+  \item {\tt all: } {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals.
+
+  \item {\tt par: } {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals
+    in parallel.  The number of workers can be controlled via the
+    command line option {\tt -async-proofs-tac-j} taking as argument
+    the desired number of workers.  Limitations:  {\tt par: } only works
+    on goals containing no existential variables and {\tacexpr} must
+    either solve the goal completely or do nothing (i.e. it cannot make
+    some progress).
+    {\tt par: } can only be used at the top level of a tactic expression.
+
 \end{Variants}
 
 \ErrMsg \errindex{No such goal}
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 45d71e32b..1c75d76dd 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -484,9 +484,11 @@ and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
 and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : bool;
+  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
   proof_block_detection : proof_block_name option
 }
+and solving_tac = bool (* a terminator *)
+and anon_abstracting_tac = bool (* abstracting anonymously its result *)
 and proof_block_name = string (* open type of delimiters *)
 type vernac_when =
   | VtNow
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 0de303c30..517f9e3af 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -384,6 +384,16 @@ VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
 | [ "..." ] -> [ true ]
 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
+let is_explicit_terminator = function TacSolve _ -> true | _ -> false
+
 VERNAC tactic_mode EXTEND VernacSolve
 | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     [ classify_as_proofstep ] -> [
@@ -391,10 +401,17 @@ VERNAC tactic_mode EXTEND VernacSolve
     vernac_solve g n t def
   ]
 | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
-    [ VtProofStep{ parallel = true; proof_block_detection = Some "par" },
-      VtLater ] -> [
-    vernac_solve SelectAll n t def
-  ]
+    [
+      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 },
+      VtLater
+    ] -> [
+      let t = rm_abstract t in
+      vernac_solve SelectAll n t def
+    ]
 END
 
 let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")"
diff --git a/stm/stm.ml b/stm/stm.ml
index c0813827d..87c23c30c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -178,7 +178,7 @@ type cmd_t = {
   cids : Id.t list;
   cblock : proof_block_name option;
   cqueue : [ `MainQueue
-           | `TacQueue of cancel_switch
+           | `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch
            | `QueryQueue of cancel_switch
            | `SkipQueue ] }
 type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
@@ -660,7 +660,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 = `TacQueue (_,_,cancel_switch) }
         | `Cmd { cqueue = `QueryQueue cancel_switch } ->
              cancel_switch := true
         | _ -> ())
@@ -1127,9 +1127,8 @@ let is_block_name_enabled name =
 let detect_proof_block id name =
   let name = match name with None -> "indent" | Some x -> x in   
   if is_block_name_enabled name &&
-     (if Flags.async_proofs_is_master () then
-      !Flags.async_proofs_mode != Flags.APoff else true)
-  then
+     (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ())
+  then (
   match cur_node id with
   | None -> ()
   | Some entry_point -> try
@@ -1142,7 +1141,7 @@ let detect_proof_block id name =
     with Not_found ->
       Errors.errorlabstrm "STM"
         (str "Unknown proof block delimiter " ++ str name)
-
+  )
 (****************************** THE SCHEDULER *********************************)
 (******************************************************************************)
 
@@ -1617,6 +1616,7 @@ and TacTask : sig
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
+  exception NoProgress
 
   include AsyncTaskQueue.Task with type task := task
 
@@ -1646,6 +1646,8 @@ end = struct (* {{{ *)
   type response =
     | RespBuiltSubProof of output
     | RespError of std_ppcmds
+    | RespNoProgress
+  exception NoProgress
 
   let name = ref "tacworker"
   let extra_env () = [||]
@@ -1668,6 +1670,11 @@ end = struct (* {{{ *)
   let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
     match resp with
     | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+    | RespNoProgress ->
+        let e = (NoProgress, Exninfo.null) in
+        t_assign (`Exn e);
+        t_kill ();
+        `Stay ((),[])
     | RespError msg ->
         let e = (RemoteException msg, Exninfo.null) in
         t_assign (`Exn e);
@@ -1689,7 +1696,7 @@ end = struct (* {{{ *)
     Option.iter VCS.restore vcs;
     try
       Reach.known_state ~cache:`No id;
-      let t, uc = Future.purify (fun () ->
+      Future.purify (fun () ->
        let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
        if not (
@@ -1705,15 +1712,13 @@ end = struct (* {{{ *)
         vernac_interp r_state_fb ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
-        | Evd.Evar_empty -> Errors.errorlabstrm "STM" (str "no progress")
+        | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
-              t, Evd.evar_universe_context sigma
+              RespBuiltSubProof (t, Evd.evar_universe_context sigma)
             else Errors.errorlabstrm "STM" (str"The solution is not ground")
        end) ()
-     in
-       RespBuiltSubProof (t,uc)
     with e when Errors.noncritical e -> RespError (Errors.print e)
 
   let name_of_task { t_name } = t_name
@@ -1724,13 +1729,15 @@ end (* }}} *)
 and Partac : sig
 
   val vernac_interp :
-    cancel_switch -> int -> Stateid.t -> Stateid.t -> aast -> unit
+    solve:bool -> abstract:bool -> cancel_switch ->
+    int -> Stateid.t -> Stateid.t -> aast ->
+      unit
 
 end = struct (* {{{ *)
     
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
-  let vernac_interp cancel nworkers safe_id id
+  let vernac_interp ~solve ~abstract cancel nworkers safe_id id
     { indentation; verbose; loc; expr = e; strlen }
   =
     let e, time, fail =
@@ -1754,29 +1761,37 @@ end = struct (* {{{ *)
         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 () -> TaskQueue.cancel_all queue) }, cancel);
-        Goal.uid g,f)
+            t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) },
+           cancel);
+        g,f)
         1 goals in
       TaskQueue.join queue;
       let assign_tac : unit Proofview.tactic =
-        Proofview.V82.tactic (fun gl ->
-          let open Tacmach in
-          let sigma, g = project gl, sig_it gl in
-          let gid = Goal.uid g in
-          let f =
-            try List.assoc gid res
-            with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
-          if Future.is_over f then
+        Proofview.(Goal.nf_enter { Goal.enter = fun g ->
+        let gid = Goal.goal g in
+        let f =
+          try List.assoc gid res
+          with Not_found -> Errors.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
+          try
             let pt, uc = Future.join f in
             prerr_endline (fun () -> string_of_ppcmds(hov 0 (
-              str"g=" ++ str gid ++ spc () ++
+              str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
               str"uc=" ++ Evd.pr_evar_universe_context uc)));
-            let sigma = Goal.V82.partial_solution sigma g pt in
-            let sigma = Evd.merge_universe_context sigma uc in
-            re_sig [] sigma
-          else (* One has failed and cancelled the others, but not this one *)
-            re_sig [g] sigma) in
+            (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
+              (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
+              Tactics.exact_no_check pt)
+          with TacTask.NoProgress ->
+            if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
+        })
+      in
       Proof.run_tactic (Global.env()) assign_tac p)))) ())
   
 end (* }}} *)
@@ -2088,11 +2103,12 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
             reach view.next), cache, true
-      | `Cmd { cast = x; cqueue = `TacQueue cancel; cblock } -> (fun () ->
+      | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel); cblock } ->
+          (fun () ->
             resilient_tactic id cblock (fun () ->
               reach ~cache:`Shallow view.next;
               Hooks.(call tactic_being_run true); 
-              Partac.vernac_interp
+              Partac.vernac_interp ~solve ~abstract
                 cancel !Flags.async_proofs_n_tacworkers view.next id x;
               Hooks.(call tactic_being_run false))
           ), cache, true
@@ -2507,7 +2523,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           `Ok
       | VtProofStep { parallel; proof_block_detection = cblock }, w ->
           let id = VCS.new_node ~id:newtip () in
-          let queue = if parallel then `TacQueue (ref false) else `MainQueue in
+          let queue =
+            match parallel with
+            | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
+            | `No -> `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/vernac_classifier.ml b/stm/vernac_classifier.ml
index a602d6b8a..f6d8c327e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -14,6 +14,11 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
 
 let string_of_in_script b = if b then " (inside script)" else ""
 
+let string_of_parallel = function
+  | `Yes (solve,abs) ->
+       "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
+  | `No -> ""
+
 let string_of_vernac_type = function
   | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
@@ -22,7 +27,7 @@ let string_of_vernac_type = function
   | VtQed VtKeepAsAxiom -> "Qed(admitted)"
   | VtQed VtDrop -> "Qed(drop)"
   | VtProofStep { parallel; proof_block_detection } ->
-      "ProofStep " ^ if parallel then "par " else "" ^ 
+      "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery (b,(id,route)) ->
@@ -95,7 +100,7 @@ let rec classify_vernac e =
         | ( VtQuery _ | VtProofStep _ | VtSideff _
           | VtStm _ | VtProofMode _ ), _ as x -> x
         | VtQed _, _ ->
-            VtProofStep { parallel = false; proof_block_detection = None },
+            VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
     (* Qed *)
@@ -113,12 +118,12 @@ let rec classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ ->
-        VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+        VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
     | VernacBullet _ ->
-        VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
         VtLater
     | VernacEndSubproof -> 
-        VtProofStep { parallel = false;
+        VtProofStep { parallel = `No;
                       proof_block_detection = Some "curly" },
         VtLater
     (* Options changing parser *)
@@ -229,4 +234,4 @@ let rec classify_vernac e =
 let classify_as_query =
   VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
 let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/test-suite/success/par_abstract.v b/test-suite/success/par_abstract.v
new file mode 100644
index 000000000..7f6f9d627
--- /dev/null
+++ b/test-suite/success/par_abstract.v
@@ -0,0 +1,25 @@
+Axiom T : Type.
+
+Lemma foo : True * Type.
+Proof.
+  split.
+  par: abstract (exact I || exact T).
+Defined.
+
+(* Yes, these names are generated hence
+   the test is fragile.  I want to assert
+   that abstract was correctly handled
+   by par: *)
+Check foo_subproof.
+Check foo_subproof0.
+Check (refl_equal _ :
+  foo =
+  pair foo_subproof foo_subproof0).
+
+Lemma bar : True * Type.
+Proof.
+  split.
+  par: (exact I || exact T).
+Defined.
+Check (refl_equal _ :
+  bar = pair I T).
diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v
index 94ff96ef8..d25fd32a1 100644
--- a/test-suite/success/paralleltac.v
+++ b/test-suite/success/paralleltac.v
@@ -1,3 +1,17 @@
+Lemma test_nofail_like_all1 :
+  True /\ False.
+Proof.
+split.
+all: trivial.
+Admitted.
+
+Lemma test_nofail_like_all2 :
+  True /\ False.
+Proof.
+split.
+par: trivial.
+Admitted.
+
 Fixpoint fib n := match n with
   | O => 1
   | S m => match m with
@@ -19,28 +33,28 @@ Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T1: linear".
-Time all: solve_P.
+Time all: solve [solve_P].
 Qed.
 
 Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T2: parallel".
-Time par: solve_P.
+Time par: solve [solve_P].
 Qed.
 
 Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T3: linear failure".
-Fail Time all: solve_P.
-all: apply (P_triv Type).
+Fail Time all: solve solve_P.
+all: solve [apply (P_triv Type)].
 Qed.
 
 Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T4: parallel failure".
-Fail Time par: solve_P.
-all: apply (P_triv Type).
+Fail Time par: solve [solve_P].
+all: solve [apply (P_triv Type)].
 Qed.