Implement soft timeout option

REPL/JSON.lean

@@ -11,7 +11,15 @@ open Lean Elab InfoTree
 
 namespace REPL
 
-structure CommandOptions where
+/-- Base structure with timeout that all command types can inherit from -/
+structure BaseOptions where
+  /--
+  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
+
+structure CommandOptions extends BaseOptions where
   allTactics : Option Bool := none
   rootGoals : Option Bool := none
   /--
@@ -38,7 +46,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 +178,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

REPL/Main.lean

@@ -362,6 +362,27 @@ 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"
+    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 =>
+      IO.cancel jobTask
+      throw e
+
 end REPL
 
 open REPL
@@ -426,14 +447,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
 

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"}
+

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}
+

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"}
+
+{"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": []}
+

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}