Skip to content

Commit

Permalink
fix: inlay hint assertion violation (leanprover#7164)
Browse files Browse the repository at this point in the history
This PR fixes an assertion violation introduced in leanprover#7149 where the
monotonic progress assumption was violated by request cancellation.
  • Loading branch information
mhuisi authored Feb 20, 2025
1 parent 2eb4787 commit 970732e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/Lean/Server/FileWorker/InlayHints.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 970732e

Please sign in to comment.