feat: add unlock_limits command to disable all resource limits (#13211)

This PR adds an `unlock_limits` command that sets `maxHeartbeats`,
`maxRecDepth`, and `synthInstance.maxHeartbeats` to 0, disabling all
core resource limits. Also makes `maxRecDepth 0` mean "no limit"
(matching the existing behavior of `maxHeartbeats 0`).

src/Lean/Compiler/LCNF/Simp/SimpM.lean

@@ -146,7 +146,7 @@ Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in
 @[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepth
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/Elab/BuiltinCommand.lean

@@ -512,6 +512,15 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
+@[builtin_command_elab «unlock_limits»] def elabUnlockLimits : CommandElab := fun _ => do
+  let opts ← getOptions
+  let opts := maxHeartbeats.set opts 0
+  let opts := maxRecDepth.set opts 0
+  let opts := synthInstance.maxHeartbeats.set opts 0
+  modifyScope ({ · with opts })
+  -- update cached value as well
+  modify ({ · with maxRecDepth := 0 })
+
 open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>

src/Lean/Exception.lean

@@ -245,7 +245,7 @@ We use this combinator to prevent stack overflows.
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then
+  if max != 0 && curr == max then
     throwMaxRecDepthAt (← getRef)
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/Parser/Command.lean

@@ -648,6 +648,12 @@ only in a single term or tactic.
 -/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
+/--
+`unlock_limits` disables all built-in resource limit options (currently `maxRecDepth`,
+`maxHeartbeats`, and `synthInstance.maxHeartbeats`) in the current scope by setting them to 0.
+-/
+@[builtin_command_parser] def «unlock_limits» := leading_parser
+  "unlock_limits"
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser

src/Lean/Util/RecDepth.lean

@@ -14,7 +14,7 @@ namespace Lean
 
 register_builtin_option maxRecDepth : Nat := {
   defValue := defaultMaxRecDepth
-  descr    := "maximum recursion depth for many Lean procedures"
+  descr    := "maximum recursion depth for many Lean procedures, 0 means no limit"
 }
 
 end Lean

tests/elab/unlock_limits.lean

@@ -0,0 +1,11 @@
+module
+
+import Lean
+
+open Lean in
+unlock_limits in
+run_cmd do
+  let opts ← getOptions
+  assert! maxHeartbeats.get opts == 0
+  assert! maxRecDepth.get opts == 0
+  assert! opts.get? `synthInstance.maxHeartbeats == some (0 : Nat)