try_for

Stream: lean4 dev

[Mario Carneiro]

I assigned try_for to @Siddharth Bhat in Providence thinking it would be a simple tactic, but it turned out to be very complicated and https://github.com/leanprover/lean4/pull/1364 stalled. What is the status of this feature? Does it need special support from the compiler / interpreter? In short: how do you run programs with a timeout and cancel them later? How does the server handle this (surely it comes up already)?

[Siddharth Bhat]

@Mario Carneiro Here's the PR which tried to add the feature into the kernel: https://github.com/leanprover/lean4/pull/1364

I didn't have the cycles then to debug what was going wrong with some of the failing test cases [I suspected that perhaps the heartbeat counter was too low, now that we track a heartbeat "accurately". But this guess could be wildly off].

I closed the PR, with the intention of getting back to it post LLVM merge. That's currently dragging on figuring out why the windows build is broken :)