feat: show live Lake LSP loading progress in status bar of editors instead of top of file

src/Lean/Data/Lsp/Basic.lean

@@ -369,7 +369,7 @@ abbrev ProgressToken := String -- do we need integers?
 structure ProgressParams (α : Type) where
   token : ProgressToken
   value : α
-  deriving ToJson
+  deriving ToJson, FromJson
 
 structure WorkDoneProgressReport where
   kind := "report"
@@ -407,6 +407,13 @@ structure WorkDoneProgressOptions where
   workDoneProgress := false
   deriving ToJson, FromJson
 
+/-- Params for `window/workDoneProgress/create` request.
+
+[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#window_workDoneProgress_create) -/
+structure WorkDoneProgressCreateParams where
+  token : ProgressToken
+  deriving ToJson, FromJson
+
 structure ResolveSupport where
   properties : Array String
   deriving FromJson, ToJson

src/Lean/Data/Lsp/Capabilities.lean

@@ -42,7 +42,8 @@ structure ShowDocumentClientCapabilities where
   deriving ToJson, FromJson
 
 structure WindowClientCapabilities where
-  showDocument? : Option ShowDocumentClientCapabilities := none
+  showDocument?     : Option ShowDocumentClientCapabilities := none
+  workDoneProgress? : Option Bool := none
   deriving ToJson, FromJson
 
 structure ChangeAnnotationSupport where
@@ -90,6 +91,9 @@ structure ClientCapabilities where
   lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
+def ClientCapabilities.workDoneProgress (c : ClientCapabilities) : Bool :=
+  c.window?.bind (·.workDoneProgress?) |>.getD false
+
 def ClientCapabilities.incrementalDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
   let some lean := c.lean?
     | return false

src/Lean/Server/FileWorker.lean

@@ -371,10 +371,12 @@ Callback from Lean language processor after parsing imports that requests necess
 Lake for processing imports.
 -/
 def setupImports
-    (doc         : DocumentMeta)
-    (cmdlineOpts : Options)
-    (chanOut     : Std.Channel OutputMessage)
-    (stx         : Elab.HeaderSyntax)
+    (doc                : DocumentMeta)
+    (cmdlineOpts        : Options)
+    (chanOut            : Std.Channel OutputMessage)
+    (clientCapabilities : Lsp.ClientCapabilities)
+    (createProgressToken : IO Unit)
+    (stx                : Elab.HeaderSyntax)
     : Language.ProcessingT IO (Except Language.Lean.HeaderProcessedSnapshot SetupImportsResult) := do
   let importsAlreadyLoaded ← importsLoadedRef.modifyGet ((·, true))
   if importsAlreadyLoaded then
@@ -386,22 +388,37 @@ def setupImports
     -- should not be visible to user as task is already canceled
     return .error { diagnostics := .empty, result? := none, metaSnap := default }
 
+  let useProgress := clientCapabilities.workDoneProgress
+  let progressToken := lakeProgressToken
+  if useProgress then
+    createProgressToken
+    chanOut.sync.send <| .ofMsg <| mkProgressBeginNotification progressToken "Lake"
+        (message? := some "Setting up dependencies...")
+
   let header := stx.toModuleHeader
   let fileSetupResult ← setupFile doc header fun stderrLine => do
-    let progressDiagnostic := {
-      range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
-      -- make progress visible anywhere in the file
-      fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.rawEndPos⟩
-      severity?  := DiagnosticSeverity.information
-      message    := stderrLine
-    }
-    chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic]
+    if useProgress then
+      let cleanLine := (stderrLine.trimAsciiEnd.toString.dropPrefix "✔ " |>.dropPrefix "✗ ").toString
+      chanOut.sync.send <| .ofMsg <| mkProgressReportNotification progressToken
+          (message? := some cleanLine)
+    else
+      let progressDiagnostic := {
+        range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
+        -- make progress visible anywhere in the file
+        fullRange? := some ⟨⟨0, 0⟩, doc.text.utf8PosToLspPos doc.text.source.rawEndPos⟩
+        severity?  := DiagnosticSeverity.information
+        message    := stderrLine
+      }
+      chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[progressDiagnostic]
   let isSetupError := fileSetupResult matches .importsOutOfDate
     || fileSetupResult matches .error ..
   chanOut.sync.send <| .ofMsg <|
     mkIleanHeaderSetupInfoNotification doc (collectImports stx) isSetupError
-  -- clear progress notifications in the end
-  chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[]
+  if useProgress then
+    chanOut.sync.send <| .ofMsg <| mkProgressEndNotification progressToken
+  else
+    -- clear progress notifications in the end
+    chanOut.sync.send <| .ofMsg <| mkPublishDiagnosticsNotification doc #[]
   let setup ← do
     match fileSetupResult with
     | .importsOutOfDate =>
@@ -461,7 +478,18 @@ section Initialization
           -- Emit a refresh request after a file worker restart.
           pendingRefreshInfo? := some { lastRefreshTimestamp := timestamp, successiveRefreshAttempts := 0 }
         })
-    let processor := Language.Lean.process (setupImports doc opts chanOut)
+    let createProgressToken : IO Unit :=
+      if initParams.capabilities.workDoneProgress then do
+        let requestId ← freshRequestIdRef.modifyGet fun id => (id, id + 1)
+        let responsePromise ← IO.Promise.new
+        pendingServerRequestsRef.modify (·.insert requestId responsePromise)
+        chanOut.sync.send <| .ofMsg <|
+          mkWorkDoneProgressCreateRequest requestId lakeProgressToken
+        let _ ← IO.wait responsePromise.result!
+      else
+        pure ()
+    let processor := Language.Lean.process
+        (setupImports doc opts chanOut initParams.capabilities createProgressToken)
     let processor ← Language.mkIncrementalProcessor processor
     let initSnap ← processor doc.mkInputContext
     let _ ← ServerTask.IO.asTask do

src/Lean/Server/Utils.lean

@@ -163,6 +163,32 @@ def mkFileProgressAtPosNotification (m : DocumentMeta) (pos : String.Pos.Raw)
 def mkFileProgressDoneNotification (m : DocumentMeta) : JsonRpc.Notification Lsp.LeanFileProgressParams :=
   mkFileProgressNotification m #[]
 
+/-- Constructs a `$/progress` notification with `WorkDoneProgressBegin`. -/
+def mkProgressBeginNotification (token : Lsp.ProgressToken) (title : String)
+    (message? : Option String := none) :
+    JsonRpc.Notification (Lsp.ProgressParams Lsp.WorkDoneProgressBegin) :=
+  { method := "$/progress", param := { token, value := { title, message? } } }
+
+/-- Constructs a `$/progress` notification with `WorkDoneProgressReport`. -/
+def mkProgressReportNotification (token : Lsp.ProgressToken)
+    (message? : Option String := none) :
+    JsonRpc.Notification (Lsp.ProgressParams Lsp.WorkDoneProgressReport) :=
+  { method := "$/progress", param := { token, value := { message? } } }
+
+/-- Constructs a `$/progress` notification with `WorkDoneProgressEnd`. -/
+def mkProgressEndNotification (token : Lsp.ProgressToken)
+    (message? : Option String := none) :
+    JsonRpc.Notification (Lsp.ProgressParams Lsp.WorkDoneProgressEnd) :=
+  { method := "$/progress", param := { token, value := { message? } } }
+
+/-- Shared progress token for Lake dependency setup. -/
+def lakeProgressToken : Lsp.ProgressToken := "lean4/lakeSetup"
+
+/-- Constructs a `window/workDoneProgress/create` request. -/
+def mkWorkDoneProgressCreateRequest (id : JsonRpc.RequestID) (token : Lsp.ProgressToken) :
+    JsonRpc.Request Lsp.WorkDoneProgressCreateParams :=
+  ⟨id, "window/workDoneProgress/create", { token }⟩
+
 -- TODO: should return a request ID (or task?) when we add response handling
 def mkApplyWorkspaceEditRequest (params : ApplyWorkspaceEditParams) :
     JsonRpc.Request ApplyWorkspaceEditParams :=

src/Lean/Server/Watchdog.lean

@@ -831,6 +831,8 @@ section ServerM
         | .notification "$/lean/importClosure" =>
           if let .ok params := parseNotificationParams? LeanImportClosureParams msg then
             handleImportClosure fw params
+        | .notification "$/progress" =>
+          writeSerializedMessage msg
         | _ =>
           writeSerializedMessage msg
 

tests/lean/run/lspProgressNotification.lean

@@ -0,0 +1,134 @@
+import Lean.Data.Lsp.Basic
+import Lean.Data.Lsp.Capabilities
+import Lean.Server.Utils
+
+/-!
+# LSP `$/progress` notification helpers
+
+Validates JSON serialization of `WorkDoneProgressBegin`, `WorkDoneProgressReport`,
+`WorkDoneProgressEnd`, `WorkDoneProgressCreateParams`, and capability parsing.
+-/
+
+open Lean Lsp Server
+
+/-! ## WorkDoneProgressBegin serializes `kind` as `"begin"` -/
+
+/--
+info: {"title": "Lake",
+ "message": "Setting up...",
+ "kind": "begin",
+ "cancellable": false}
+-/
+#guard_msgs in
+  #eval do
+    let begin_ : WorkDoneProgressBegin := { title := "Lake", message? := some "Setting up..." }
+    IO.println (toString (toJson begin_))
+
+/-! ## WorkDoneProgressReport serializes `kind` as `"report"` -/
+
+/--
+info: {"message": "Building Mathlib.Algebra", "kind": "report", "cancellable": false}
+-/
+#guard_msgs in
+  #eval do
+    let report : WorkDoneProgressReport := { message? := some "Building Mathlib.Algebra" }
+    IO.println (toString (toJson report))
+
+/-! ## WorkDoneProgressEnd serializes `kind` as `"end"` -/
+
+/--
+info: {"kind": "end"}
+-/
+#guard_msgs in
+  #eval do
+    let end_ : WorkDoneProgressEnd := {}
+    IO.println (toString (toJson end_))
+
+/-! ## WorkDoneProgressCreateParams round-trips through JSON -/
+
+/--
+info: {"token": "myToken"}
+-/
+#guard_msgs in
+  #eval do
+    let params : WorkDoneProgressCreateParams := { token := "myToken" }
+    IO.println (toString (toJson params))
+
+/-! ## ProgressParams wraps value with token -/
+
+/--
+info: {"value": {"title": "Lake", "kind": "begin", "cancellable": false},
+ "token": "lake"}
+-/
+#guard_msgs in
+  #eval do
+    let notif := mkProgressBeginNotification "lake" "Lake"
+    IO.println (toString (toJson notif.param))
+
+/-! ## ClientCapabilities.workDoneProgress accessor -/
+
+/--
+info: true
+-/
+#guard_msgs in
+  #eval do
+    let caps : ClientCapabilities := {
+      window? := some { workDoneProgress? := some true }
+    }
+    IO.println (toString caps.workDoneProgress)
+
+/--
+info: false
+-/
+#guard_msgs in
+  #eval do
+    let caps : ClientCapabilities := {}
+    IO.println (toString caps.workDoneProgress)
+
+/--
+info: false
+-/
+#guard_msgs in
+  #eval do
+    let caps : ClientCapabilities := {
+      window? := some {}
+    }
+    IO.println (toString caps.workDoneProgress)
+
+/-! ## ClientCapabilities with workDoneProgress round-trips through JSON -/
+
+/--
+info: true
+-/
+#guard_msgs in
+  #eval do
+    let j := toJson ({ window? := some { workDoneProgress? := some true } } : ClientCapabilities)
+    match fromJson? j with
+    | .ok (caps : ClientCapabilities) => IO.println (toString caps.workDoneProgress)
+    | .error e => IO.println s!"parse error: {e}"
+
+/-! ## lakeProgressToken is the expected string -/
+
+/--
+info: "lean4/lakeSetup"
+-/
+#guard_msgs in
+  #eval IO.println (toString (toJson lakeProgressToken))
+
+/-! ## mkWorkDoneProgressCreateRequest produces correct request -/
+
+/--
+info: window/workDoneProgress/create
+-/
+#guard_msgs in
+  #eval do
+    let req := mkWorkDoneProgressCreateRequest 42 lakeProgressToken
+    IO.println req.method
+
+/--
+info: {"token": "lean4/lakeSetup"}
+-/
+#guard_msgs in
+  #eval do
+    let req := mkWorkDoneProgressCreateRequest 42 lakeProgressToken
+    IO.println (toString (toJson req.param))