`try_for` tactic (timeouts in tactics)

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

Start by examining the CoreM heartbeat counter and the separate C++ heartbeat counter, then review the history referenced by issue #1364 to understand why previous timeout attempts failed. Use the provided try_for example as the behavioral target, including aborting an over-limit tactic and allowing one within the limit.