feat: Run cancel token with timeout
This commit is contained in:
parent
48485a868b
commit
be505b8050
|
@ -3,7 +3,10 @@ import Pantograph.Goal
|
|||
import Pantograph.Protocol
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Version
|
||||
|
||||
import Lean
|
||||
import Std.Time
|
||||
import Std.Internal.Async
|
||||
|
||||
namespace Lean
|
||||
|
||||
|
@ -212,4 +215,12 @@ def goalConvExit (state: GoalState): CoreM TacticResult :=
|
|||
def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryCalc goal pred
|
||||
|
||||
-- Cancel the token after a timeout.
|
||||
@[export pantograph_run_cancel_token_with_timeout_m]
|
||||
def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : Std.Time.Millisecond.Offset) : IO Unit := do
|
||||
let _ ← EIO.asTask do
|
||||
let () ← (← Std.Internal.IO.Async.sleep timeout).block
|
||||
cancelToken.set
|
||||
return ()
|
||||
|
||||
end Pantograph
|
||||
|
|
Loading…
Reference in New Issue