Skip to content

fix: tolerate Lean document identifier field rename - #422

Open
ejgallego wants to merge 2 commits into
mainfrom
fix/lsp-version-field-compat
Open

ejgallego wants to merge 2 commits into
mainfrom
fix/lsp-version-field-compat

Conversation

@ejgallego

@ejgallego ejgallego commented Nov 13, 2026 •

Copy link
Copy Markdown
Collaborator

This PR keeps Beam compatible with the VersionedTextDocumentIdentifier field rename in leanprover/lean4#16237, reverted by leanprover/lean4#16356. Positional construction and matching let the same source compile before and after the rename while preserving snapshot version checks and progress filtering.

  • Keep the default toolchain and supported release window unchanged, and document the compatibility boundary and removal condition.
  • Cover missing and null versions as raw JSON: progress notifications accept either, while snapshot-bound requests reject both and leave the document usable. Retain progress coverage for stale, current, and newer versions.
  • Qualified on Linux x86-64 against the exact #16237 head (03b566a584a43808b6a4fd430b2842b5e087d3cc): tests/test-lsp.sh and the broker pending tests pass with the strengthened assertions. This exercises the reverted API change, which the current pinned-toolchain CI cannot cover.

@ejgallego
ejgallego marked this pull request as ready for review November 13, 2026 14:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant