From 61c74f429433ea7142161aca7d6f02e63b5d1f54 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 9 Nov 2026 06:15:58 -0800
Subject: [PATCH 1/2] fix: tolerate Lean 4.37 document identifier field rename

---
 Beam/Broker/Pending.lean                    |  3 ++-
 Beam/Broker/Server.lean                     | 12 +++++------
 Beam/LSP/Lib/Request.lean                   |  7 +++---
 CHANGELOG.md                                |  2 ++
 tests/lean/BeamTest/Broker/PendingTest.lean | 24 +++++++++++++++++++--
 tests/lean/BeamTest/LSP/Scenario.lean       | 21 ++++++------------
 tests/lean/BeamTest/LSP/TestRunner.lean     |  2 +-
 7 files changed, 43 insertions(+), 28 deletions(-)

diff --git a/Beam/Broker/Pending.lean b/Beam/Broker/Pending.lean
index e3260bc78..9cfbf9ca1 100644
--- a/Beam/Broker/Pending.lean
+++ b/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
 
diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean
index cb2aabfbe..651534f95 100644
--- a/Beam/Broker/Server.lean
+++ b/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)]
diff --git a/Beam/LSP/Lib/Request.lean b/Beam/LSP/Lib/Request.lean
index 50c422040..c5e3f00e6 100644
--- a/Beam/LSP/Lib/Request.lean
+++ b/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
diff --git a/CHANGELOG.md b/CHANGELOG.md
index df5c8d477..89404c294 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,6 +23,8 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Fixed
 
+- Keep snapshot-bound requests and progress notifications compatible with Lean 4.37's
+  `VersionedTextDocumentIdentifier` field rename, 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,
diff --git a/tests/lean/BeamTest/Broker/PendingTest.lean b/tests/lean/BeamTest/Broker/PendingTest.lean
index 62fbb8ca2..8d4144dc0 100644
--- a/tests/lean/BeamTest/Broker/PendingTest.lean
+++ b/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,24 @@ private def checkSyncFileProgressLines : IO Unit := do
   requireFieldAbsent "finished progress" "totalLines" renderedProgress
   requireJsonInt "finished progress" "rangeEndLine" 13 renderedProgress
 
+/-- Exercise the wire identifier as well as progress selection: Lean 4.37 briefly renamed its
+optional version field, but neither missing versions nor stale progress may change meaning. -/
+private def checkSyncFileProgressVersionSelection : IO Unit := do
+  for (version?, expectedUpdates) in [
+      (none, 1), (some 0, 0), (some 1, 1), (some 2, 1)] do
+    let params := mkFileProgress #[mkRange 0 0 1 0] version?
+    let decoded : LeanFileProgressParams ← match fromJson? (toJson params) with
+      | .ok value => pure value
+      | .error error => throw <| IO.userError s!"fileProgress identifier round trip: {error}"
+    let pending ← mkPending
+      (progress? := some {})
+      (tracked? := some ("file:///workspace/Foo.lean", 1))
+    PendingRequest.observeProgress pending decoded
+    let some progress ← pending.progressRef.get
+      | throw <| IO.userError "versioned fileProgress cleared progress"
+    require s!"fileProgress version {version?} selects only current or unversioned progress"
+      (progress.updates == expectedUpdates)
+
 private def checkDiagnosticLineCanExceedProgressRange : IO Unit := do
   let active ← observeFileProgress {} #[mkRange 0 0 1 0]
   let finished ← observeFileProgress active #[]
@@ -601,6 +620,7 @@ def main : IO Unit := do
   checkPendingResolveError
   checkSyncFileProgressDisplay
   checkSyncFileProgressLines
+  checkSyncFileProgressVersionSelection
   checkDiagnosticLineCanExceedProgressRange
   checkDiagnosticEmitterFailureIsolation
   checkProgressEmitterFailureIsolation
diff --git a/tests/lean/BeamTest/LSP/Scenario.lean b/tests/lean/BeamTest/LSP/Scenario.lean
index a76ce777a..0c97af190 100644
--- a/tests/lean/BeamTest/LSP/Scenario.lean
+++ b/tests/lean/BeamTest/LSP/Scenario.lean
@@ -368,7 +368,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 +429,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 +454,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 +464,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 +480,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 +528,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)
diff --git a/tests/lean/BeamTest/LSP/TestRunner.lean b/tests/lean/BeamTest/LSP/TestRunner.lean
index 19d7b1712..cdd89dd23 100644
--- a/tests/lean/BeamTest/LSP/TestRunner.lean
+++ b/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
 

From a86d3981cdc0b1bff19a29c4e2e94febba751359 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Fri, 13 Nov 2026 15:14:45 +0100
Subject: [PATCH 2/2] test: cover missing and null document versions

---
 CHANGELOG.md                                  |  5 ++--
 docs/COMPATIBILITY.md                         |  6 +++++
 tests/lean/BeamTest/Broker/PendingTest.lean   | 24 ++++++++++---------
 .../LSP/Requests/RunAt/BasicTest.lean         | 20 ++++++++++++++++
 tests/lean/BeamTest/LSP/Scenario.lean         |  5 ++++
 5 files changed, 47 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89404c294..8e455ffcf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,8 +23,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Fixed
 
-- Keep snapshot-bound requests and progress notifications compatible with Lean 4.37's
-  `VersionedTextDocumentIdentifier` field rename, without changing the supported release window.
+- 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,
diff --git a/docs/COMPATIBILITY.md b/docs/COMPATIBILITY.md
index c36f380b0..d42bc8378 100644
--- a/docs/COMPATIBILITY.md
+++ b/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.
diff --git a/tests/lean/BeamTest/Broker/PendingTest.lean b/tests/lean/BeamTest/Broker/PendingTest.lean
index 8d4144dc0..f71b3fefb 100644
--- a/tests/lean/BeamTest/Broker/PendingTest.lean
+++ b/tests/lean/BeamTest/Broker/PendingTest.lean
@@ -488,22 +488,24 @@ private def checkSyncFileProgressLines : IO Unit := do
   requireFieldAbsent "finished progress" "totalLines" renderedProgress
   requireJsonInt "finished progress" "rangeEndLine" 13 renderedProgress
 
-/-- Exercise the wire identifier as well as progress selection: Lean 4.37 briefly renamed its
-optional version field, but neither missing versions nor stale progress may change meaning. -/
+/-- Both wire encodings of an unknown version must preserve progress selection. -/
 private def checkSyncFileProgressVersionSelection : IO Unit := do
-  for (version?, expectedUpdates) in [
-      (none, 1), (some 0, 0), (some 1, 1), (some 2, 1)] do
-    let params := mkFileProgress #[mkRange 0 0 1 0] version?
-    let decoded : LeanFileProgressParams ← match fromJson? (toJson params) with
-      | .ok value => pure value
-      | .error error => throw <| IO.userError s!"fileProgress identifier round trip: {error}"
+  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 ("file:///workspace/Foo.lean", 1))
-    PendingRequest.observeProgress pending decoded
+      (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 {version?} selects only current or unversioned progress"
+    require s!"fileProgress version filtering: {param.compress}"
       (progress.updates == expectedUpdates)
 
 private def checkDiagnosticLineCanExceedProgressRange : IO Unit := do
diff --git a/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean b/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean
index 851ef272a..e0cf6e785 100644
--- a/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean
+++ b/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
diff --git a/tests/lean/BeamTest/LSP/Scenario.lean b/tests/lean/BeamTest/LSP/Scenario.lean
index 0c97af190..df783e53a 100644
--- a/tests/lean/BeamTest/LSP/Scenario.lean
+++ b/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