From ab7aed29308351daf4b7c35216d6033aa33c0a6c Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 9 Sep 2024 14:08:37 +0200 Subject: [PATCH] feat: use incrementality for completion in tactic blocks (#5205) This PR enables the use of incrementality for completion in tactic blocks. Consider the following example: ```lean example : True := by have : True := T sleep 10000 ``` Before this PR, in order to respond to a completion request after `T`, `sleep 10000` has to complete first since the command must be fully elaborated. After this PR, the completion request is responded to immediately. --- .../Server/FileWorker/RequestHandling.lean | 38 ++++++++++--------- src/Lean/Server/Requests.lean | 29 ++++++++++---- src/Lean/Widget/UserWidget.lean | 2 +- 3 files changed, 44 insertions(+), 25 deletions(-) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 8db908b87931..ab54b0c131e3 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -28,25 +28,28 @@ open Snapshots open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString) +def findCompletionInfoTreeAtPos + (doc : EditableDocument) + (pos : String.Pos) + : Task (Option Elab.InfoTree) := + -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command, + -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent + -- snapshot that is eligible for completion should be separated by some delimiter. + findInfoTreeAtPos doc (fun s => s.data.stx.getTailPos?.any (· + ⟨1⟩ >= pos)) pos + def handleCompletion (p : CompletionParams) : RequestM (RequestTask CompletionList) := do let doc ← readDoc let text := doc.meta.text let pos := text.lspPosToUtf8Pos p.position let caps := (← read).initParams.capabilities - -- dbg_trace ">> handleCompletion invoked {pos}" - -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command, - -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent - -- command starts with a keyword that (currently?) does not participate in completion. - withWaitFindSnap doc (·.endPos + ' ' >= pos) - (notFoundX := + mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do + let some infoTree := infoTree? -- work around https://github.com/microsoft/vscode/issues/155738 - -- this is important when a snapshot cannot be found because it was aborted - pure { items := #[{label := "-"}], isIncomplete := true }) - (x := fun snap => do - if let some r ← Completion.find? p doc.meta.text pos snap.infoTree caps then - return r - return { items := #[ ], isIncomplete := true }) + | return { items := #[{label := "-"}], isIncomplete := true } + if let some r ← Completion.find? p doc.meta.text pos infoTree caps then + return r + return { items := #[ ], isIncomplete := true } /-- Handles `completionItem/resolve` requests that are sent by the client after the user selects @@ -64,9 +67,10 @@ def handleCompletionItemResolve (item : CompletionItem) let some id := data.id? | return .pure item let pos := text.lspPosToUtf8Pos data.params.position - withWaitFindSnap doc (·.endPos + ' ' >= pos) - (notFoundX := pure item) - (x := fun snap => Completion.resolveCompletionItem? text pos snap.infoTree item id) + mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do + let some infoTree := infoTree? + | return item + Completion.resolveCompletionItem? text pos infoTree item id open Elab in def handleHover (p : HoverParams) @@ -234,7 +238,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio let doc ← readDoc let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do + mapTask (findInfoTreeAtPosWithTrailingWhitespace doc hoverPos) <| Option.bindM fun infoTree => do let rs@(_ :: _) := infoTree.goalsAt? doc.meta.text hoverPos | return none let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do @@ -276,7 +280,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams) let doc ← readDoc let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do + mapTask (findInfoTreeAtPosWithTrailingWhitespace doc hoverPos) <| Option.bindM fun infoTree => do let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := infoTree.termGoalAt? hoverPos | return none let ty ← ci.runMetaM i.lctx do diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index dbd84e047e7c..9fbe1b5110c7 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -191,16 +191,17 @@ where open Language in /-- -Finds the info tree of the first snapshot task containing `pos`, asynchronously. The info tree may -be from a nested snapshot, such as a single tactic. +Finds the info tree of the first snapshot task matching `isMatchingSnapshot` and containing `pos`, +asynchronously. The info tree may be from a nested snapshot, such as a single tactic. See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done. -/ -partial def findInfoTreeAtPos (doc : EditableDocument) (pos : String.Pos) : - Task (Option Elab.InfoTree) := - -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on - -- the first character of the subsequent command if any) - findCmdParsedSnap doc (·.data.parserState.pos ≥ pos) |>.bind (sync := true) fun +partial def findInfoTreeAtPos + (doc : EditableDocument) + (isMatchingSnapshot : Lean.CommandParsedSnapshot → Bool) + (pos : String.Pos) + : Task (Option Elab.InfoTree) := + findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun | some infoTree => .pure <| some infoTree | none => cmdParsed.data.finishedSnap.task.map (sync := true) fun s => @@ -209,6 +210,20 @@ partial def findInfoTreeAtPos (doc : EditableDocument) (pos : String.Pos) : some s.cmdState.infoState.trees[0]! | none => .pure none +/-- +Finds the info tree of the first snapshot task containing `pos` (including trailing whitespace), +asynchronously. The info tree may be from a nested snapshot, such as a single tactic. + +See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done. +-/ +def findInfoTreeAtPosWithTrailingWhitespace + (doc : EditableDocument) + (pos : String.Pos) + : Task (Option Elab.InfoTree) := + -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on + -- the first character of the subsequent command if any) + findInfoTreeAtPos doc (·.data.parserState.pos ≥ pos) pos + open Elab.Command in def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do let rc ← readThe RequestContext diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index bb71e6e67e75..37cf0f25c3e7 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -400,7 +400,7 @@ open Lean Server RequestM in def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do let doc ← readDoc let filemap := doc.meta.text - mapTask (findInfoTreeAtPos doc <| filemap.lspPosToUtf8Pos pos) fun + mapTask (findInfoTreeAtPosWithTrailingWhitespace doc <| filemap.lspPosToUtf8Pos pos) fun | some infoTree@(.context (.commandCtx cc) _) => ContextInfo.runMetaM { cc with } {} do let env ← getEnv