perf: parallelize exact? and apply? tactics

Use `MetaM.parIterWithCancel` to try all candidate lemmas in parallel
while preserving deterministic result ordering. When a complete solution
is found, remaining tasks are cancelled and the result is returned
immediately.

This removes the old sequential `tryOnEach` implementation along with
the heartbeat-based abortion mechanism (`abortSpeculation`,
`mkHeartbeatCheck`).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <[email protected]>

Author: kim-em

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -37,7 +37,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
     let allowFailure := fun g => do
       let g ← g.withContext (instantiateMVars (.mvar g))
       return required.all fun e => e.occurs g
-    match (← librarySearch goal tactic allowFailure) with
+    match ← librarySearch goal tactic allowFailure with
     -- Found goal that closed problem
     | none =>
       addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (checkState? := initialState)

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.LazyDiscrTree
 public import Lean.Meta.Tactic.SolveByElim
 public import Lean.Util.Heartbeats
+public import Lean.Elab.Parallel
 
 public section
 
@@ -119,20 +120,6 @@ def libSearchFindDecls : Expr → MetaM (Array (Name × DeclMod)) :=
       (droppedKeys := droppedKeys)
       (constantsPerTask := constantsPerImportTask)
 
-/--
-Return an action that returns true when the remaining heartbeats is less
-than the currently remaining heartbeats * leavePercent / 100.
--/
-def mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool) := do
-  let maxHB ← getMaxHeartbeats
-  let hbThreshold := (← getRemainingHeartbeats) * leavePercent / 100
-  -- Return true if we should stop
-  pure $
-    if maxHB = 0 then
-      pure false
-    else do
-      return (← getRemainingHeartbeats) < hbThreshold
-
 private def librarySearchEmoji : Except ε (Option α) → String
 | .error _ => bombEmoji
 | .ok (some _) => crossEmoji
@@ -157,24 +144,6 @@ def interleaveWith {α β γ} (f : α → γ) (x : Array α) (g : β → γ) (y
           (y.extract n y.size).map g
   pure $ res ++ last
 
-/--
-An exception ID that indicates further speculation on candidate lemmas should stop
-and current results should be returned.
--/
-private builtin_initialize abortSpeculationId : InternalExceptionId ←
-  registerInternalExceptionId `Lean.Meta.LibrarySearch.abortSpeculation
-
-/--
-Called to abort speculative execution in library search.
--/
-def abortSpeculation [MonadExcept Exception m] : m α :=
-  throw (Exception.internal abortSpeculationId {})
-
-/-- Returns true if this is an abort speculation exception. -/
-def isAbortSpeculation : Exception → Bool
-| .internal id _ => id == abortSpeculationId
-| _ => false
-
 section LibrarySearch
 
 /--
@@ -241,59 +210,14 @@ private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM
       else
         failure
 
-/--
-Sequentially invokes a tactic `act` on each value in candidates on the current state.
-
-The tactic `act` should return a list of meta-variables that still need to be resolved.
-If this list is empty, then no variables remain to be solved, and `tryOnEach` returns
-`none` with the environment set so each goal is resolved.
-
-If the action throws an internal exception with the `abortSpeculationId` id then
-further computation is stopped and intermediate results returned. If any other
-exception is thrown, then it is silently discarded.
--/
-def tryOnEach
-    (act : Candidate → MetaM (List MVarId))
-    (candidates : Array Candidate) :
-    MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  let mut a := #[]
-  let s ← saveState
-  for c in candidates do
-    match ← (tryCatch (Except.ok <$> act c) (pure ∘ Except.error)) with
-    | .error e =>
-      restoreState s
-      if isAbortSpeculation e then
-        break
-    | .ok remaining =>
-      if remaining.isEmpty then
-        return none
-      let ctx ← getMCtx
-      restoreState s
-      a := a.push (remaining, ctx)
-  return (.some a)
-
-private def librarySearch' (goal : MVarId)
-    (tactic : List MVarId → MetaM (List MVarId))
-    (allowFailure : MVarId → MetaM Bool)
-    (leavePercentHeartbeats : Nat) :
-    MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
-  profileitM Exception "librarySearch" (← getOptions) do
-    -- Create predicate that returns true when running low on heartbeats.
-    let candidates ← librarySearchSymm libSearchFindDecls goal
-    let cfg : ApplyConfig := { allowSynthFailures := true }
-    let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats
-    let act := fun cand => do
-        if ←shouldAbort then
-          abortSpeculation
-        librarySearchLemma cfg tactic allowFailure cand
-    tryOnEach act candidates
-
 /--
 Tries to solve the goal either by:
 * calling `tactic true`
 * or applying a library lemma then calling `tactic false` on the resulting goals.
 
+Runs all candidates in parallel, iterates through results in order.
+Cancels remaining tasks and returns immediately if a complete solution is found.
+
 Typically here `tactic` is `solveByElim`,
 with the `Bool` flag indicating whether it may retry with `exfalso`.
 
@@ -311,11 +235,36 @@ this is not currently tracked.)
 def librarySearch (goal : MVarId)
     (tactic : Bool → List MVarId → MetaM (List MVarId) :=
       fun initial g => solveByElim [] (maxDepth := 6) (exfalso := initial) g)
-    (allowFailure : MVarId → MetaM Bool := fun _ => pure true)
-    (leavePercentHeartbeats : Nat := 10) :
+    (allowFailure : MVarId → MetaM Bool := fun _ => pure true) :
     MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  (tactic true [goal] *> pure none) <|>
-  librarySearch' goal (tactic false) allowFailure leavePercentHeartbeats
+  let tryDirect : MetaM (Option (Array (List MVarId × MetavarContext))) := do
+    let _ ← tactic true [goal]
+    pure none
+  tryDirect <|> do
+  withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
+  profileitM Exception "librarySearch" (← getOptions) do
+    let candidates ← librarySearchSymm libSearchFindDecls goal
+    let cfg : ApplyConfig := { allowSynthFailures := true }
+    let jobs := candidates.toList.map fun cand => do
+      let remaining ← librarySearchLemma cfg (tactic false) allowFailure cand
+      pure (remaining, ← getMCtx)
+    let (cancel, iter) ← MetaM.parIterWithCancelChunked jobs (maxTasks := 128)
+    let mut partialSuccesses : Array (List MVarId × MetavarContext) := #[]
+    for result in iter.allowNontermination do
+      match result with
+      | .ok (remaining, mctx) =>
+        if remaining.isEmpty then
+          -- Complete solution found - cancel remaining tasks and return
+          cancel
+          setMCtx mctx
+          return none
+        else
+          -- Partial success - collect it
+          partialSuccesses := partialSuccesses.push (remaining, mctx)
+      | .error _ =>
+        -- Task failed, continue to next
+        continue
+    return some partialSuccesses
 
 end LibrarySearch