fix: correctly set initHeartbeats in Lean.Environment.unsafeRunMetaM

[eric-wieser]

This PR ensures that Lean.Environment.unsafeRunMetaM can be run late in a lean process, without thinking it has already consumed all available heartbeats.

[eric-wieser]

changelog-library

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd5329126bed2c921d53daf1919de58977116e51 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 23:14:10)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fd5329126bed2c921d53daf1919de58977116e51 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 23:14:12)

[fiforeach]

Thanks for this.

With this change maxHeartbeats gets a special treatment. Are there other options that one might reasonably be expected to be passed to the sub-execution? Are there reasons not to pass all options that were set?

[eric-wieser]

With this change maxHeartbeats gets a special treatment.

I'm passing initHeartbeats, not maxHeartbeats

Are there reasons not to pass all options that were set?

initHeartbeats is state, not an option.

[fiforeach]

I see.

So do I understand correctly that this will initialize the "sub execution" to continue with a potentially nonzero initial value of heartbeats, potentially causing the maximum to be reached even earlier than previously?

[eric-wieser]

No, the opposite; when code does a heartbeat check, it asserts that getNumHeartbeats <= initHeartbeats + limit. For this to make sense, initHeartbeats needs to be initialized at the point where the relevant code begins, else the limit will instead be enforced from when Lean started up.

[Kha]

Thanks but I'm relatively sure we want #13202 instead (perhaps it doesn't even matter in practice)

[eric-wieser]

I think you do need this one, else a callback that does change the heartbeat limit will not count it correctly.