`try_for` tactic (timeouts in tactics)

[digama0]

The situation does not seem to have changed since #1364 , but there is no current issue tracking this so I thought I would open this so we don't forget. There is currently no equivalent of the try_for tactic from lean 3, which amounts to a metaprogramming API which allows you to abort a tactic call if a heartbeat limit is exceeded. CoreM has a heartbeat counter, and there is also a (unrelated?) heartbeat counter in the C++ code, but attempts to hook these up into a reliable timeout mechanism appear to have failed.

Desired behavior:

example : True := by
  -- Note, this may not actually work as a test case 
  -- since `try_for` counts heartbeats and `sleep` counts ms. 
  -- Substitute any expensive tactic for a better test
  fail_if_success try_for 100 (sleep 1000)
  try_for 10000 (sleep 1000)
  trivial

[Kha]

It is not clear to me what this issue is asking for. checkHeartbeats has existed and been used since basically the beginning afaics, and the kernel integration (why is that relevant for tactics?) was done in #4113. If a specific try_for tactic is desired, a more focused RFC should be opened.

[digama0]

This is about interrupting computations which are taking too long, either by making sure that there are checkHeartbeats checks literally everywhere or having some preemptive threading primitive (which is what we had in lean 3) where we can just cause arbitrary lean code to yield a timeout exception using runtime integration of some kind.

[Kha]

CoreM implements cooperative preemption via heartbeats and cancellation tokens, which we check in all the fundamental meta and kernel functions. This is unlikely to materially change.

[digama0]

Okay, so can we have a try_for tactic then? The spec for it is quite clear and this tactic is long overdue.

[nomeata]

Does this need changes in core APIs or would it be possible to implement that (say in batteries) already now?

[lenianiva]

Does this need changes in core APIs or would it be possible to implement that (say in batteries) already now?

We can probably implement this now as an independent tactic