f11d137a30
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`).
11 lines
229 B
Text
11 lines
229 B
Text
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)
|