Add task cancellation

Author: augustepoiroux

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
 

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
 

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

@@ -26,7 +26,7 @@
 
 {"proofStatus": "Completed", "proofState": 3, "goals": []}
 
-{"message": "Operation timed out after 1ms"}
+{"message": "Operation timed out"}
 
 {"message": "Unknown proof state."}