fix: make applyEdit optional in WorkspaceClientCapabilities of LSP

The `applyEdit` field should be optional in `WorkspaceClientCapabilities` by the
LSP spec and some clients don't populate it in requests

Closes leanprover#4541

src/Lean/Data/Lsp/Capabilities.lean

@@ -54,7 +54,7 @@ structure WorkspaceEditClientCapabilities where
   deriving ToJson, FromJson
 
 structure WorkspaceClientCapabilities where
-  applyEdit: Bool
+  applyEdit? : Option Bool := none
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 

tests/lean/server/init_exit_with_zed.lean

@@ -0,0 +1,13 @@
+import Lean.Data.Lsp
+open IO Lean Lsp
+
+def main : IO Unit := do
+  Ipc.runWith (←IO.appPath) #["--server"] do
+    let hIn ← Ipc.stdin
+    hIn.write (←FS.readBinFile "init_zed_0_150_4.log")
+    hIn.flush
+    let initResp ← Ipc.readResponseAs 0 InitializeResult
+    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
+
+    Ipc.shutdown 1
+    discard Ipc.waitForExit

tests/lean/server/init_zed_0_150_4.log

@@ -0,0 +1,3 @@
+Content-Length: 1858
+
+{"params":{"workspaceFolders":[{"uri":"file:///tmp","name":""}],"rootUri":"file:///tmp","processId":null,"clientInfo":{"version":"0.150.4","name":"Zed"},"capabilities":{"workspace":{"workspaceFolders":true,"workspaceEdit":{"snippetEditSupport":true,"resourceOperations":["create","rename","delete"],"documentChanges":true},"symbol":{},"inlayHint":{"refreshSupport":true},"didChangeWatchedFiles":{"relativePatternSupport":true,"dynamicRegistration":true},"didChangeConfiguration":{"dynamicRegistration":true},"diagnostic":{},"configuration":true},"window":{"workDoneProgress":true},"textDocument":{"synchronization":{"didSave":true},"signatureHelp":{"signatureInformation":{"parameterInformation":{"labelOffsetSupport":true},"documentationFormat":["markdown","plaintext"],"activeParameterSupport":true}},"rename":{"prepareSupport":true},"rangeFormatting":{"dynamicRegistration":true},"publishDiagnostics":{"relatedInformation":true},"onTypeFormatting":{"dynamicRegistration":true},"inlayHint":{"resolveSupport":{"properties":["textEdits","tooltip","label.tooltip","label.location","label.command"]},"dynamicRegistration":false},"hover":{"contentFormat":["markdown"]},"formatting":{"dynamicRegistration":true},"definition":{"linkSupport":true},"completion":{"contextSupport":true,"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextMode","data"]},"completionItem":{"snippetSupport":true,"resolveSupport":{"properties":["documentation","additionalTextEdits"]},"labelDetailsSupport":true,"insertReplaceSupport":true}},"codeAction":{"resolveSupport":{"properties":["kind","diagnostics","isPreferred","disabled","edit","command"]},"dataSupport":true,"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["refactor","quickfix","source"]}}}},"experimental":{"serverStatusNotification":true}}},"method":"initialize","jsonrpc":"2.0","id":0}