From 0d1907c1df2093f2ef1da2b470693c8b0860f0b4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 7 Feb 2025 17:50:31 +0100 Subject: [PATCH] feat: parallel progress notifications (#6329) This PR enables the language server to present multiple disjoint line ranges as being worked on. Even before parallelism lands, we make use of this feature to show post-elaboration tasks such as kernel checking on the first line of a declaration to distinguish them from the final tactic step. ![image](https://github.com/user-attachments/assets/f6170689-6835-40c0-baba-df067a60b605) --- .github/workflows/ci.yml | 4 +- src/Lean/Data/Lsp/Basic.lean | 4 +- src/Lean/Elab/MutualDef.lean | 16 ++-- src/Lean/Language/Lean.lean | 38 +++++---- src/Lean/Server/FileWorker.lean | 133 ++++++++++++++++++++------------ 5 files changed, 121 insertions(+), 74 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56f5dfbd82..7129b9c895 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -175,8 +175,8 @@ jobs: "os": "ubuntu-latest", "check-level": 2, "CMAKE_PRESET": "debug", - // exclude seriously slow tests - "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress'" + // exclude seriously slow/stackoverflowing tests + "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress|3807'" }, // TODO: suddenly started failing in CI /*{ diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 98e80e35e3..cf38373638 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -27,7 +27,7 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally. structure Position where line : Nat character : Nat - deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson + deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson, Repr instance : ToString Position := ⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ @@ -38,7 +38,7 @@ instance : LE Position := leOfOrd structure Range where start : Position «end» : Position - deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord + deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord, Repr instance : LT Range := ltOfOrd instance : LE Range := leOfOrd diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 8ba59ff7b3..a31fdcffa0 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -215,6 +215,14 @@ private def elabHeaders (views : Array DefView) return newHeader if let some snap := view.headerSnap? then let (tacStx?, newTacTask?) ← mkTacTask view.value tacPromise + let bodySnap := + -- Only use first line of body as range when we have incremental tactics as otherwise we + -- would cover their progress + { range? := if newTacTask?.isSome then + view.ref.getPos?.map fun pos => ⟨pos, pos⟩ + else + getBodyTerm? view.value |>.getD view.value |>.getRange? + task := bodyPromise.resultD default } snap.new.resolve <| some { diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog)) @@ -223,7 +231,7 @@ private def elabHeaders (views : Array DefView) tacStx? tacSnap? := newTacTask? bodyStx := view.value - bodySnap := mkBodyTask view.value bodyPromise + bodySnap } newHeader := { newHeader with -- We should only forward the promise if we are actually waiting on the @@ -245,12 +253,6 @@ where guard whereDeclsOpt.isNone return body - /-- Creates snapshot task with appropriate range from body syntax and promise. -/ - mkBodyTask (body : Syntax) (new : IO.Promise (Option BodyProcessedSnapshot)) : - Language.SnapshotTask (Option BodyProcessedSnapshot) := - let rangeStx := getBodyTerm? body |>.getD body - { range? := rangeStx.getRange?, task := new.resultD default } - /-- If `body` allows for incremental tactic reporting and reuse, creates a snapshot task out of the passed promise with appropriate range, otherwise immediately resolves the promise to a dummy diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index 4b36d9a5cd..94807f0c2b 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -294,6 +294,13 @@ If the option is defined in this library, use '-D{`weak ++ name}' to set it cond return opts +private def getNiceCommandStartPos? (stx : Syntax) : Option String.Pos := do + let mut stx := stx + if stx[0].isOfKind ``Command.declModifiers then + -- modifiers are morally before the actual declaration + stx := stx[1] + stx.getPos? + /-- Entry point of the Lean language processor. @@ -331,6 +338,8 @@ where -- parser state may still have changed because of trailing whitespace and comments etc., so -- they are passed separately from `old` if let some oldSuccess := old.result? then + -- make sure to update ranges of all reused tasks + let progressRange? := some ⟨newParserState.pos, ctx.input.endPos⟩ return { ictx stx := newStx @@ -338,11 +347,12 @@ where cancelTk? := ctx.newCancelTk result? := some { parserState := newParserState - processedSnap := (← oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do + processedSnap := (← oldSuccess.processedSnap.bindIO (range? := progressRange?) + (sync := true) fun oldProcessed => do if let some oldProcSuccess := oldProcessed.result? then -- also wait on old command parse snapshot as parsing is cheap and may allow for -- elaboration reuse - oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do + oldProcSuccess.firstCmdSnap.bindIO (sync := true) (range? := progressRange?) fun oldCmd => do let prom ← IO.Promise.new parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx return .pure { @@ -477,11 +487,14 @@ where -- have changed because of trailing whitespace and comments etc., so it is passed separately -- from `old` if let some oldNext := old.nextCmdSnap? then do + -- make sure to update ranges of all reused tasks + let progressRange? := some ⟨newParserState.pos, ctx.input.endPos⟩ let newProm ← IO.Promise.new - let _ ← old.finishedSnap.bindIO (sync := true) fun oldFinished => + -- can reuse range, syntax unchanged + let _ ← old.finishedSnap.bindIO (sync := true) (range? := progressRange?) fun oldFinished => -- also wait on old command parse snapshot as parsing is cheap and may allow for -- elaboration reuse - oldNext.bindIO (sync := true) fun oldNext => do + oldNext.bindIO (sync := true) (range? := progressRange?) fun oldNext => do parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx return .pure () prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result! } } @@ -540,15 +553,10 @@ where let elabPromise ← IO.Promise.new let finishedPromise ← IO.Promise.new let reportPromise ← IO.Promise.new - -- (Try to) use last line of command as range for final snapshot task. This ensures we do not - -- retract the progress bar to a previous position in case the command support incremental - -- reporting but has significant work after resolving its last incremental promise, such as - -- final type checking; if it does not support incrementality, `elabSnap` constructed in - -- `parseCmd` and containing the entire range of the command will determine the reported - -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is - -- irrelevant in this case. - let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩ - let finishedSnap := { range? := endRange?, task := finishedPromise.result! } + -- report terminal tasks on first line of decl such as not to hide incremental tactics' + -- progress + let initRange? := getNiceCommandStartPos? stx |>.map fun pos => ⟨pos, pos⟩ + let finishedSnap := { range? := initRange?, task := finishedPromise.result! } let tacticCache ← old?.map (·.tacticCache) |>.getDM (IO.mkRef {}) let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts @@ -566,7 +574,7 @@ where diagnostics, finishedSnap, tacticCache, nextCmdSnap? stx := stx', parserState := parserState' elabSnap := { range? := stx.getRange?, task := elabPromise.result! } - reportSnap := { range? := endRange?, task := reportPromise.result! } + reportSnap := { range? := initRange?, task := reportPromise.result! } } let cmdState ← doElab stx cmdState beginPos { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise } @@ -597,7 +605,7 @@ where pure <| .pure <| .mk { diagnostics := .empty } #[] reportPromise.resolve <| .mk { diagnostics := .empty } <| - cmdState.snapshotTasks.push { range? := endRange?, task := traceTask } + cmdState.snapshotTasks.push { range? := initRange?, task := traceTask } if let some next := next? then -- We're definitely off the fast-forwarding path now parseCmd none parserState cmdState next (sync := false) ctx diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 659dede5ba..bdc625661b 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -148,11 +148,6 @@ section Elab newInfoTrees : Array Elab.InfoTree := #[] /-- Whether we encountered any snapshot with `Snapshot.isFatal`. -/ hasFatal := false - /-- - Last `Snapshot.range?` encountered that was not `none`, if any. We use this as a fallback when - reporting progress as we should always report *some* range when waiting on a task. - -/ - lastRange? : Option String.Range := none deriving Inhabited register_builtin_option server.reportDelayMs : Nat := { @@ -195,34 +190,78 @@ This option can only be set on the command line, not in the lakefile or via `set See also section "Communication" in Lean/Server/README.md. Debouncing: we only report information - * after first waiting for `reportDelayMs`, to give trivial tasks a chance to finish - * when first blocking, i.e. not before skipping over any unchanged snapshots and such trivial - tasks - * afterwards, each time new information is found in a snapshot - * at the very end, if we never blocked (e.g. emptying a file should make - sure to empty diagnostics as well eventually) -/ + 1. after first waiting for `reportDelayMs`, to give trivial tasks a chance to finish + 2. when first blocking, i.e. not before skipping over any unchanged snapshots and such trivial + tasks + 3. afterwards, each time new information is found in a snapshot + 4. at the very end, if we never blocked (e.g. emptying a file should make + sure to empty diagnostics as well eventually) -/ private partial def reportSnapshots (ctx : WorkerContext) (doc : EditableDocumentCore) (cancelTk : CancelToken) : BaseIO (Task Unit) := do let t ← BaseIO.asTask do - IO.sleep (server.reportDelayMs.get ctx.cmdlineOpts).toUInt32 + IO.sleep (server.reportDelayMs.get ctx.cmdlineOpts).toUInt32 -- "Debouncing 1." BaseIO.bindTask t fun _ => do - BaseIO.bindTask (← go (toSnapshotTree doc.initSnap) {}) fun st => do - if (← cancelTk.isSet) then - return .pure () - - -- callback at the end of reporting - if st.hasFatal then - ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta 0 .fatalError - else - ctx.chanOut.send <| mkFileProgressDoneNotification doc.meta - unless st.hasBlocked do - publishDiagnostics ctx doc - -- This will overwrite existing ilean info for the file, in case something - -- went wrong during the incremental updates. - ctx.chanOut.send (← mkIleanInfoFinalNotification doc.meta st.allInfoTrees) + let (_, st) ← handleTasks #[.pure <| toSnapshotTree doc.initSnap] |>.run {} + if (← cancelTk.isSet) then return .pure () + + -- callback at the end of reporting + if st.hasFatal then + ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta 0 .fatalError + else + ctx.chanOut.send <| mkFileProgressDoneNotification doc.meta + unless st.hasBlocked do -- "Debouncing 4." + publishDiagnostics ctx doc + -- This will overwrite existing ilean info for the file, in case something + -- went wrong during the incremental updates. + ctx.chanOut.send (← mkIleanInfoFinalNotification doc.meta st.allInfoTrees) + return .pure () where - go (node : SnapshotTree) (st : ReportSnapshotsState) : BaseIO (Task ReportSnapshotsState) := do + /-- + Given an array of possibly-unfinished tasks, handles them, possibly after waiting for one of + them to finish. + -/ + handleTasks (ts : Array (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do + let ts ← ts.flatMapM handleFinished + -- all `ts` are now (likely) in-progress, report them + sendFileProgress ts + -- check again whether this has changed before commiting to waiting + if (← ts.anyM (IO.hasFinished ·.task)) then + handleTasks ts + else if h : ts.size > 0 then + if !(← get).hasBlocked then -- "Debouncing 2." + publishDiagnostics ctx doc + modify fun st => { st with hasBlocked := true } + -- wait for at least one task to finish; there is a race condition here where a task may + -- have finished between the previous check and this line but we accept the progress + -- notifications being temporarily out of date in this case + let _ ← IO.waitAny (ts.map (·.task) |>.toList) + (by simp only [Array.toList_map, List.length_map, Array.length_toList, gt_iff_lt, h]) + handleTasks ts + + /-- Recursively handles finished tasks and replaces them with their unfinished children. -/ + handleFinished (t : SnapshotTask SnapshotTree) : + StateT ReportSnapshotsState BaseIO (Array (SnapshotTask SnapshotTree)) := do + if (← IO.hasFinished t.task) then + handleNode t.task.get + -- limit children's reported range to that of the parent, if any, to avoid strange + -- non-monotonic progress updates; replace missing children's ranges with parent's + let ts := t.task.get.children.map (fun t' => { t' with range? := + match t.range?, t'.range? with + | some r, some r' => + let start := max r.start r'.start + let stop := min r.stop r'.stop + -- ensure `stop ≥ start`, lest we end up with negative ranges if `r` and `r'` are + -- disjoint + let stop := max start stop + some { start, stop } + | r?, r?' => r?' <|> r? }) + ts.flatMapM handleFinished + else + return #[t] + + /-- Handles information of a single now-finished snapshot. -/ + handleNode (node : SnapshotTree) : StateT ReportSnapshotsState BaseIO Unit := do if node.element.diagnostics.msgLog.hasUnreported then let diags ← if let some memorized ← node.element.diagnostics.interactiveDiagsRef?.bindM fun ref => do @@ -235,35 +274,33 @@ This option can only be set on the command line, not in the lakefile or via `set cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics } pure diags doc.diagnosticsRef.modify (· ++ diags) - if st.hasBlocked then + if (← get).hasBlocked then publishDiagnostics ctx doc - let mut st := { st with hasFatal := st.hasFatal || node.element.isFatal } + modify fun st => { st with hasFatal := st.hasFatal || node.element.isFatal } if let some itree := node.element.infoTree? then - let mut newInfoTrees := st.newInfoTrees.push itree - if st.hasBlocked then + let mut newInfoTrees := (← get).newInfoTrees.push itree + if (← get).hasBlocked then ctx.chanOut.send (← mkIleanInfoUpdateNotification doc.meta newInfoTrees) newInfoTrees := #[] - st := { st with newInfoTrees, allInfoTrees := st.allInfoTrees.push itree } + modify fun st => { st with newInfoTrees, allInfoTrees := st.allInfoTrees.push itree } - goSeq st node.children.toList + /-- Reports given tasks' ranges, merging overlapping ones. -/ + sendFileProgress (tasks : Array (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do + let ranges := tasks.filterMap (·.range?) + let ranges := ranges.qsort (·.start < ·.start) + let ranges := ranges.foldl (init := #[]) fun rs r => match rs[rs.size - 1]? with + | some last => + if last.stop < r.start then + rs.push r + else + rs.pop.push { last with stop := max last.stop r.stop } + | none => rs.push r + let ranges := ranges.map (·.toLspRange doc.meta.text) + let notifs := ranges.map ({ range := ·, kind := .processing }) + ctx.chanOut.send <| mkFileProgressNotification doc.meta notifs - goSeq (st : ReportSnapshotsState) : - List (SnapshotTask SnapshotTree) → BaseIO (Task ReportSnapshotsState) - | [] => return .pure st - | t::ts => do - let mut st := st - st := { st with lastRange? := t.range? <|> st.lastRange? } - unless (← IO.hasFinished t.task) do - -- report *some* recent range even if `t.range?` is `none`; see also `State.lastRange?` - if let some range := st.lastRange? then - ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta range.start - if !st.hasBlocked then - publishDiagnostics ctx doc - st := { st with hasBlocked := true } - BaseIO.bindTask t.task fun t => do - BaseIO.bindTask (← go t st) (goSeq · ts) end Elab structure PendingRequest where