feat: debug[cls] do for debugging code

This PR adds a simple framework for enabling debugging-only code (consistency checks or special options). Debug classes are similar to trace classes, but their options start with `debug` instead of `trace`. Adds `Meta.validateTypeCorrect` and `Meta.validateIsSort` as consistency check versions that avoid side effects and add context to any errors.

src/Lean/CoreM.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Util.RecDepth
 public import Lean.Util.Trace
+public import Lean.Util.Debug
 public import Lean.Log
 public import Lean.ResolveName
 public import Lean.Elab.InfoTree.Types
@@ -245,6 +246,8 @@ structure Context where
   suppressElabErrors : Bool := false
   /-- Cache of `Lean.inheritedTraceOptions`. -/
   inheritedTraceOptions : Std.HashSet Name := {}
+  /-- Cache of `Lean.inheritedDebugOptions`. -/
+  inheritedDebugOptions : Std.HashSet Name := {}
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -293,7 +296,8 @@ instance : MonadWithOptions CoreM where
 -- Helper function for ensuring fields derived from e.g. options have the correct value.
 @[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
   let inheritedTraceOptions ← inheritedTraceOptions.get
-  withReader (fun ctx => { ctx with inheritedTraceOptions }) do
+  let inheritedDebugOptions ← inheritedDebugOptions.get
+  withReader (fun ctx => { ctx with inheritedTraceOptions, inheritedDebugOptions }) do
     withOptions id x
 
 instance : AddMessageContext CoreM where
@@ -369,6 +373,9 @@ instance : MonadTrace CoreM where
   modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
   getInheritedTraceOptions := return (← read).inheritedTraceOptions
 
+instance : MonadDebug CoreM where
+  getInheritedDebugOptions := return (← read).inheritedDebugOptions
+
 structure SavedState extends State where
   /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
   passedHeartbeats : Nat

src/Lean/Elab/MutualDef.lean

@@ -489,18 +489,14 @@ register_builtin_option linter.unusedSectionVars : Bool := {
   descr := "enable the 'unused section variables in theorem body' linter"
 }
 
-register_builtin_option debug.proofAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace the bodies (proofs) of theorems with `sorry`"
-}
+builtin_initialize
+  registerDebugClass `proofAsSorry "replace the bodies (proofs) of theorems with `sorry`"
 
 /-- Returns true if `k` is a theorem, option `debug.proofAsSorry` is set to true, and the environment contains the axiom `sorryAx`. -/
 private def useProofAsSorry (k : DefKind) : CoreM Bool := do
   if k.isTheorem then
-    if debug.proofAsSorry.get (← getOptions) then
-      if (← getEnv).contains ``sorryAx then
-        return true
+    debug[proofAsSorry] if (← getEnv).contains ``sorryAx then
+      return true
   return false
 
 private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (sc : Command.Scope) : TermElabM (Array Expr) :=

src/Lean/Elab/PreDefinition/WF/Basic.lean

@@ -13,17 +13,18 @@ public section
 
 namespace Lean.Elab.WF
 
-register_builtin_option debug.rawDecreasingByGoal : Bool := {
-  defValue := false
-  descr    := "Shows the raw `decreasing_by` goal including internal implementation detail \
-               instead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
-               purposes. Please report an issue if you have to use this option for other reasons."
-}
+builtin_initialize
+  registerDebugClass `rawDecreasingByGoal
+    "Shows the raw `decreasing_by` goal including internal implementation detail \
+     instead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
+     purposes. Please report an issue if you have to use this option for other reasons."
 
 open Lean Elab Tactic
 
 def applyCleanWfTactic : TacticM Unit := do
-  unless debug.rawDecreasingByGoal.get (← getOptions) do
-    Tactic.evalTactic (← `(tactic| all_goals clean_wf))
+  debug[rawDecreasingByGoal]
+    -- Skip applying `clean_wf`
+    return
+  Tactic.evalTactic (← `(tactic| all_goals clean_wf))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -21,10 +21,9 @@ public section
 namespace Lean.Elab.WF
 open Meta
 
-register_builtin_option debug.definition.wf.replaceRecApps : Bool := {
-    defValue := false
-    descr    := "Type check every step of the well-founded definition translation"
-  }
+builtin_initialize
+  registerDebugClass `definition.wf.replaceRecApps
+    "Type check every step of the well-founded definition translation"
 
 /-
 Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and
@@ -67,7 +66,7 @@ where
 
   loop (F : Expr) (e : Expr) : StateRefT (HasConstCache #[recFnName]) TermElabM Expr := do
     let e' ← loopGo F e
-    if (debug.definition.wf.replaceRecApps.get (← getOptions)) then
+    debug[definition.wf.replaceRecApps] do
       withTransparency .all do withNewMCtxDepth do
         unless (← isTypeCorrect e') do
           throwError "Type error introduced when transforming{indentExpr e}\nto{indentExpr e'}"

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

@@ -676,19 +676,19 @@ open Lean Elab Tactic Parser.Tactic
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. -/
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
   liftMetaFinishingTactic fun g => do
-    if debug.terminalTacticsAsSorry.get (← getOptions) then
+    debug[terminalTacticsAsSorry] do
       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 type (← instantiateMVarsProfiling g') (zetaDelta := true)
-        g.assign e
+      return
+    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 type (← instantiateMVarsProfiling g') (zetaDelta := true)
+      g.assign e
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via

src/Lean/Elab/Term.lean

@@ -1274,11 +1274,8 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) :
 def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
   return (← get).syntheticMVars.get? mvarId
 
-register_builtin_option debug.byAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
-}
+builtin_initialize
+  registerDebugClass `byAsSorry "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
 
 /--
 Creates a new metavariable of type `type` that will be synthesized using the tactic code.
@@ -1286,14 +1283,13 @@ The `tacticCode` syntax is the full `by ..` syntax.
 -/
 def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind)
     (delayOnMVars := false) : TermElabM Expr := do
-  if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
-    withRef tacticCode <| mkLabeledSorry type false (unique := true)
-  else
-    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
-    let mvarId := mvar.mvarId!
-    let ref ← getRef
-    registerSyntheticMVar ref mvarId <| .tactic tacticCode (← saveContext) kind delayOnMVars
-    return mvar
+  debug[byAsSorry] if ← isProp type then
+    return ← withRef tacticCode <| mkLabeledSorry type false (unique := true)
+  let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
+  let mvarId := mvar.mvarId!
+  let ref ← getRef
+  registerSyntheticMVar ref mvarId <| .tactic tacticCode (← saveContext) kind delayOnMVars
+  return mvar
 
 /--
   Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.

src/Lean/Meta/Check.lean

@@ -307,6 +307,7 @@ where
 
 /--
 Throw an exception if `e` is not type correct.
+Assumption: `e` has had its metavariables instantiated.
 -/
 def check (e : Expr) : MetaM Unit :=
   withTraceNode `Meta.check (fun res =>
@@ -319,6 +320,7 @@ def check (e : Expr) : MetaM Unit :=
 
 /--
 Return true if `e` is type correct.
+Assumption: `e` has had its metavariables instantiated.
 -/
 def isTypeCorrect (e : Expr) : MetaM Bool := do
   try
@@ -330,4 +332,37 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
 builtin_initialize
   registerTraceClass `Meta.check
 
+/-!
+### Consistency checks
+
+These are variants that check type correctness, for consistency checks.
+They avoid assigning metavariables or doing any other side effects.
+-/
+
+/--
+Consistency check: validates that `e` is type correct, without assigning metavariables.
+If the expected type is provided, verifies that `e` has that type.
+-/
+def validateTypeCorrect (e : Expr) (expectedType? : Option Expr := none) : MetaM Unit :=
+  withNewMCtxDepth do
+    prependError "validateTypeCorrect: expression is not type correct{indentExpr e}\nerror:" do
+      check (← instantiateMVars e)
+    if let some expectedType := expectedType? then
+      let ty ← prependError m!"validateTypeCorrect: could not infer type of{indentExpr e}\nerror:" do
+        inferType e
+      let b ← prependError m!"validateTypeCorrect: error when checking that type of{indentExpr e}\nis{indentExpr expectedType}\nerror:" do
+        isDefEq ty expectedType
+      unless b do
+        throwError "validateTypeCorrect: expression{indentExpr e}\n{← mkHasTypeButIsExpectedMsg ty expectedType}"
+
+/--
+Consistency check: validates that `e` is a sort. Does not validate type correctness.
+-/
+def validateIsSort (e : Expr) : MetaM Unit :=
+  withNewMCtxDepth do
+    let b ← prependError "validateIsSort: expression is not type correct{indentExpr e}\nerror:" do
+      Meta.isType e
+    unless b do
+      throwError "validateIsSort: expression is not a sort{indentExpr e}"
+
 end Lean.Meta

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

@@ -204,7 +204,7 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
   mkGoal mvarId params
 
 def main (mvarId : MVarId) (params : Params) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
-  if debug.terminalTacticsAsSorry.get (← getOptions) then
+  debug[terminalTacticsAsSorry] do
     mvarId.admit
     return {
         failure? := none, issues := [], config := params.config, trace := {}, counters := {}, simp := {}, splitDiags := {}

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

@@ -26,10 +26,9 @@ register_builtin_option backward.dsimp.proofs : Bool := {
     descr    := "Let `dsimp` simplify proof terms"
   }
 
-register_builtin_option debug.simp.check.have : Bool := {
-    defValue := false
-    descr    := "(simp) enable consistency checks for `have` telescope simplification"
-  }
+builtin_initialize
+  registerDebugClass `tactic.simp.check "(simp) enable consistency checks"
+  registerDebugClass `tactic.simp.check.have "(simp) enable consistency checks for `have` telescope simplification"
 
 builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
   registerInternalExceptionId `congrHypothesisFailed
@@ -624,9 +623,10 @@ def simpHaveTelescope (e : Expr) : SimpM Result := do
     assert! !info.haveInfo.isEmpty
     let (fixed, used) ← info.computeFixedUsed (keepUnused := !(← getConfig).zetaUnused)
     let r ← simpHaveTelescopeAux info fixed used e 0 (Array.mkEmpty info.haveInfo.size)
-    if r.modified && debug.simp.check.have.get (← getOptions) then
-      check r.expr
-      check r.proof
+    if r.modified then
+      debug[tactic.simp.check.have] do
+        validateTypeCorrect r.expr
+        validateTypeCorrect r.proof
     return (r.toResult info.level e, used, fixed, r.modified)
 where
   /-

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -225,12 +225,12 @@ where
         if inErasedSet thm then continue
         if rflOnly then
           unless thm.rfl do
-            if debug.tactic.simp.checkDefEqAttr.get (← getOptions) &&
-               backward.dsimp.useDefEqAttr.get (← getOptions) then
-              let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do
-                isRflProof thm.proof
-              if isRflOld then
-                logWarning m!"theorem {thm.proof} is no longer rfl"
+            debug[tactic.simp.check.defEqAttr] do
+              if backward.dsimp.useDefEqAttr.get (← getOptions) then
+                let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do
+                  isRflProof thm.proof
+                if isRflOld then
+                  logWarning m!"theorem {thm.proof} is no longer rfl"
             continue
         if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
           trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -45,12 +45,11 @@ register_builtin_option backward.dsimp.useDefEqAttr : Bool := {
     can be used in `dsimp` or with `implicitDefEqProofs`."
 }
 
-register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
-  defValue := false
-  descr    := "If true, whenever `dsimp` fails to apply a rewrite rule because it is not marked as \
-    `defeq`, check whether it would have been considered as a rfl theorem before the introduction \
-    of the `defeq` attribute, and warn if it was. Note that this is a costly check."
-}
+builtin_initialize
+  registerDebugClass `tactic.simp.check.defEqAttr
+    "If true, whenever `dsimp` fails to apply a rewrite rule because it is not marked as \
+     `defeq`, check whether it would have been considered as a rfl theorem before the introduction \
+     of the `defeq` attribute, and warn if it was. Note that this is a costly check."
 
 /--
 An `Origin` is an identifier for simp theorems which indicates roughly

src/Lean/Util.lean

@@ -21,6 +21,7 @@ public import Lean.Util.RecDepth
 public import Lean.Util.ShareCommon
 public import Lean.Util.Sorry
 public import Lean.Util.Trace
+public import Lean.Util.Debug
 public import Lean.Util.FindExpr
 public import Lean.Util.ReplaceExpr
 public import Lean.Util.ForEachExpr

src/Lean/Util/Debug.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+module
+
+prelude
+public import Lean.Util.Trace
+
+public section
+
+/-!
+# Simple debugging and consistency check framework
+
+During development it is useful to enable expensive consistency checks
+and sometimes even tweak behavior to stress test a component.
+
+It is useful to be able to conditionally enable these in a consistent way,
+and to leave them in for future use.
+
+Like trace messages, debugging classes can be enabled using
+`set_option debug.class.name true`.
+This enables code for `debug.class.name` as well as child classes
+that are explicitly marked as inherited (see `registerDebugClass`).
+
+This module provides the API to manage debugging classes and enabling debugging code.
+The key entry points are:
+- ``registerDebugClass `class.name`` registers a debugging class.
+- `Lean.isDebuggingEnabledFor` determines whether a debugging class is enabled.
+- `debug[class.name] doElem` is a `doElem` for conveniently making use of debugging classes in `do` notation.
+
+Try to follow these guidelines:
+1. **No heisenbugs.** Make sure debugging code avoids creating side effects,
+   unless the side effects are a documented intent.
+2. **Document the purpose.** Each debugging class should come with a description
+   that explains what consistency checks or side effects the class enables.
+3. **Good defaults.** Enabling a debug class for a module should enable reasonable
+   consistency checks, without needing to enable additional options.
+
+-/
+
+namespace Lean
+
+builtin_initialize inheritedDebugOptions : IO.Ref (Std.HashSet Name) ← IO.mkRef ∅
+
+class MonadDebug (m : Type → Type) where
+  /--
+  Like `MonadTrace`, should return the value of `inheritedDebugOptions.get`,
+  which does not change after initialization.
+  As `IO.Ref.get` may be too expensive on frequent and multi-threaded access,
+  the value may want to be cached, which is done in the stdlib in `CoreM`.
+  -/
+  getInheritedDebugOptions : m (Std.HashSet Name) := by exact inheritedDebugOptions.get
+
+instance (m n) [MonadLift m n] [MonadDebug m] : MonadDebug n where
+  getInheritedDebugOptions := liftM (MonadDebug.getInheritedDebugOptions : m _)
+
+variable {α : Type} {m : Type → Type} [Monad m] [MonadDebug m] [MonadOptions m] [MonadLiftT IO m]
+
+def checkDebugOption (inherited : Std.HashSet Name) (opts : Options) (cls : Name) : Bool :=
+  !opts.isEmpty && go (`debug ++ cls)
+where
+  go (opt : Name) : Bool :=
+    if let some enabled := opts.get? opt then
+      enabled
+    else if let .str parent _ := opt then
+      inherited.contains opt && go parent
+    else
+      false
+
+def isDebuggingEnabledFor (cls : Name) : m Bool := do
+  return checkDebugOption (← MonadDebug.getInheritedDebugOptions) (← getOptions) cls
+
+/--
+Registers a debug class.
+The `descr` option is used to create a `debug` option description of the form "enable/disable debugging option: {descr}".
+
+By default, debug classes are not inherited;
+that is, `set_option debug.foo true "descr"` does not imply `set_option debug.foo.bar true`.
+Calling ``registerDebugClass `foo.bar "descr" (inherited := true)`` enables this inheritance
+on an opt-in basis.
+-/
+def registerDebugClass (debugClassName : Name) (descr : String) (inherited := false) (defValue := false) (ref : Name := by exact decl_name%) : IO Unit := do
+  let optionName := `debug ++ debugClassName
+  registerOption optionName {
+    declName := ref
+    group := "debug"
+    defValue
+    descr := s!"enable/disable debugging option: {descr}"
+  }
+  if inherited then
+    inheritedDebugOptions.modify (·.insert optionName)
+
+def expandDebugMacro (id : Syntax) (d : TSyntax `doElem) : MacroM (TSyntax `doElem) := do
+  `(doElem| do
+    let cls := $(quote id.getId.eraseMacroScopes)
+    if (← Lean.isDebuggingEnabledFor cls) then
+      $d:doElem)
+
+macro "debug[" id:ident "]" d:doElem : doElem => do
+  expandDebugMacro id d
+
+end Lean

tests/lean/interactive/isRflParallel.lean

@@ -13,7 +13,7 @@ evaluated.
 -- set_option trace.Elab.block true
 set_option debug.skipKernelTC true
 set_option backward.dsimp.useDefEqAttr false
-set_option debug.tactic.simp.checkDefEqAttr false
+set_option debug.tactic.simp.check.defEqAttr false
 
 axiom testSorry : α
 

tests/lean/run/simpHave.lean

@@ -9,7 +9,7 @@ set_option linter.unusedSimpArgs false
 -- Enable simp consistency checks, so that the elaborator type checker is run on generated proofs.
 -- We want this so that we can verify that haves are "elaborator type correct",
 -- since the kernel does not check `nonDep`.
-set_option debug.simp.check.have true
+set_option debug.tactic.simp.check.have true
 -- To see the types of `have` binders for verification.
 set_option pp.letVarTypes true
 
@@ -615,7 +615,7 @@ example (n : Nat) (h : n = 190) : lp 20 0 = n := by
 -- set_option profiler true
 -- set_option profiler.threshold 2
 -- #time
-set_option debug.simp.check.have false in
+set_option debug.tactic.simp.check.have false in
 example (n : Nat) (h : n = 4950) : lp 100 0 = n := by
   simp -zeta -zetaUnused only [lp]
   simp -zeta only [Nat.zero_add]