How to set tactic timeout in Lean 4?

Stream: lean4

[Kaiyu Yang]

Hi,

I'm wondering if there is an equivalent of Lean 3's try_for_time tactic in Lean 4. Thank you!

[Scott Morrison]

Perhaps set_option maxHeartbeats ... in ... is useful? It is measured in "heartbeats" rather than seconds, and is a command, rather than a tactic combinator, but we can probably make something work.

[Mario Carneiro]

No, there is no equivalent of try_for and this is a big problem. There is a way to control the global heartbeat limit but it just causes a low level failure that can't be caught reliably. I don't think the situation has changed appreciably since lean4#1364

[Kaiyu Yang]

Thank you Mario and Scott!

[Kaiyu Yang]

The heartbeat is like a (deterministic) timeout for the entire module instead of a tactic?

[Scott Morrison]

Yes, the heartbeat counter provided in core counts up across the whole module. See src4#getRemainingHeartbeats for some helper functions.