From 147ce5ab18ac5f80d92ca40d368c7844aa6eb274 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
Date: Tue, 17 Mar 2026 12:48:53 -0400
Subject: [PATCH] chore: use IO.CancelToken in server (#12948)

This PR moves `RequestCancellationToken` from `IO.Ref` to
`IO.CancelToken`.

They consist of the same data, but the constructor of `CancelToken` is
private. Hence there is no way to take the `Ref` in a
`RequestCancellationToken` and turn it into a `CancelToken`. This in
turn means that we can't set `Core.Context.cancelTk?` to be the one in
`RequestContext` when launching `CoreM` tasks in request handlers.
---
 src/Lean/Server/RequestCancellation.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Server/RequestCancellation.lean b/src/Lean/Server/RequestCancellation.lean
index 6d500b8aa1..7d310d0cd9 100644
--- a/src/Lean/Server/RequestCancellation.lean
+++ b/src/Lean/Server/RequestCancellation.lean
@@ -14,8 +14,8 @@ public section
 namespace Lean.Server
 
 structure RequestCancellationToken where
-  cancelledByCancelRequest   : IO.Ref Bool
-  cancelledByEdit            : IO.Ref Bool
+  cancelledByCancelRequest   : IO.CancelToken
+  cancelledByEdit            : IO.CancelToken
   requestCancellationPromise : IO.Promise Unit
   editCancellationPromise    : IO.Promise Unit
 
@@ -23,18 +23,18 @@ namespace RequestCancellationToken
 
 def new : BaseIO RequestCancellationToken := do
   return {
-    cancelledByCancelRequest   := ← IO.mkRef false
-    cancelledByEdit            := ← IO.mkRef false
+    cancelledByCancelRequest   := ← IO.CancelToken.new
+    cancelledByEdit            := ← IO.CancelToken.new
     requestCancellationPromise := ← IO.Promise.new
     editCancellationPromise    := ← IO.Promise.new
   }
 
 def cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit := do
-  tk.cancelledByCancelRequest.set true
+  tk.cancelledByCancelRequest.set
   tk.requestCancellationPromise.resolve ()
 
 def cancelByEdit (tk : RequestCancellationToken) : BaseIO Unit := do
-  tk.cancelledByEdit.set true
+  tk.cancelledByEdit.set
   tk.editCancellationPromise.resolve ()
 
 def requestCancellationTask (tk : RequestCancellationToken): ServerTask Unit :=
@@ -47,10 +47,10 @@ def cancellationTasks (tk : RequestCancellationToken) : List (ServerTask Unit) :
   [tk.requestCancellationTask, tk.editCancellationTask]
 
 def wasCancelledByCancelRequest (tk : RequestCancellationToken) : BaseIO Bool :=
-  tk.cancelledByCancelRequest.get
+  tk.cancelledByCancelRequest.isSet
 
 def wasCancelledByEdit (tk : RequestCancellationToken) : BaseIO Bool :=
-  tk.cancelledByEdit.get
+  tk.cancelledByEdit.isSet
 
 def wasCancelled (tk : RequestCancellationToken) : BaseIO Bool := do
   return (← tk.wasCancelledByCancelRequest) || (← tk.wasCancelledByEdit)