Open digama0 opened 6 months ago
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.
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.
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.
Okay, so can we have a try_for
tactic then? The spec for it is quite clear and this tactic is long overdue.
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: