From be505b80504b34f1298c734a97ecfc3af2d06a68 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 28 Mar 2025 19:06:43 -0700 Subject: [PATCH] feat: Run cancel token with timeout --- Pantograph/Library.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index b060275..aa7c42d 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -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