Execute monad with timeout

Stream: lean4

[Leni Aniva]

Is there a simple way to run a monad based on CoreM with a timeout?

e.g.

def runWithTimeout (t: Nat) (m: CoreM a): CoreM (Except Timeout a) := ...

where runWithTimeout t m would return .ok a if the monad finished in time, and otherwise .error with some timeout object.

I know there's a field for max heartbeats, but can I just use withCoreContext { maxHeartbeats := ... } to achieve this effect?

[Mario Carneiro]

no, this is a long standing open issue

[Mario Carneiro]

lean4#3812

[Sebastian Ullrich]

Leni Aniva said:

I know there's a field for max heartbeats, but can I just use withCoreContext { maxHeartbeats := ... } to achieve this effect?

Yes, that should work as it is effectively what the Lean elaborator does. Someone in the called code just has to call Core.checkSystem sufficiently often, which all the fundamental meta functions do

[Eric Wieser]

Could we have a MonadCheckSystem typeclass to make it possible to generalize this? Is there a version of checkSystem for CommandElabM?

import Lean
run_cmd do
  Lean.Core.checkSystem "foo" -- fails, wrong type

[Eric Wieser]

(the actual application I have in mind is being able to create a no-op implementation of MonadCheckSystem Id, so that you can write a function and prove things about it for m := Id, but then invoke it with interruptibility with m := CoreM)

[Sebastian Ullrich]

That sounds like something that would be best to introduce locally in your project for now :) . CoreM is currently the only core monad with any heartbeats concept.

[Leni Aniva]

Mario Carneiro said:

no, this is a long standing open issue

that issue refers to the frontend interface. If I just want to run some random TermElabM with a timeout I could just use a heartbeat, right?

[Eric Wieser]

CoreM is currently the only core monad with any heartbeats concept.

I now remember that I wanted to abstract over docs#IO.checkCanceled as well

[Eric Wieser]

The context is #16666, where it would be better if the gaussian elimination algorithm used by linarith didn't have to live in CoreM