WorkspaceEdits fail when targeting a URI without a version #16236

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)
• When reporting a perceived soundness bug: Does it affect lake check --paranoid?
  If in doubt, please reach out on security@lean-fro.org for responsible disclosure.

Description

LSP requires OptionalVersionedTextIdentifiers to have a (non-optional) version: integer | null field. However, Lean's VersionedTextIdentifer (which seems to also be used for the Optional* version) allows version? : Option Nat := none. The ToJson deriving handler sees the ? at the end of the field name, and omits the entire field from the resulting json when version? := none instead of providing it as "version": null (as it should).

As a result, VS code will reject edits to URIs that do not (or cannot) have a version, such as edits to newly-created files or cross-file edits on unopened files. (Note how VS code's metamodel of the LSP (assuming I'm looking at something meaningful here) does not have "optional": true for version.)

Context

This arose when developing ImportGraph tooling for Mathlib to allow users to transport declarations out of the current file and into a new one. (Claude pinpointed the bug. Note: this issue was human-written.)

It can be worked around in a widget by modifying the json manually, or by using version? := some 0, which works "accidentally" (but my understanding is that this is really not correct, and "versions" are only a property of opened files).

Steps to Reproduce

(Claude assisted in creating this MWE.)

import Lean

open Lean Server Lsp

-- Note: field is omitted:
/-- info: {"uri": "new"} -/
#guard_msgs in
run_cmd logInfo s!"{toJson { uri := "new", version? := none : VersionedTextDocumentIdentifier }}"

-- 1. Create a code action that attempts to create a file `New.txt` adjacent to the current one and edits it -/
@[code_action_provider]
def versionNullRepro : CodeActionProvider := fun params _ => do
  -- File `New.txt` adjacent to this one
  let some new := System.Uri.fileUriToPath? params.textDocument.uri |>.map fun path =>
      System.Uri.pathToUri <| path.withFileName "New.txt"
    | return #[]
  let insert : TextEdit := { range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, newText := "edited!" }
  let title := "Create New.txt"
  return #[{
    eager := { title }
    lazy? := some <| pure { title, edit? := some {
      documentChanges? := some #[
        .create { uri := new },
        -- No `version?` available since it hasn't been opened, so should use `none` (the default):
        .edit {
            textDocument := { uri := new, version? := none }
            edits := #[insert] }
      ]}}}]

-- 2. Try code action anywhere
example : True := trivial

Expected behavior: The new file is created and has the text "edited!"

Actual behavior: No file is created and the code action silently fails. (Note that all the document changes are rejected, including .create, even though .create's argument does not even take a version?.)

Versions

4.37.0-nightly-2026-11-03, macOS

Additional Information

Note: it seems to me like the "correct" fix (short of introducing a new corresponding OptionalVersionedTextIdentifier in Lean) would be to simply rename the field version? to version, as ? is meant to be used only for optional fields. Then the ToJson deriving handler would automatically retain the field and its value of none would become null. However, this would be a breaking change.

UPDATE: After trying this out downstream in #16237, it seems ProofWidgets4 just needs a 1-line change.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.