chore: do not set unused Option.Decl.group (#11307)

nomeata · web-flow · commit 4288aa71e0f6 · 2025-11-21T16:44:38.000Z
This PR removes all code that sets the `Option.Decl.group` field, which is unused and has no clearly documented meaning. The actual removal of the field would be #11305.
diff --git a/src/Lean/Compiler/LCNF/ConfigOptions.lean b/src/Lean/Compiler/LCNF/ConfigOptions.lean
@@ -43,31 +43,26 @@ structure ConfigOptions where
 
 register_builtin_option compiler.small : Nat := {
   defValue := 1
-  group    := "compiler"
   descr    := "(compiler) function declarations with size `≤ small` is inlined even if there are multiple occurrences."
 }
 
 register_builtin_option compiler.maxRecInline : Nat := {
   defValue := 1
-  group    := "compiler"
   descr    := "(compiler) maximum number of times a recursive definition tagged with `[inline]` can be recursively inlined before generating an error during compilation."
 }
 
 register_builtin_option compiler.maxRecInlineIfReduce : Nat := {
   defValue := 16
-  group    := "compiler"
   descr    := "(compiler) maximum number of times a recursive definition tagged with `[inline_if_reduce]` can be recursively inlined before generating an error during compilation."
 }
 
 register_builtin_option compiler.checkTypes : Bool := {
   defValue := false
-  group    := "compiler"
   descr    := "(compiler) perform type compatibility checking after each compiler pass. Note this is not a complete check, and it is used only for debugging purposes. It fails in code that makes heavy use of dependent types."
 }
 
 register_builtin_option compiler.extract_closed : Bool := {
   defValue := true
-  group    := "compiler"
   descr    := "(compiler) enable/disable closed term caching"
 }
 
diff --git a/src/Lean/Compiler/Options.lean b/src/Lean/Compiler/Options.lean
@@ -14,7 +14,6 @@ namespace Lean.Compiler
 
 register_builtin_option compiler.check : Bool := {
   defValue := false
-  group    := "compiler"
   descr    := "type check code after each compiler step (this is useful for debugging purses)"
 }
 
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
@@ -15,13 +15,11 @@ public section
 namespace Lean
 register_builtin_option diagnostics : Bool := {
   defValue := false
-  group    := "diagnostics"
   descr    := "collect diagnostic information"
 }
 
 register_builtin_option diagnostics.threshold : Nat := {
   defValue := 20
-  group    := "diagnostics"
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
 }
 
@@ -454,7 +452,6 @@ the exception has been thrown.
 
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
-  group    := "debug"
   descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
 }
 
@@ -560,7 +557,6 @@ def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelT
 /-- Option for capturing output to stderr during elaboration. -/
 register_builtin_option stderrAsMessages : Bool := {
   defValue := true
-  group    := "server"
   descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
 }
 
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
@@ -66,7 +66,6 @@ deriving Inhabited
 register_builtin_option doc.verso : Bool := {
   defValue := false,
   descr := "whether to use Verso syntax in docstrings"
-  group := "doc"
 }
 
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
@@ -1161,7 +1161,6 @@ If `true`, suggestions are provided for code elements.
 register_builtin_option doc.verso.suggestions : Bool := {
   defValue := true
   descr := "whether to provide suggestions for code elements"
-  group := "doc"
 }
 
 -- Normally, name suggestions should be provided relative to the current scope. But
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
@@ -482,7 +482,6 @@ register_builtin_option linter.unusedSectionVars : Bool := {
 
 register_builtin_option debug.proofAsSorry : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "replace the bodies (proofs) of theorems with `sorry`"
 }
 
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
@@ -54,7 +54,6 @@ register_builtin_option inductive.autoPromoteIndices : Bool := {
 
 register_builtin_option bootstrap.inductiveCheckResultingUniverse : Bool := {
   defValue := true,
-  group    := "bootstrap",
   descr    := "by default the `inductive`/`structure` commands report an error if the resulting universe is not zero, \
     but may be zero for some universe parameters. Reason: unless this type is a subsingleton, \
     it is hardly what the user wants since it can only eliminate into `Prop`. \
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -142,7 +142,6 @@ private def compileDecl (decl : Declaration) : TermElabM Unit := do
 
 register_builtin_option diagnostics.threshold.proofSize : Nat := {
   defValue := 16384
-  group    := "diagnostics"
   descr    := "only display proof statistics when proof has at least this number of terms"
 }
 
diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
@@ -19,7 +19,6 @@ builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
 
 register_builtin_option mvcgen.warning : Bool := {
   defValue := true
-  group    := "debug"
   descr    := "disable `mvcgen` usage warning"
 }
 
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
@@ -16,7 +16,6 @@ public section
 
 register_builtin_option tactic.customEliminators : Bool := {
   defValue := true
-  group    := "tactic"
   descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
     defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
 }
@@ -977,7 +976,6 @@ def evalInduction : Tactic := fun stx =>
 
 register_builtin_option tactic.fun_induction.unfolding : Bool := {
   defValue := true
-  group    := "tactic"
   descr    := "if set to 'true', then 'fun_induction' and 'fun_cases' will use the “unfolding \
     functional induction (resp. cases) principle” ('….induct_unfolding'/'….fun_cases_unfolding'), \
     which will attempt to replace the function goal of interest in the goal with the appropriate \
diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean
@@ -1329,7 +1329,6 @@ def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDec
 
 register_builtin_option debug.byAsSorry : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
 }
 
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
@@ -64,7 +64,6 @@ def getBetterRef (ref : Syntax) (macroStack : MacroStack) : Syntax :=
 
 register_builtin_option pp.macroStack : Bool := {
   defValue := false
-  group    := "pp"
   descr    := "display macro expansion stack"
 }
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
@@ -71,7 +71,6 @@ paths back together.
 namespace Lean
 register_builtin_option debug.skipKernelTC : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
 }
 
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
@@ -69,7 +69,6 @@ private def mkInaccessibleUserName (unicode : Bool) : Name → Name
 
 register_builtin_option pp.sanitizeNames : Bool := {
   defValue := true
-  group    := "pp"
   descr    := "add suffix to shadowed/inaccessible variables when pretty printing"
 }
 
diff --git a/src/Lean/Linter/Sets.lean b/src/Lean/Linter/Sets.lean
@@ -22,7 +22,6 @@ meta def registerSet (setName : Name) (ref : Name := by exact decl_name%) : IO (
   registerOption setName {
     declName := ref
     defValue := false
-    group := "linterSet"
     descr := ""
   }
   return { name := setName, defValue := false }
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
@@ -15,13 +15,11 @@ namespace Lean.Meta
 
 register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "use lazy delta reduction when solving unification constrains of the form `(f a).i =?= (g b).i`"
 }
 
 register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
 }
 
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
@@ -1002,7 +1002,6 @@ private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (O
 /- See comment at `mkMatcher` before `mkAuxDefinition` -/
 register_builtin_option bootstrap.genMatcherCode : Bool := {
   defValue := true
-  group := "bootstrap"
   descr := "disable code generation for auxiliary matcher function"
 }
 
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
@@ -14,37 +14,31 @@ namespace Lean.Meta
 
 register_builtin_option pp.auxDecls : Bool := {
   defValue := false
-  group    := "pp"
   descr    := "display auxiliary declarations used to compile recursive functions"
 }
 
 register_builtin_option pp.implementationDetailHyps : Bool := {
   defValue := false
-  group    := "pp"
   descr    := "display implementation detail hypotheses in the local context"
 }
 
 register_builtin_option pp.inaccessibleNames : Bool := {
   defValue := true
-  group    := "pp"
   descr    := "display inaccessible declarations in the local context"
 }
 
 register_builtin_option pp.showLetValues : Bool := {
   defValue := false
-  group    := "pp"
   descr    := "always display let-declaration values in the info view"
 }
 
 register_builtin_option pp.showLetValues.threshold : Nat := {
   defValue := 0
-  group    := "pp"
   descr    := "when `pp.showLetValues` is false, the maximum size of a term allowed before it is replaced by `⋯`"
 }
 
 register_builtin_option pp.showLetValues.tactic.threshold : Nat := {
   defValue := 255
-  group    := "pp"
   descr    := "when `pp.showLetValues` is false, the maximum size of a term allowed before it is replaced by `⋯`, for tactic goals"
 }
 
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
@@ -29,7 +29,6 @@ register_builtin_option synthInstance.maxSize : Nat := {
 
 register_builtin_option backward.synthInstance.canonInstances : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
 }
 
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -1087,13 +1087,11 @@ where
 
 register_builtin_option backward.grind.inferPattern : Bool := {
   defValue := false
-  group    := "backward compatibility"
   descr    := "use old E-matching pattern inference"
 }
 
 register_builtin_option backward.grind.checkInferPatternDiscrepancy : Bool := {
   defValue := false
-  group    := "backward compatibility"
   descr    := "check whether old and new pattern inference procedures infer the same pattern"
 }
 
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -73,19 +73,16 @@ def isInterpreted (e : Expr) : MetaM Bool := do
 
 register_builtin_option grind.debug : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "check invariants after updates"
 }
 
 register_builtin_option grind.debug.proofs : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "check proofs between the elements of all equivalence classes"
 }
 
 register_builtin_option grind.warning : Bool := {
   defValue := false
-  group    := "debug"
   descr    := "generate a warning whenever `grind` is used"
 }
 
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
@@ -77,7 +77,6 @@ namespace Lean.Meta
 
 register_builtin_option tactic.hygienic : Bool := {
   defValue := true
-  group    := "tactic"
   descr    := "make sure tactics are hygienic"
 }
 
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -336,7 +336,6 @@ def dsimprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM DSte
 
 register_builtin_option simprocs : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "Enable/disable `simproc`s (simplification procedures)."
 }
 
diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean
@@ -133,7 +133,6 @@ private partial def findIfToSplit? (e : Expr) : MetaM (Option (Expr × Expr)) :=
 
 register_builtin_option backward.split : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "use the old semantics for the `split` tactic where nested `if-then-else` terms could be simplified too"
 }
 
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
@@ -16,7 +16,6 @@ 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"
 }
 
@@ -175,7 +174,6 @@ def _root_.Lean.MVarId.isSubsingleton (g : MVarId) : MetaM Bool := do
 
 register_builtin_option tactic.skipAssignedInstances : Bool := {
   defValue := true
-  group    := "backward compatibility"
   descr    := "in the `rw` and `simp` tactics, if an instance implicit argument is assigned, do not try to synthesize instance."
 }
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
@@ -380,7 +380,6 @@ opaque evalParserConst (declName : Name) : ParserFn
 
 register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
   defValue := false
-  group    := "internal"
   descr    := "(Lean bootstrapping) use parsers from the current stage inside quotations"
 }
 
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
@@ -33,7 +33,6 @@ def ppUsing (e : Expr) (delab : Expr → MetaM Term) : MetaM Format := do
 
 register_builtin_option pp.exprSizes : Bool := {
   defValue := false
-  group    := "pp"
   descr    := "(pretty printer) prefix each embedded expression with its sizes in the format \
     (size disregarding sharing/size with sharing/size with max sharing)"
 }
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
diff --git a/src/Lean/Util/Profile.lean b/src/Lean/Util/Profile.lean
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean

Original file line number	Diff line number	Diff line change
`@@ -43,31 +43,26 @@ structure ConfigOptions where`
`43`	`43`
`44`	`44`	`register_builtin_option compiler.small : Nat := {`
`45`	`45`	`defValue := 1`
`46`		`- group := "compiler"`
`47`	`46`	descr := "(compiler) function declarations with size `≤ small` is inlined even if there are multiple occurrences."
`48`	`47`	`}`
`49`	`48`
`50`	`49`	`register_builtin_option compiler.maxRecInline : Nat := {`
`51`	`50`	`defValue := 1`
`52`		`- group := "compiler"`
`53`	`51`	descr := "(compiler) maximum number of times a recursive definition tagged with `[inline]` can be recursively inlined before generating an error during compilation."
`54`	`52`	`}`
`55`	`53`
`56`	`54`	`register_builtin_option compiler.maxRecInlineIfReduce : Nat := {`
`57`	`55`	`defValue := 16`
`58`		`- group := "compiler"`
`59`	`56`	descr := "(compiler) maximum number of times a recursive definition tagged with `[inline_if_reduce]` can be recursively inlined before generating an error during compilation."
`60`	`57`	`}`
`61`	`58`
`62`	`59`	`register_builtin_option compiler.checkTypes : Bool := {`
`63`	`60`	`defValue := false`
`64`		`- group := "compiler"`
`65`	`61`	`descr := "(compiler) perform type compatibility checking after each compiler pass. Note this is not a complete check, and it is used only for debugging purposes. It fails in code that makes heavy use of dependent types."`
`66`	`62`	`}`
`67`	`63`
`68`	`64`	`register_builtin_option compiler.extract_closed : Bool := {`
`69`	`65`	`defValue := true`
`70`		`- group := "compiler"`
`71`	`66`	`descr := "(compiler) enable/disable closed term caching"`
`72`	`67`	`}`
`73`	`68`
Original file line number	Diff line number	Diff line change
`@@ -14,7 +14,6 @@ namespace Lean.Compiler`
`14`	`14`
`15`	`15`	`register_builtin_option compiler.check : Bool := {`
`16`	`16`	`defValue := false`
`17`		`- group := "compiler"`
`18`	`17`	`descr := "type check code after each compiler step (this is useful for debugging purses)"`
`19`	`18`	`}`
`20`	`19`
Original file line number	Diff line number	Diff line change
`@@ -15,13 +15,11 @@ public section`
`15`	`15`	`namespace Lean`
`16`	`16`	`register_builtin_option diagnostics : Bool := {`
`17`	`17`	`defValue := false`
`18`		`- group := "diagnostics"`
`19`	`18`	`descr := "collect diagnostic information"`
`20`	`19`	`}`
`21`	`20`
`22`	`21`	`register_builtin_option diagnostics.threshold : Nat := {`
`23`	`22`	`defValue := 20`
`24`		`- group := "diagnostics"`
`25`	`23`	`descr := "only diagnostic counters above this threshold are reported by the definitional equality"`
`26`	`24`	`}`
`27`	`25`
`@@ -454,7 +452,6 @@ the exception has been thrown.`
`454`	`452`
`455`	`453`	`register_builtin_option debug.moduleNameAtTimeout : Bool := {`
`456`	`454`	`defValue := true`
`457`		`- group := "debug"`
`458`	`455`	`descr := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"`
`459`	`456`	`}`
`460`	`457`
`@@ -560,7 +557,6 @@ def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelT`
`560`	`557`	`/-- Option for capturing output to stderr during elaboration. -/`
`561`	`558`	`register_builtin_option stderrAsMessages : Bool := {`
`562`	`559`	`defValue := true`
`563`		`- group := "server"`
`564`	`560`	descr := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
`565`	`561`	`}`
`566`	`562`
Original file line number	Diff line number	Diff line change
`@@ -66,7 +66,6 @@ deriving Inhabited`
`66`	`66`	`register_builtin_option doc.verso : Bool := {`
`67`	`67`	`defValue := false,`
`68`	`68`	`descr := "whether to use Verso syntax in docstrings"`
`69`		`- group := "doc"`
`70`	`69`	`}`
`71`	`70`
`72`	`71`	`private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}`
Original file line number	Diff line number	Diff line change
@@ -1161,7 +1161,6 @@ If `true`, suggestions are provided for code elements.
`1161`	`1161`	`register_builtin_option doc.verso.suggestions : Bool := {`
`1162`	`1162`	`defValue := true`
`1163`	`1163`	`descr := "whether to provide suggestions for code elements"`
`1164`		`- group := "doc"`
`1165`	`1164`	`}`
`1166`	`1165`
`1167`	`1166`	`-- Normally, name suggestions should be provided relative to the current scope. But`
Original file line number	Diff line number	Diff line change
`@@ -482,7 +482,6 @@ register_builtin_option linter.unusedSectionVars : Bool := {`
`482`	`482`
`483`	`483`	`register_builtin_option debug.proofAsSorry : Bool := {`
`484`	`484`	`defValue := false`
`485`		`- group := "debug"`
`486`	`485`	descr := "replace the bodies (proofs) of theorems with `sorry`"
`487`	`486`	`}`
`488`	`487`
Original file line number	Diff line number	Diff line change
`@@ -142,7 +142,6 @@ private def compileDecl (decl : Declaration) : TermElabM Unit := do`
`142`	`142`
`143`	`143`	`register_builtin_option diagnostics.threshold.proofSize : Nat := {`
`144`	`144`	`defValue := 16384`
`145`		`- group := "diagnostics"`
`146`	`145`	`descr := "only display proof statistics when proof has at least this number of terms"`
`147`	`146`	`}`
`148`	`147`
Original file line number	Diff line number	Diff line change
@@ -19,7 +19,6 @@ builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
`19`	`19`
`20`	`20`	`register_builtin_option mvcgen.warning : Bool := {`
`21`	`21`	`defValue := true`
`22`		`- group := "debug"`
`23`	`22`	descr := "disable `mvcgen` usage warning"
`24`	`23`	`}`
`25`	`24`