merge lean-pr-testing-10204

Author: kim-em

Aesop/Check.lean

@@ -16,8 +16,7 @@ namespace Aesop
 initialize Check.all : Lean.Option Bool ←
   Option.register `aesop.check.all
     { defValue := false
-      descr := "(aesop) Enable all runtime checks. Individual checks can still be disabled."
-      group := "tactic" }
+      descr := "(aesop) Enable all runtime checks. Individual checks can still be disabled." }
 
 structure Check where
   toOption : Lean.Option Bool
@@ -42,7 +41,7 @@ end Check
 local macro "register_aesop_check_option" optName:ident descr:str : command =>
   `(initialize option : Lean.Option Bool ←
       Lean.Option.register $(quote $ `aesop.check ++ optName.getId)
-        { defValue := false, descr := $descr, group := "tactic" }
+        { defValue := false, descr := $descr }
 
     def $(mkIdent $ `Check ++ optName.getId) : Aesop.Check := ⟨option⟩)
 

Aesop/Stats/Basic.lean

@@ -18,7 +18,6 @@ namespace Aesop
 initialize collectStatsOption : Lean.Option Bool ←
   Lean.Option.register `aesop.collectStats {
     defValue := false
-    group := "aesop"
     descr := "(aesop) collect statistics about Aesop invocations. Use #aesop_stats to display the collected statistics."
   }
 

Aesop/Tracing.lean

@@ -25,7 +25,6 @@ def registerTraceOption (traceName : Name) (descr : String) :
     IO TraceOption := do
   let option ← Option.register (`trace.aesop ++ traceName) {
     defValue := false
-    group := "trace"
     descr
   }
   return { traceClass := `aesop ++ traceName, option }

Aesop/Util/Basic.lean

@@ -445,7 +445,6 @@ def elabPattern (stx : Syntax) : TermElabM Expr :=
 
 register_option aesop.smallErrorMessages : Bool := {
     defValue := false
-    group := "aesop"
     descr := "(aesop) Print smaller error messages. Used for testing."
   }
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4-pr-releases:pr-release-10204-faccc35
+leanprover/lean4:nightly-2025-11-27