Zulip Chat Archive

Stream: lean4 dev

Topic: try_for


Mario Carneiro (Sep 22 2022 at 22:51):

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 (Sep 23 2022 at 09:36):

@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 :)


Last updated: Dec 20 2023 at 11:08 UTC