From c4d9d2ada3201642bbcd24f64e2e63c0f948080c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:33 +0200 Subject: [PATCH 1/2] Implement timeout option --- REPL/JSON.lean | 19 +++++++++++----- REPL/Main.lean | 35 ++++++++++++++++++++++------- test/timeout.expected.out | 46 +++++++++++++++++++++++++++++++++++++++ test/timeout.in | 15 +++++++++++++ 4 files changed, 101 insertions(+), 14 deletions(-) create mode 100644 test/timeout.expected.out create mode 100644 test/timeout.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..6f90e2ee 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -11,7 +11,14 @@ open Lean Elab InfoTree namespace REPL -structure CommandOptions where +/-- Base structure with timeout that all command types can inherit from -/ +structure BaseOptions where + /-- + Optional timeout in milliseconds. If none, no timeout will be applied. + -/ + timeout : Option Nat := none + +structure CommandOptions extends BaseOptions where allTactics : Option Bool := none rootGoals : Option Bool := none /-- @@ -38,7 +45,7 @@ deriving ToJson, FromJson /-- Run a tactic in a proof state. -/ -structure ProofStep where +structure ProofStep extends BaseOptions where proofState : Nat tactic : String deriving ToJson, FromJson @@ -170,21 +177,21 @@ structure Error where message : String deriving ToJson, FromJson -structure PickleEnvironment where +structure PickleEnvironment extends BaseOptions where env : Nat pickleTo : System.FilePath deriving ToJson, FromJson -structure UnpickleEnvironment where +structure UnpickleEnvironment extends BaseOptions where unpickleEnvFrom : System.FilePath deriving ToJson, FromJson -structure PickleProofState where +structure PickleProofState extends BaseOptions where proofState : Nat pickleTo : System.FilePath deriving ToJson, FromJson -structure UnpickleProofState where +structure UnpickleProofState extends BaseOptions where unpickleProofStateFrom : System.FilePath env : Option Nat deriving ToJson, FromJson diff --git a/REPL/Main.lean b/REPL/Main.lean index d181080f..f790f275 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -362,6 +362,23 @@ def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do catch ex => return .inr ⟨"Lean error:\n" ++ ex.toString⟩ +/-- +Run a task with an optional timeout in milliseconds. +-/ +def runWithTimeout (timeout? : Option Nat) (task : M IO α) : M IO α := + match timeout? with + | none => task + | some timeout => do + let jobTask ← IO.asTask (prio := .dedicated) (StateT.run task (← get)) + let timeoutTask : IO (α × State) := do + IO.sleep timeout.toUInt32 + throw <| IO.userError s!"Operation timed out after {timeout}ms" + match ← IO.waitAny [jobTask, ← IO.asTask timeoutTask] with + | .ok (a, state) => do + modify fun _ => state + return a + | .error e => throw e + end REPL open REPL @@ -426,14 +443,16 @@ where loop : M IO Unit := do if query = "" then return () if query.startsWith "#" || query.startsWith "--" then loop else - IO.println <| toString <| ← match ← parse query with - | .command r => return toJson (← runCommand r) - | .file r => return toJson (← processFile r) - | .proofStep r => return toJson (← runProofStep r) - | .pickleEnvironment r => return toJson (← pickleCommandSnapshot r) - | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) - | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) - | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) + IO.println <| toString <| ← try + match ← parse query with + | .command r => return toJson (← runWithTimeout r.timeout (runCommand r)) + | .file r => return toJson (← runWithTimeout r.timeout (processFile r)) + | .proofStep r => return toJson (← runWithTimeout r.timeout (runProofStep r)) + | .pickleEnvironment r => return toJson (← runWithTimeout r.timeout (pickleCommandSnapshot r)) + | .unpickleEnvironment r => return toJson (← runWithTimeout r.timeout (unpickleCommandSnapshot r)) + | .pickleProofSnapshot r => return toJson (← runWithTimeout r.timeout (pickleProofSnapshot r)) + | .unpickleProofSnapshot r => return toJson (← runWithTimeout r.timeout (unpickleProofSnapshot r)) + catch e => return toJson (⟨e.toString⟩ : Error) printFlush "\n" -- easier to parse the output if there are blank lines loop diff --git a/test/timeout.expected.out b/test/timeout.expected.out new file mode 100644 index 00000000..64c2d6a3 --- /dev/null +++ b/test/timeout.expected.out @@ -0,0 +1,46 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 49}, + "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2", + "endPos": {"line": 1, "column": 54}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"sorries": + [{"proofState": 2, + "pos": {"line": 1, "column": 49}, + "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2", + "endPos": {"line": 1, "column": 54}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + +{"message": "Operation timed out after 1ms"} + +{"message": "Unknown proof state."} + +{"sorries": + [{"proofState": 4, + "pos": {"line": 1, "column": 49}, + "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2", + "endPos": {"line": 1, "column": 54}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, + "data": "declaration uses 'sorry'"}], + "env": 2} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + diff --git a/test/timeout.in b/test/timeout.in new file mode 100644 index 00000000..a774932b --- /dev/null +++ b/test/timeout.in @@ -0,0 +1,15 @@ +{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry"} + +{"tactic": "assumption", "proofState": 0} + +{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry", "timeout": 1000} + +{"tactic": "assumption", "proofState": 2} + +{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry", "timeout": 1} + +{"tactic": "assumption", "proofState": 4} + +{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry"} + +{"tactic": "assumption", "proofState": 4} From 5abeb587a6863edeec6f74ab871ce8172defb26f Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:33 +0200 Subject: [PATCH 2/2] Add task cancellation --- REPL/JSON.lean | 3 ++- REPL/Main.lean | 10 ++++--- .../test/long_kernel_check.expected.out | 27 +++++++++++++++++++ test/Mathlib/test/long_kernel_check.in | 6 +++++ test/timeout.expected.out | 2 +- 5 files changed, 43 insertions(+), 5 deletions(-) create mode 100644 test/Mathlib/test/long_kernel_check.expected.out create mode 100644 test/Mathlib/test/long_kernel_check.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 6f90e2ee..60aa48b8 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -14,7 +14,8 @@ namespace REPL /-- Base structure with timeout that all command types can inherit from -/ structure BaseOptions where /-- - Optional timeout in milliseconds. If none, no timeout will be applied. + Optional soft timeout in milliseconds. If none, no timeout will be applied. + If the timeout is reached, an attempt will be made to interrupt the process. -/ timeout : Option Nat := none diff --git a/REPL/Main.lean b/REPL/Main.lean index f790f275..2847228e 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -372,12 +372,16 @@ def runWithTimeout (timeout? : Option Nat) (task : M IO α) : M IO α := let jobTask ← IO.asTask (prio := .dedicated) (StateT.run task (← get)) let timeoutTask : IO (α × State) := do IO.sleep timeout.toUInt32 - throw <| IO.userError s!"Operation timed out after {timeout}ms" - match ← IO.waitAny [jobTask, ← IO.asTask timeoutTask] with + throw <| IO.userError s!"Operation timed out" + let timeoutTask ← IO.asTask timeoutTask + match ← IO.waitAny [jobTask, timeoutTask] with | .ok (a, state) => do + IO.cancel timeoutTask modify fun _ => state return a - | .error e => throw e + | .error e => + IO.cancel jobTask + throw e end REPL diff --git a/test/Mathlib/test/long_kernel_check.expected.out b/test/Mathlib/test/long_kernel_check.expected.out new file mode 100644 index 00000000..2176aeb5 --- /dev/null +++ b/test/Mathlib/test/long_kernel_check.expected.out @@ -0,0 +1,27 @@ +{"env": 0} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 2, "column": 83}, + "goal": + "u v : ℕ → ℕ\nh₀ : ∀ (n : ℕ), u n = 2 * n + 2\nh₁ : ∀ (n : ℕ), v n = 2 * n + 1\n⊢ ∑ k ∈ Finset.range 2003, u k - ∑ k ∈ Finset.range 2003, v k = 2003", + "endPos": {"line": 2, "column": 88}}], + "messages": + [{"severity": "info", + "pos": {"line": 2, "column": 6}, + "endPos": {"line": 2, "column": 7}, + "data": + "The '∑ x in s, f x' notation is deprecated: please use '∑ x ∈ s, f x' instead:\n∑ k ∈ Finset.range 2003, u k"}, + {"severity": "info", + "pos": {"line": 2, "column": 39}, + "endPos": {"line": 2, "column": 40}, + "data": + "The '∑ x in s, f x' notation is deprecated: please use '∑ x ∈ s, f x' instead:\n∑ k ∈ Finset.range 2003, v k"}, + {"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 22}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"message": "Operation timed out"} + diff --git a/test/Mathlib/test/long_kernel_check.in b/test/Mathlib/test/long_kernel_check.in new file mode 100644 index 00000000..df5ce284 --- /dev/null +++ b/test/Mathlib/test/long_kernel_check.in @@ -0,0 +1,6 @@ +{"cmd": "import Mathlib\nset_option maxHeartbeats 0\nset_option maxRecDepth 100000"} + +{"cmd": "theorem amc12a_2003_p1 (u v : ℕ → ℕ) (h₀ : ∀ n, u n = 2 * n + 2) (h₁ : ∀ n, v n = 2 * n + 1) :\n ((∑ k in Finset.range 2003, u k) - ∑ k in Finset.range 2003, v k) = 2003 := by sorry", "env": 0} + +{"tactic": "(\nsimp only [h₀, h₁, Finset.sum_range_succ, Finset.sum_range_zero]; rfl)", "proofState": 0, "timeout": 2000} + diff --git a/test/timeout.expected.out b/test/timeout.expected.out index 64c2d6a3..f323f88e 100644 --- a/test/timeout.expected.out +++ b/test/timeout.expected.out @@ -26,7 +26,7 @@ {"proofStatus": "Completed", "proofState": 3, "goals": []} -{"message": "Operation timed out after 1ms"} +{"message": "Operation timed out"} {"message": "Unknown proof state."}