set_option Not Working in Tactic Mode

[RexWzh]

When using the Lean REPL, set_option maxHeartbeats appears to have no effect in tactic mode, while it works correctly in command mode.

Minimal Working Example

Works in Command Mode:

{"cmd": "import Mathlib\n\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\n"}

{"cmd": "theorem mathd_numbertheory_314 (r n : ℕ) (h₀ : r = 1342 % 13) (h₁ : 0 < n) (h₂ : 1342 ∣ n)\n    (h₃ : n % 13 < r) : 6710 ≤ n := by\ncontrapose! h₃\ninterval_cases n <;> simp_all (config := {decide := true})", "env": 0}

Same proof in tactic mode fails:

{"cmd": "import Mathlib\n\nset_option maxHeartbeats 0\nset_option maxRecDepth 1000000\n"}

{"cmd": "theorem mathd_numbertheory_314 (r n : ℕ) (h₀ : r = 1342 % 13) (h₁ : 0 < n) (h₂ : 1342 ∣ n)\n    (h₃ : n % 13 < r) : 6710 ≤ n := by sorry", "env": 0}

{"tactic": "contrapose! h₃", "proofState": 0}

{"tactic": "interval_cases n <;> simp_all (config := {decide := true})", "proofState": 1}

Error message:

{"message": "Lean error:\n(deterministic) timeout at `elaborator`, maximum number of heartbeats (200000) has been reached\nUse `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)"}

What I've Tried

1. Verify in the lean:

import Mathlib
set_option maxHeartbeats 0
set_option maxRecDepth 1000000
theorem mathd_numbertheory_314 (r n : ℕ) (h₀ : r = 1342 % 13) (h₁ : 0 < n) (h₂ : 1342 ∣ n)
    (h₃ : n % 13 < r) : 6710 ≤ n := by
contrapose! h₃
interval_cases n <;> simp_all (config := {decide := true})

lake env lean mathd_numbertheory_314.lean

2. Test set_option in command mode:

   • remove set_option maxHeartbeats 0: raise the same error with heartbeats (200000)
   • lower the number to set_option maxHeartbeats 100000: raise error with heartbeats (100000)

3. Test set_option in tactic mode:

   • remove set_option maxHeartbeats 0: raise the same error with heartbeats (200000)
   • lower the number set_option maxHeartbeats 100000: raise the same error with heartbeats (200000)
   • set set_option maxHeartbeats 0 and set_option maxRecDepth 300000: raise the same error with heartbeats (200000)
   • specify "env" in the tactic mode(the same error)