fix: tolerate Lean document identifier field rename

Beam/Broker/Pending.lean

@@ -171,7 +171,8 @@ private def matchesSyncFileProgress
     (version : Nat)
     (params : LeanFileProgressParams) : Bool :=
   let matchesUri := params.textDocument.uri == uri
-  let matchesVersion := params.textDocument.version?.map (fun progressVersion =>
+  let ⟨_, progressVersion?⟩ := params.textDocument
+  let matchesVersion := progressVersion?.map (fun progressVersion =>
     decide (version <= progressVersion)) |>.getD true
   matchesUri && matchesVersion
 

Beam/Broker/Server.lean

@@ -935,7 +935,7 @@ private def syncFileSnapshotDetailed
       if changedSource then sendTextDocumentDidSave session snapshot.uri else pure session
     | .change =>
         let param := toJson ({
-          textDocument := { uri := snapshot.uri, version? := some decision.version }
+          textDocument := ⟨snapshot.uri, some decision.version⟩
           contentChanges := #[TextDocumentContentChangeEvent.fullChange snapshot.text]
           : DidChangeTextDocumentParams
         })
@@ -2313,7 +2313,7 @@ private def requireCurrentImportBasis
     let publishedModules := current.publishedModules.toArray.map fun (module, eventSeq) =>
       { module, eventSeq : Beam.LSP.ImportBasis.PublishedModule }
     let param := toJson ({
-      textDocument := { uri := started.document.uri, version? := some started.document.version }
+      textDocument := ⟨started.document.uri, some started.document.version⟩
       publishedModules
       : Beam.LSP.ImportBasis.CheckParams
     })
@@ -2642,7 +2642,7 @@ private def handleRunAtOp
   let started ← liftFailureIO <| server.withRequestSessionState req do
     startSyncedWorkspaceRequest server req snapshot method
       (fun uri => Json.mkObj <|
-        [ ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier }))
+        [ ("textDocument", toJson (VersionedTextDocumentIdentifier.mk uri (some request.version)))
         , ("position", toJson ({ line := request.line, character := request.character : Lsp.Position }))
         , ("text", toJson request.text)
         ] ++ (match request.storeHandle? with
@@ -2666,7 +2666,7 @@ private def positionLspParams
     (extraFields : List (String × Json) := []) : Json :=
   Json.mkObj <|
     [
-      ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier })),
+      ("textDocument", toJson (VersionedTextDocumentIdentifier.mk uri (some request.version))),
       ("position", toJson ({ line := request.line, character := request.character : Lsp.Position }))
     ] ++ extraFields
 
@@ -2836,7 +2836,7 @@ private def handleGoalsOp
   let position : Lsp.Position := { line := request.line, character := request.character }
   let pending ← runSyncedDocumentRequest server req method
     (fun uri => Json.mkObj [
-      ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier })),
+      ("textDocument", toJson (VersionedTextDocumentIdentifier.mk uri (some request.version))),
       ("position", toJson position)
     ])
     request.version
@@ -2852,7 +2852,7 @@ private def handleTodoOp
   let method := todoMethod
   let pending ← runSyncedDocumentRequest server req method
     (fun uri => Json.mkObj <|
-      [ ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier }))
+      [ ("textDocument", toJson (VersionedTextDocumentIdentifier.mk uri (some request.version)))
       ] ++
       (match request.range? with
       | some range => [("range", toJson range)]

Beam/LSP/Lib/Request.lean

@@ -30,11 +30,12 @@ def checkRequestCancelled : RequestM Unit := do
 def requireDocumentVersion (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier) :
     RequestM Unit := do
   let doc ← RequestM.readDoc
-  match textDocument.version? with
-  | none =>
+  -- Constructor matching also accepts Lean 4.37's rename of the optional version field.
+  match textDocument with
+  | ⟨_, none⟩ =>
       throw <| RequestError.invalidParams
         "textDocument.version is required for snapshot-bound Beam LSP requests"
-  | some expectedVersion =>
+  | ⟨_, some expectedVersion⟩ =>
       unless doc.meta.version == expectedVersion do
         throw {
           code := Lean.JsonRpc.ErrorCode.contentModified

CHANGELOG.md

@@ -23,6 +23,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Fixed
 
+- Keep snapshot-bound requests and progress notifications compatible with the
+  `VersionedTextDocumentIdentifier` field rename proposed in
+  [Lean #16237](https://github.com/leanprover/lean4/pull/16237), without changing the supported release window.
 - `save` refusals that suggest `lake build` (`saveUnsupportedSetup`, `saveTraceStale`) and the
   deferred-compilation readiness message in `sync` now say to stop the CLI owner or drop the MCP
   workspace and confirm cleanup before building, then start a fresh session. Building while the session was live left dependencies marked as needing a save,

docs/COMPATIBILITY.md

@@ -54,6 +54,12 @@ A Lean release line is the canonical `major.minor` family recorded in
   use Lake's full `ModulePreSetup.trace` directly. Lake 4.34–4.35 require the C output descriptor;
   4.36 and current nightly SDKs use optional `ModuleOutputDescrs.c?`. Beam supplies the generated C
   descriptor on both shapes.
+- `Lean.Lsp.VersionedTextDocumentIdentifier` uses positional construction and matching across
+  the `version?` → `version` field rename in
+  [Lean #16237](https://github.com/leanprover/lean4/pull/16237), reverted by
+  [Lean #16356](https://github.com/leanprover/lean4/pull/16356). Both forms carry a `DocumentUri`
+  and an `Option Nat`. Progress accepts an unknown version; snapshot-bound requests require one.
+  Named version fields can be used again when every supported SDK includes the rename.
 - Standalone installation manifest schema 4 and native installation manifest schema 3.
   Earlier installation records do not establish a complete component
   set and must be reinstalled; they are not accepted as current installation inventories.

tests/lean/BeamTest/Broker/PendingTest.lean

@@ -399,8 +399,9 @@ private def mkRange (startLine startCharacter endLine endCharacter : Nat) : Rang
   «end» := { line := endLine, character := endCharacter }
 }
 
-private def mkFileProgress (ranges : Array Range) : LeanFileProgressParams := {
-  textDocument := { uri := "file:///workspace/Foo.lean", version? := some 1 }
+private def mkFileProgress (ranges : Array Range)
+    (version? : Option Nat := some 1) : LeanFileProgressParams := {
+  textDocument := ⟨"file:///workspace/Foo.lean", version?⟩
   processing := ranges.map fun range => { range }
 }
 
@@ -487,6 +488,26 @@ private def checkSyncFileProgressLines : IO Unit := do
   requireFieldAbsent "finished progress" "totalLines" renderedProgress
   requireJsonInt "finished progress" "rangeEndLine" 13 renderedProgress
 
+/-- Both wire encodings of an unknown version must preserve progress selection. -/
+private def checkSyncFileProgressVersionSelection : IO Unit := do
+  let uri := "file:///workspace/Foo.lean"
+  for (versionFields, expectedUpdates) in [
+      ([], 1), ([("version", Json.null)], 1),
+      ([("version", toJson (0 : Nat))], 0),
+      ([("version", toJson (1 : Nat))], 1),
+      ([("version", toJson (2 : Nat))], 1)] do
+    let param := Json.mkObj [
+      ("textDocument", Json.mkObj (("uri", toJson uri) :: versionFields)),
+      ("processing", toJson (mkFileProgress #[mkRange 0 0 1 0]).processing)]
+    let pending ← mkPending
+      (progress? := some {})
+      (tracked? := some (uri, 1))
+    PendingRequest.observeProgress pending param
+    let some progress ← pending.progressRef.get
+      | throw <| IO.userError "versioned fileProgress cleared progress"
+    require s!"fileProgress version filtering: {param.compress}"
+      (progress.updates == expectedUpdates)
+
 private def checkDiagnosticLineCanExceedProgressRange : IO Unit := do
   let active ← observeFileProgress {} #[mkRange 0 0 1 0]
   let finished ← observeFileProgress active #[]
@@ -601,6 +622,7 @@ def main : IO Unit := do
   checkPendingResolveError
   checkSyncFileProgressDisplay
   checkSyncFileProgressLines
+  checkSyncFileProgressVersionSelection
   checkDiagnosticLineCanExceedProgressRange
   checkDiagnosticEmitterFailureIsolation
   checkProgressEmitterFailureIsolation

tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean

@@ -343,6 +343,25 @@ def checkRunAtStaleEdit : ScenarioM Unit := do
 
   closeDoc doc
 
+def checkRunAtMissingVersion : ScenarioM Unit := do
+  let path := "tests/scenario/docs/SimpleProof.lean"
+  let doc ← openDoc path
+  syncDoc doc
+  let uri := System.Uri.pathToUri (← IO.FS.realPath path)
+  for versionFields in [[], [("version", Json.null)]] do
+    let params := Json.mkObj [
+      ("textDocument", Json.mkObj (("uri", toJson uri) :: versionFields)),
+      ("position", toJson ({ line := 1, character := 2 } : Lean.Lsp.Position)),
+      ("text", toJson "exact trivial")]
+    let req ← sendRawRequest Beam.LSP.RunAt.method params
+    expectErrorContains req invalidParamsJson
+    let outcome ← awaitReq req
+    unless outcome.errorMessage.contains "textDocument.version is required" do
+      throw <| IO.userError s!"unversioned runAt: unexpected error {outcome.errorMessage}"
+  -- Rejected requests must leave the document usable.
+  requireRunAtSolvesProof "runAt after unversioned requests" doc ⟨1, 2⟩ "exact trivial"
+  closeDoc doc
+
 def checkRunAtStaleVersion : ScenarioM Unit := do
   let doc ← openDoc "tests/scenario/docs/SimpleProof.lean"
   syncDoc doc
@@ -565,6 +584,7 @@ def run : ScenarioM Unit := do
   checkRunAtInvalidPositionLine
   checkRunAtInvalidPositionCharacter
   checkRunAtStaleEdit
+  checkRunAtMissingVersion
   checkRunAtStaleVersion
   checkRunAtStaleEditConcurrentRequest
   checkRunAtCancellation

tests/lean/BeamTest/LSP/Scenario.lean

@@ -222,6 +222,11 @@ private def registerRequest (requestID : RequestID) (params : Json) : ScenarioM
   }
   pure req
 
+/-- Send JSON unchanged so request tests can exercise malformed or omitted fields. -/
+def sendRawRequest (method : String) (params : Json) : ScenarioM ReqHandle := do
+  let requestID ← sendRequest method params
+  registerRequest requestID params
+
 private partial def waitForRequestOutcome (expectedID : RequestID) : ScenarioM RequestOutcome := do
   if let some outcome ← takeQueuedResponse? expectedID then
     return outcome
@@ -368,7 +373,7 @@ def changeDocBatch (doc : DocHandle) (specs : Array ChangeSpec) : ScenarioM Unit
   let docState ← getDocState doc
   let contentChanges := specs.map mkRangeChange
   let params : DidChangeTextDocumentParams := {
-    textDocument := { uri := docState.uri, version? := docState.versionNo }
+    textDocument := ⟨docState.uri, docState.versionNo⟩
     contentChanges
   }
   Ipc.writeNotification ⟨"textDocument/didChange", params⟩
@@ -429,10 +434,7 @@ def notifyWatchedFileChanged (path : System.FilePath)
 def sendRunAt (doc : DocHandle) (spec : SendRunAtSpec) : ScenarioM ReqHandle := do
   let docState ← getDocState doc
   let params : Beam.LSP.RunAt.Params := {
-    textDocument := {
-      uri := docState.uri
-      version? := some (spec.version?.getD (docState.versionNo - 1))
-    }
+    textDocument := ⟨docState.uri, some (spec.version?.getD (docState.versionNo - 1))⟩
     position := { line := spec.line, character := spec.character }
     text := spec.text
     storeHandle? := if spec.storeHandle then some true else none
@@ -457,10 +459,7 @@ def runWithHandle (doc : DocHandle) (handle : Beam.LSP.RunAt.Handle) (spec : Run
 def sendGoals (doc : DocHandle) (spec : GoalsSpec) : ScenarioM ReqHandle := do
   let docState ← getDocState doc
   let params : Beam.LSP.Goals.Params := {
-    textDocument := {
-      uri := docState.uri
-      version? := some (spec.version?.getD (docState.versionNo - 1))
-    }
+    textDocument := ⟨docState.uri, some (spec.version?.getD (docState.versionNo - 1))⟩
     position := { line := spec.line, character := spec.character }
   }
   let method := if spec.useAfter then Beam.LSP.Goals.afterMethod else Beam.LSP.Goals.prevMethod
@@ -470,10 +469,7 @@ def sendGoals (doc : DocHandle) (spec : GoalsSpec) : ScenarioM ReqHandle := do
 def sendTodo (doc : DocHandle) (spec : TodoSpec) : ScenarioM ReqHandle := do
   let docState ← getDocState doc
   let params : Beam.LSP.Todo.TodoParams := {
-    textDocument := {
-      uri := docState.uri
-      version? := some (spec.version?.getD (docState.versionNo - 1))
-    }
+    textDocument := ⟨docState.uri, some (spec.version?.getD (docState.versionNo - 1))⟩
     range? := some {
       start := { line := spec.startLine, character := spec.startCharacter }
       «end» := { line := spec.endLine, character := spec.endCharacter }
@@ -489,7 +485,7 @@ def sendTodoWholeDocument
     (kinds? : Option (Array Beam.LSP.Todo.TodoKind) := none) : ScenarioM ReqHandle := do
   let docState ← getDocState doc
   let params : Beam.LSP.Todo.TodoParams := {
-    textDocument := { uri := docState.uri, version? := some (docState.versionNo - 1) }
+    textDocument := ⟨docState.uri, some (docState.versionNo - 1)⟩
     kinds?
   }
   let requestID ← sendRequest Beam.LSP.Todo.method (toJson params)
@@ -537,7 +533,7 @@ def sendImportBasisCheck (doc : DocHandle) (version? : Option Nat := none)
     ScenarioM ReqHandle := do
   let docState ← getDocState doc
   let params : Beam.LSP.ImportBasis.CheckParams := {
-    textDocument := { uri := docState.uri, version? := some (version?.getD (docState.versionNo - 1)) }
+    textDocument := ⟨docState.uri, some (version?.getD (docState.versionNo - 1))⟩
     publishedModules
   }
   let requestID ← sendRequest Beam.LSP.ImportBasis.checkMethod (toJson params)

tests/lean/BeamTest/LSP/TestRunner.lean

@@ -105,7 +105,7 @@ private def buildParams (runner : Lean.Server.Test.Runner.RunnerState) (paramsTe
   let Except.ok params := Json.parse paramsText
     | throw <| IO.userError s!"failed to parse {paramsText}"
   let params := params.setObjVal! "textDocument" <|
-    toJson ({ uri := runner.uri, version? := some (runner.versionNo - 1) : VersionedTextDocumentIdentifier })
+    toJson (VersionedTextDocumentIdentifier.mk runner.uri (some (runner.versionNo - 1)))
   let params := params.setObjVal! "position" (toJson runner.pos)
   pure params