From 970732ea11515cb6aa96beb3cb3578f6fc8e2cde Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 20 Feb 2025 14:03:44 +0100 Subject: [PATCH] fix: inlay hint assertion violation (#7164) This PR fixes an assertion violation introduced in #7149 where the monotonic progress assumption was violated by request cancellation. --- src/Lean/Server/FileWorker/InlayHints.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker/InlayHints.lean b/src/Lean/Server/FileWorker/InlayHints.lean index ca8103dd2a10..5d32135439d7 100644 --- a/src/Lean/Server/FileWorker/InlayHints.lean +++ b/src/Lean/Server/FileWorker/InlayHints.lean @@ -126,10 +126,12 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) : let timeSinceLastEditMs := timestamp - lastEditTimestamp inlayHintEditDelayMs - timeSinceLastEditMs let (snaps, _, isComplete) ← ctx.doc.cmdSnaps.getFinishedPrefixWithConsistentLatency editDelayMs.toUInt32 (cancelTk? := ctx.cancelTk.cancellationTask) + -- This cancellation check is crucial for the invariant `finishedSnaps >= oldFinishedSnaps` below. + RequestM.checkCancelled let snaps := snaps.toArray let finishedSnaps := snaps.size let oldFinishedSnaps := s.oldFinishedSnaps - -- File processing is monotonic modulo `didChange` notifications. + -- File processing is monotonic modulo `didChange` notifications and cancellation. assert! finishedSnaps >= oldFinishedSnaps -- VS Code emits inlay hint requests *every time the user scrolls*. This is reasonably expensive, -- so in addition to re-using old inlay hints from parts of the file that haven't been processed