feat: add debug.terminalTacticsAsSorry (#8012)

This PR adds the option `debug.terminalTacticsAsSorry`. When enabled,
terminal tactics such as `grind` and `omega` are replaced with `sorry`.
Useful for debugging and fixing bootstrapping issues.

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -674,16 +674,19 @@ open Lean Elab Tactic Parser.Tactic
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
   let declName? ← Term.getDeclName?
   liftMetaFinishingTactic fun g => do
-    let some g ← g.falseOrByContra | return ()
-    g.withContext do
-      let type ← g.getType
-      let g' ← mkFreshExprSyntheticOpaqueMVar type
-      let hyps := (← getLocalHyps).toList
-      trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
-      omega hyps g'.mvarId! cfg
-      -- Omega proofs are typically rather large, so hide them in a separate definition
-      let e ← mkAuxTheorem (prefix? := declName?) type (← instantiateMVarsProfiling g') (zetaDelta := true)
-      g.assign e
+    if debug.terminalTacticsAsSorry.get (← getOptions) then
+      g.admit
+    else
+      let some g ← g.falseOrByContra | return ()
+      g.withContext do
+        let type ← g.getType
+        let g' ← mkFreshExprSyntheticOpaqueMVar type
+        let hyps := (← getLocalHyps).toList
+        trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
+        omega hyps g'.mvarId! cfg
+        -- Omega proofs are typically rather large, so hide them in a separate definition
+        let e ← mkAuxTheorem (prefix? := declName?) type (← instantiateMVarsProfiling g') (zetaDelta := true)
+        g.assign e
 
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -161,20 +161,26 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
-  let go : GrindM Result := withReducible do
-    let goals ← initCore mvarId params
-    let (failures, skipped) ← solve goals fallback
-    trace[grind.debug.final] "{← ppGoals goals}"
-    let issues   := (← get).issues
-    let trace    := (← get).trace
-    let counters := (← get).counters
-    let simp     := (← get).simpStats
-    if failures.isEmpty then
-      -- If there are no failures and diagnostics are enabled, we still report the performance counters.
-      if (← isDiagnosticsEnabled) then
-        if let some msg ← mkGlobalDiag counters simp then
-          logInfo msg
-    return { failures, skipped, issues, config := params.config, trace, counters, simp }
-  go.run mainDeclName params fallback
+  if debug.terminalTacticsAsSorry.get (← getOptions) then
+    mvarId.admit
+    return {
+        failures := [], skipped := [], issues := [], config := params.config, trace := {}, counters := {}, simp := {}
+    }
+  else
+    let go : GrindM Result := withReducible do
+      let goals ← initCore mvarId params
+      let (failures, skipped) ← solve goals fallback
+      trace[grind.debug.final] "{← ppGoals goals}"
+      let issues   := (← get).issues
+      let trace    := (← get).trace
+      let counters := (← get).counters
+      let simp     := (← get).simpStats
+      if failures.isEmpty then
+        -- If there are no failures and diagnostics are enabled, we still report the performance counters.
+        if (← isDiagnosticsEnabled) then
+          if let some msg ← mkGlobalDiag counters simp then
+            logInfo msg
+      return { failures, skipped, issues, config := params.config, trace, counters, simp }
+    go.run mainDeclName params fallback
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Util.lean

@@ -11,6 +11,12 @@ import Lean.Meta.PPGoal
 
 namespace Lean.Meta
 
+register_builtin_option debug.terminalTacticsAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "when enabled, terminal tactics such as `grind` and `omega` are replaced with `sorry`. Useful for debugging and fixing bootstrapping issues"
+}
+
 /-- Get the user name of the given metavariable. -/
 def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name :=
   return (← mvarId.getDecl).userName

src/stdlib_flags.h

@@ -7,6 +7,8 @@ options get_default_options() {
 #if LEAN_IS_STAGE0 == 1
     // set to true to generally avoid bootstrapping issues limited to proofs
     opts = opts.update({"debug", "proofAsSorry"}, false);
+    // set to true to generally avoid bootstrapping issues in `omega` and `grind`
+    opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
     opts = opts.update({"interpreter", "prefer_native"}, false);

tests/lean/run/terminalAsSorry.lean

@@ -0,0 +1,17 @@
+set_option debug.terminalTacticsAsSorry true
+
+example (_ : x > 0) : False := by
+  omega
+
+example (_ : x > 0) : False := by
+  grind
+
+set_option debug.terminalTacticsAsSorry false
+
+example (_ : x > 0) : False := by
+  fail_if_success omega
+  sorry
+
+example (_ : x > 0) : False := by
+  fail_if_success grind
+  sorry