From 3b0f57f0a1e47d1b790a9c3474723ece3e4e0a16 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Mar 2026 11:30:08 +0100 Subject: [PATCH] refactor: split runAt request modules and harden broker flows --- Beam.lean | 1 + Beam/Broker/Deps.lean | 96 ++ Beam/Broker/Server.lean | 871 +++++------------- Beam/Broker/SyncSaveSupport.lean | 130 +++ RunAt/Lib/Goals.lean | 138 +++ RunAt/Lib/Handles.lean | 155 ++++ RunAt/Lib/Support.lean | 171 ++++ RunAt/Plugin.lean | 716 +------------- RunAt/Requests/DirectImports.lean | 38 + RunAt/Requests/Goals.lean | 31 + RunAt/Requests/RunAt.lean | 155 ++++ RunAt/Requests/Save.lean | 174 ++++ RunAtTest/Broker/StartupHandshakeTest.lean | 69 ++ .../Broker/StartupHandshakeTestMain.lean | 9 + RunAtTest/Handle/LifecycleTest.lean | 83 ++ RunAtTest/RequestSurfaceTest.lean | 104 +++ RunAtTest/Scenario.lean | 87 +- lakefile.lean | 9 + tests/test-broker-fast.sh | 2 + tests/test.sh | 14 +- 20 files changed, 1694 insertions(+), 1359 deletions(-) create mode 100644 Beam/Broker/SyncSaveSupport.lean create mode 100644 RunAt/Lib/Goals.lean create mode 100644 RunAt/Lib/Handles.lean create mode 100644 RunAt/Lib/Support.lean create mode 100644 RunAt/Requests/DirectImports.lean create mode 100644 RunAt/Requests/Goals.lean create mode 100644 RunAt/Requests/RunAt.lean create mode 100644 RunAt/Requests/Save.lean create mode 100644 RunAtTest/Broker/StartupHandshakeTest.lean create mode 100644 RunAtTest/Broker/StartupHandshakeTestMain.lean create mode 100644 RunAtTest/Handle/LifecycleTest.lean create mode 100644 RunAtTest/RequestSurfaceTest.lean diff --git a/Beam.lean b/Beam.lean index 90f847f7..966bf95e 100644 --- a/Beam.lean +++ b/Beam.lean @@ -10,5 +10,6 @@ import Beam.Broker.Deps import Beam.Broker.LakeSave import Beam.Broker.Lean import Beam.Broker.Protocol +import Beam.Broker.SyncSaveSupport import Beam.Broker.Transport import Beam.Broker.UnixNative diff --git a/Beam/Broker/Deps.lean b/Beam/Broker/Deps.lean index 388cb5c9..e5db43c4 100644 --- a/Beam/Broker/Deps.lean +++ b/Beam/Broker/Deps.lean @@ -58,6 +58,102 @@ def normalizeModuleForPath (root path : System.FilePath) (uri : DocumentUri) (mo | some name => some { name, uri } | none => none +structure DirectImportsQueryResult where + version : Nat + imports : Array String := #[] + deriving Inhabited + +structure ModuleHistorySnapshot where + path : String + lastSyncSeq : Nat := 0 + lastSaveSeq : Nat := 0 + deriving Inhabited + +structure StaleDirectDepHint where + module : String + path : String + needsSave : Bool + lastSyncSeq : Nat + lastSaveSeq : Nat + deriving Inhabited + +def moduleJson (root : System.FilePath) (module : LeanModule) : Json := + let path? := workspacePath? root module.uri + Json.mkObj <| + [ + ("name", toJson module.name), + ("uri", toJson module.uri), + ("workspace", toJson path?.isSome) + ] ++ + match path? with + | some path => [("path", toJson path)] + | none => [] + +def importJson (root : System.FilePath) (imp : LeanImport) : Json := + Json.mkObj [ + ("module", moduleJson root imp.module), + ("kind", toJson imp.kind) + ] + +def depsPayload (root : System.FilePath) (module : LeanModule) + (imports importedBy : Array LeanImport) + (importClosure importedByClosure : Std.TreeMap String LeanImport) : Json := + Json.mkObj [ + ("module", moduleJson root module), + ("imports", Json.arr <| imports.map (importJson root)), + ("importedBy", Json.arr <| importedBy.map (importJson root)), + ("importClosure", Json.arr <| importClosure.toList.map (fun (_, imp) => importJson root imp) |>.toArray), + ("importedByClosure", Json.arr <| importedByClosure.toList.map (fun (_, imp) => importJson root imp) |>.toArray) + ] + +def staleDirectDepHintJson (hint : StaleDirectDepHint) : Json := + Json.mkObj [ + ("module", toJson hint.module), + ("path", toJson hint.path), + ("needsSave", toJson hint.needsSave), + ("lastSyncSeq", toJson hint.lastSyncSeq), + ("lastSaveSeq", toJson hint.lastSaveSeq) + ] + +def staleSyncErrorData + (targetPath : String) + (hints : Array StaleDirectDepHint) : Json := + let saveHints := hints.filter (·.needsSave) + let recoveryPlan := + (saveHints.map fun hint => s!"lean-beam save \"{hint.path}\"") ++ + #[s!"lean-beam refresh \"{targetPath}\"", "lake build"] + Json.mkObj [ + ("targetPath", toJson targetPath), + ("staleDirectDeps", Json.arr <| hints.map staleDirectDepHintJson), + ("saveDeps", Json.arr <| saveHints.map (fun hint => toJson hint.path)), + ("recoveryPlan", Json.arr <| recoveryPlan.map toJson) + ] + +def collectStaleDirectDepHints + (importsResult : DirectImportsQueryResult) + (version : Nat) + (targetLastSyncSeq : Nat) + (history : Std.TreeMap String ModuleHistorySnapshot) + : Array StaleDirectDepHint := + if importsResult.version != version then + #[] + else + importsResult.imports.foldl (init := #[]) fun hints moduleName => + match history.get? moduleName with + | some moduleHistory => + if moduleHistory.lastSaveSeq > targetLastSyncSeq then + hints.push { + module := moduleName + path := moduleHistory.path + needsSave := moduleHistory.lastSaveSeq < moduleHistory.lastSyncSeq + lastSyncSeq := moduleHistory.lastSyncSeq + lastSaveSeq := moduleHistory.lastSaveSeq + } + else + hints + | none => + hints + def importInfoToWorkspaceImport? (moduleIndex : Std.TreeMap String System.FilePath) (info : ImportInfo) : Option LeanImport := do diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean index 645a6a76..7d2bf991 100644 --- a/Beam/Broker/Server.lean +++ b/Beam/Broker/Server.lean @@ -18,6 +18,7 @@ import Beam.Broker.Transport import Beam.Broker.Lean import Beam.Broker.Deps import Beam.Broker.LakeSave +import Beam.Broker.SyncSaveSupport import Std.Sync.Mutex open Lean @@ -117,6 +118,77 @@ structure State where abbrev M := StateRefT State IO +inductive BrokerFailureCode where + | invalidParams + | requestCancelled + | contentModified + | workerExited + | syncBarrierIncomplete + | saveTargetNotModule + | internalError + deriving Inhabited, BEq, Repr + +def BrokerFailureCode.name : BrokerFailureCode → String + | .invalidParams => "invalidParams" + | .requestCancelled => "requestCancelled" + | .contentModified => "contentModified" + | .workerExited => "workerExited" + | .syncBarrierIncomplete => syncBarrierIncompleteCode + | .saveTargetNotModule => saveTargetNotModuleCode + | .internalError => "internalError" + +instance : ToJson BrokerFailureCode where + toJson code := toJson code.name + +instance : FromJson BrokerFailureCode where + fromJson? j := + match j with + | .str "invalidParams" => .ok .invalidParams + | .str "requestCancelled" => .ok .requestCancelled + | .str "contentModified" => .ok .contentModified + | .str "workerExited" => .ok .workerExited + | .str s => + if s == syncBarrierIncompleteCode then + .ok .syncBarrierIncomplete + else if s == saveTargetNotModuleCode then + .ok .saveTargetNotModule + else if s == "internalError" then + .ok .internalError + else + .error s!"expected broker failure code, got {j.compress}" + | _ => .error s!"expected broker failure code, got {j.compress}" + +structure BrokerFailure where + code : BrokerFailureCode + message : String := "" + data? : Option Json := none + deriving Inhabited, FromJson, ToJson + +private def brokerFailurePrefix : String := + "brokerfail:" + +def BrokerFailure.toResponse (failure : BrokerFailure) : Response := + { + ok := false + error? := some { + code := failure.code.name + message := failure.message + data? := failure.data? + } + } + +def brokerFailureMessage (failure : BrokerFailure) : String := + s!"{brokerFailurePrefix}{(toJson failure).compress}" + +def throwBrokerFailure (failure : BrokerFailure) : IO α := do + throw <| IO.userError (brokerFailureMessage failure) + +def decodeBrokerFailure? (msg : String) : Option BrokerFailure := do + guard <| msg.startsWith brokerFailurePrefix + let raw := msg.drop brokerFailurePrefix.length |>.toString + let json ← Json.parse raw |>.toOption + fromJson? json |>.toOption + def mkSessionToken : IO String := do let pid ← IO.Process.getPID let now ← IO.monoNanosNow @@ -391,67 +463,6 @@ private def diagnosticDisplayPath (root : System.FilePath) (uri : DocumentUri) : private def diagnosticStreamKey (diagnostic : Diagnostic) : String := (toJson diagnostic).compress -private def isIncompleteBarrierDiagnostic (diagnostic : Diagnostic) : Bool := - diagnostic.message.contains "Failed to build module dependencies." || - diagnostic.message.contains "error: target is out-of-date and needs to be rebuilt" - -private def effectiveSyncDiagnosticSeverity (diagnostic : Diagnostic) : - Option DiagnosticSeverity := - if isIncompleteBarrierDiagnostic diagnostic then - some .error - else - diagnostic.severity? - -private def filterSyncDiagnostics (fullDiagnostics : Bool) (diagnostics : Array Diagnostic) : - Array Diagnostic := - if fullDiagnostics then - diagnostics - else - diagnostics.filter (fun diagnostic => effectiveSyncDiagnosticSeverity diagnostic == some .error) - -private def syncErrorCount (diagnostics : Array Diagnostic) : Nat := - diagnostics.foldl (init := 0) fun count diagnostic => - if effectiveSyncDiagnosticSeverity diagnostic == some .error then - count + 1 - else - count - -private def syncWarningCount (diagnostics : Array Diagnostic) : Nat := - diagnostics.foldl (init := 0) fun count diagnostic => - if effectiveSyncDiagnosticSeverity diagnostic == some .warning then - count + 1 - else - count - -private structure SyncSaveReadiness where - stateErrorCount : Nat := 0 - stateCommandErrorCount : Nat := 0 - saveReady : Bool := true - saveReadyReason : String := "ok" - deriving Inhabited - -private def syncSaveReadinessOfResult - (result : RunAt.Internal.SaveReadinessResult) : SyncSaveReadiness := - { - stateErrorCount := result.diagnosticErrorCount - stateCommandErrorCount := result.commandErrorCount - saveReady := result.saveReady - saveReadyReason := result.saveReadyReason - } - -private structure DirectImportsQueryResult where - version : Nat - imports : Array String := #[] - deriving Inhabited - -private structure StaleDirectDepHint where - module : String - path : String - needsSave : Bool - lastSyncSeq : Nat - lastSaveSeq : Nat - deriving Inhabited - private def emitNewTrackedDiagnostics (root : System.FilePath) (seen : Std.TreeSet String compare) @@ -582,7 +593,10 @@ partial def sessionReaderLoop (session : Session) : IO Unit := do pure () sessionReaderLoop session catch e => - failAllPendingRequests session s!"workerExited: {e.toString}" + failAllPendingRequests session <| brokerFailureMessage { + code := .workerExited + message := e.toString + } try session.proc.kill catch _ => @@ -681,6 +695,33 @@ def sendRequestJson (session : Session) (method : String) (param : Json) : IO (S let (session, result, _) ← sendRequestJsonTracked session method param pure (session, result) +private partial def awaitInitializeResponse (stdout : IO.FS.Stream) : IO Unit := do + let msg ← stdout.readLspMessage + match msg with + | .response id _ => + if id == 0 then + pure () + else + throwBrokerFailure { + code := .internalError + message := s!"unexpected response id {id} before initialize completed" + } + | .responseError id _code message _ => + if id == 0 then + throwBrokerFailure { code := .internalError, message := s!"initialize failed: {message}" } + else + throwBrokerFailure { + code := .internalError + message := s!"unexpected response error id {id} before initialize completed: {message}" + } + | .notification .. => + awaitInitializeResponse stdout + | .request .. => + throwBrokerFailure { + code := .internalError + message := "unexpected server request before initialize completed" + } + def ensureSession (backend : Backend) : M Session := do let state ← get let config := state.config @@ -722,7 +763,7 @@ def ensureSession (backend : Backend) : M Session := do pending } writeLspRequest stdin ({ id := 0, method := "initialize", param := initializeParams backend root : Lean.JsonRpc.Request Json }) - let _ ← stdout.readLspMessage + awaitInitializeResponse stdout writeLspNotification stdin ({ method := "initialized", param := Json.mkObj [] : Lean.JsonRpc.Notification Json }) let _ ← IO.asTask do try @@ -842,46 +883,6 @@ def recordFileProgress (session : Session) (uri : DocumentUri) | none => session -private def diagnosticsIndicateIncompleteBarrier (diagnostics : Array Diagnostic) : Bool := - diagnostics.any isIncompleteBarrierDiagnostic - -private def incompleteBarrierProgress (progress? : Option SyncFileProgress := none) : SyncFileProgress := - match progress? with - | some progress => { progress with done := false } - | none => { done := false } - -private def syncBarrierIncompleteMessage - (uri : DocumentUri) - (version : Nat) - (progress? : Option SyncFileProgress) : String := - let progress := incompleteBarrierProgress progress? - s!"Lean diagnostics barrier did not complete for {uri} at version {version}; " ++ - s!"fileProgress={toJson progress |>.compress}. An imported target may be stale or broken, " ++ - s!"or the Lean worker may have exited. Run `lake build` or fix the upstream module first." - -private def syncBarrierIncomplete? - (progress? : Option SyncFileProgress) - (diagnostics : Array Diagnostic := #[]) : Bool := - if diagnosticsIndicateIncompleteBarrier diagnostics then - true - else - match progress? with - | some progress => !progress.done - | none => false - -private def effectiveSyncBarrierProgress - (priorProgress? : Option SyncFileProgress) - (progress? : Option SyncFileProgress) - (diagnostics : Array Diagnostic) : Option SyncFileProgress := - if diagnosticsIndicateIncompleteBarrier diagnostics then - some <| incompleteBarrierProgress (progress?.or priorProgress?) - else - match progress? with - | some progress => - some progress - | none => - some <| priorProgress?.getD {} - def decodeResponseAs [FromJson α] (json : Json) : IO α := do match fromJson? json with | .ok value => pure value @@ -908,7 +909,10 @@ private def ensureSyncBarrierComplete (progress? : Option SyncFileProgress) (diagnostics : Array Diagnostic := #[]) : IO Unit := do if syncBarrierIncomplete? progress? diagnostics then - throw <| IO.userError <| syncBarrierIncompleteMessage uri version progress? + throwBrokerFailure { + code := .syncBarrierIncomplete + message := syncBarrierIncompleteMessage uri version progress? + } def waitForDiagnostics (session : Session) (uri : DocumentUri) (version : Nat) : IO Session := do let params := toJson (WaitForDiagnosticsParams.mk uri version) @@ -1024,43 +1028,6 @@ private def markDocSavedVersion (session : Session) (uri : DocumentUri) (version | none => session -def moduleJson (root : System.FilePath) (module : LeanModule) : Json := - let path? := workspacePath? root module.uri - Json.mkObj <| - [ - ("name", toJson module.name), - ("uri", toJson module.uri), - ("workspace", toJson path?.isSome) - ] ++ - match path? with - | some path => [("path", toJson path)] - | none => [] - -def leanSavePayload (spec : LeanSaveSpec) (version : Nat) (sourceHash : Lake.Hash) : Json := - Json.mkObj <| - [ - ("path", toJson spec.relPath), - ("module", toJson spec.moduleName.toString), - ("version", toJson version), - ("sourceHash", toJson sourceHash), - ("olean", toJson spec.oleanPath.toString), - ("ilean", toJson spec.ileanPath.toString), - ("c", toJson spec.cPath.toString), - ("trace", toJson spec.tracePath.toString) - ] ++ - (match spec.oleanServerPath? with - | some path => [("oleanServer", toJson path.toString)] - | none => []) ++ - (match spec.oleanPrivatePath? with - | some path => [("oleanPrivate", toJson path.toString)] - | none => []) ++ - (match spec.irPath? with - | some path => [("ir", toJson path.toString)] - | none => []) ++ - (match spec.bcPath? with - | some path => [("bc", toJson path.toString)] - | none => []) - def saveOlean (leanCmd? : Option String) (session : Session) @@ -1118,23 +1085,6 @@ def saveOlean })) pure (markDocSavedVersion session uri docState.version, leanSavePayload spec docState.version docState.textTraceHash, fileProgress?) -def importJson (root : System.FilePath) (imp : LeanImport) : Json := - Json.mkObj [ - ("module", moduleJson root imp.module), - ("kind", toJson imp.kind) - ] - -def depsPayload (root : System.FilePath) (module : LeanModule) - (imports importedBy : Array LeanImport) - (importClosure importedByClosure : Std.TreeMap String LeanImport) : Json := - Json.mkObj [ - ("module", moduleJson root module), - ("imports", Json.arr <| imports.map (importJson root)), - ("importedBy", Json.arr <| importedBy.map (importJson root)), - ("importClosure", Json.arr <| importClosure.toList.map (fun (_, imp) => importJson root imp) |>.toArray), - ("importedByClosure", Json.arr <| importedByClosure.toList.map (fun (_, imp) => importJson root imp) |>.toArray) - ] - private def docSyncStatus (path : System.FilePath) (docState : DocState) : IO String := do if !(← path.pathExists) then pure "missing" @@ -1290,16 +1240,6 @@ def withFileProgress (resp : Response) (fileProgress? : Option SyncFileProgress) | some progress => { resp with fileProgress? := some progress } | none => resp -def currentFileProgressSink? : M (Option (SyncFileProgress → IO Unit)) := do - let state ← get - pure <| state.streamSink?.map fun emit => - fun progress => emit (StreamMessage.mkFileProgress state.currentClientRequestId? progress) - -def currentDiagnosticSink? : M (Option (StreamDiagnostic → IO Unit)) := do - let state ← get - pure <| state.streamSink?.map fun emit => - fun diagnostic => emit (StreamMessage.mkDiagnostic state.currentClientRequestId? diagnostic) - def updateSession (session : Session) : M Unit := do modify fun state => let backendState := getBackendState state session.backend @@ -1362,7 +1302,9 @@ private def isWorkerExitedMessage (msg : String) : Bool := msg.startsWith "workerExited:" private def responseForExceptionMessage (msg : String) : Response := - if isRequestCancelledMessage msg then + if let some failure := decodeBrokerFailure? msg then + failure.toResponse + else if isRequestCancelledMessage msg then reqError "requestCancelled" msg else if isContentModifiedMessage msg then reqError "contentModified" msg @@ -1377,178 +1319,6 @@ private def responseForExceptionMessage (msg : String) : Response := else reqError "internalError" msg -def handleEnsureOp (req : Request) (session : Session) : M (Response × Bool) := do - let payload := Json.mkObj [ - ("backend", toJson req.backend), - ("root", toJson session.root.toString), - ("epoch", toJson session.epoch), - ] - pure (sessionResult session payload, false) - -def handleSyncFileOp (req : Request) (session : Session) : M (Response × Bool) := do - try - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let path ← resolvePath session.root path - let session ← syncFile session path - let uri := sessionUri path - let docState ← requireDocState session uri - let emitProgress? ← currentFileProgressSink? - let emitDiagnostic? ← currentDiagnosticSink? - let fullDiagnostics := req.fullDiagnostics?.getD false - let (session, fileProgress?, diagnostics) ← - waitForSyncBarrierWithDiagnostics session uri docState.version - emitProgress? fullDiagnostics emitDiagnostic? - let (session, saveReadiness) ← fetchSyncSaveReadiness session uri - let session := markDocSyncedVersion (recordFileProgress session uri fileProgress?) uri docState.version - updateSession session - let payload := toJson ({ - version := docState.version - errorCount := syncErrorCount diagnostics - warningCount := syncWarningCount diagnostics - stateErrorCount := saveReadiness.stateErrorCount - stateCommandErrorCount := saveReadiness.stateCommandErrorCount - saveReady := saveReadiness.saveReady - saveReadyReason := saveReadiness.saveReadyReason - : SyncFileResult - }) - pure (withFileProgress (sessionResult session payload) fileProgress?, false) - catch e => - pure (responseForExceptionMessage e.toString, false) - -def handleCloseOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let (session, savedPayload?, fileProgress?) ← - if req.saveArtifacts?.getD false then - try - let leanCmd? := (← get).config.leanCmd? - let emitProgress? ← currentFileProgressSink? - let emitDiagnostic? ← currentDiagnosticSink? - let fullDiagnostics := req.fullDiagnostics?.getD false - let (session, payload, fileProgress?) ← - saveOlean leanCmd? session path emitProgress? fullDiagnostics emitDiagnostic? - pure (session, some payload, fileProgress?) - catch e => - return (responseForExceptionMessage e.toString, false) - else - pure (session, none, none) - let session ← closeFile session path - updateSession session - let payload := Json.mkObj <| - [("closed", toJson true)] ++ - match savedPayload? with - | some saved => [("saved", saved)] - | none => [] - pure (withFileProgress (sessionResult session payload) fileProgress?, false) - -def handleRunAtOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let line ← - match req.requireLine with - | .ok line => pure line - | .error err => return (reqError "invalidParams" err, false) - let character ← - match req.requireCharacter with - | .ok character => pure character - | .error err => return (reqError "invalidParams" err, false) - let text ← - match req.requireText with - | .ok text => pure text - | .error err => return (reqError "invalidParams" err, false) - let method ← - match runAtMethod req.backend with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let emitProgress? ← currentFileProgressSink? - let params := Json.mkObj <| - [ ("textDocument", toJson ({ uri := uri : TextDocumentIdentifier })) - , ("position", toJson ({ line := line, character := character : Lsp.Position })) - , ("text", toJson text) - ] ++ - match req.storeHandle? with - | some b => [("storeHandle", toJson b)] - | none => [] - try - let (session, result, fileProgress?) ← - sendRequestJsonTracked session method params - (tracked := some (uri, docState.version)) - (emitProgress? := emitProgress?) - let session := recordFileProgress session uri fileProgress? - updateSession session - pure (withFileProgress (sessionResult session (wrapResultHandle session result)) fileProgress?, false) - catch e => - let msg := e.toString - if let some resp := decodeJsonRpcError msg then - pure (resp, false) - else - pure (reqError "internalError" msg, false) - -def handleRequestAtOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let line ← - match req.requireLine with - | .ok line => pure line - | .error err => return (reqError "invalidParams" err, false) - let character ← - match req.requireCharacter with - | .ok character => pure character - | .error err => return (reqError "invalidParams" err, false) - let requestedMethod ← - match req.requireMethod with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let method ← - match requestAtMethod req.backend requestedMethod with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let extraParams ← - match req.requireParamsObject with - | .ok params => pure params - | .error err => return (reqError "invalidParams" err, false) - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let emitProgress? ← currentFileProgressSink? - let params := Json.mergeObj extraParams <| Json.mkObj [ - ("textDocument", toJson ({ uri := uri : TextDocumentIdentifier })), - ("position", toJson ({ line := line, character := character : Lsp.Position })) - ] - try - let tracked := - if session.backend == .lean then - some (uri, docState.version) - else - none - let (session, result, fileProgress?) ← - sendRequestJsonTracked session method params (tracked := tracked) (emitProgress? := emitProgress?) - let session := - if session.backend == .lean then - recordFileProgress session uri fileProgress? - else - session - updateSession session - pure (withFileProgress (sessionResult session result) fileProgress?, false) - catch e => - let msg := e.toString - if let some resp := decodeJsonRpcError msg then - pure (resp, false) - else - pure (reqError "internalError" msg, false) - def handleDepsOp (req : Request) : M (Response × Bool) := do let path ← match req.requirePath with @@ -1573,181 +1343,6 @@ def handleDepsOp (req : Request) : M (Response × Bool) := do else pure (reqError "internalError" msg, false) -def handleSaveOleanOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - try - let leanCmd? := (← get).config.leanCmd? - let emitProgress? ← currentFileProgressSink? - let emitDiagnostic? ← currentDiagnosticSink? - let fullDiagnostics := req.fullDiagnostics?.getD false - let (session, payload, fileProgress?) ← - saveOlean leanCmd? session path emitProgress? fullDiagnostics emitDiagnostic? - let uri := sessionUri (← resolvePath session.root path) - let session := recordFileProgress session uri fileProgress? - updateSession session - pure (withFileProgress (sessionResult session payload) fileProgress?, false) - catch e => - pure (responseForExceptionMessage e.toString, false) - -def handleGoalsOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let line ← - match req.requireLine with - | .ok line => pure line - | .error err => return (reqError "invalidParams" err, false) - let character ← - match req.requireCharacter with - | .ok character => pure character - | .error err => return (reqError "invalidParams" err, false) - let method ← - match goalsMethod req.backend req.mode? with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - if req.backend == .lean && req.text?.isSome then - return (reqError "invalidParams" "lean goals does not accept speculative text; use lean-run-at for execution", false) - let position : Lsp.Position := { line := line, character := character } - let params := - match req.backend with - | .lean => - Json.mkObj [ - ("textDocument", - toJson ({ uri := uri : TextDocumentIdentifier })), - ("position", toJson position) - ] - | .rocq => - let fields := - [ - ("textDocument", toJson ({ uri := uri, version? := some docState.version : VersionedTextDocumentIdentifier })), - ("position", toJson position), - ("mode", toJson (goalModeValue req.mode?)), - ("compact", toJson (req.compact?.getD false)), - ("pp_format", toJson (goalPpFormatValue req.ppFormat?)) - ] ++ - match req.text? with - | some text => [("command", toJson text)] - | none => [] - Json.mkObj fields - try - let tracked := - if session.backend == .lean then - some (uri, docState.version) - else - none - let emitProgress? ← currentFileProgressSink? - let (session, result, fileProgress?) ← - sendRequestJsonTracked session method params (tracked := tracked) (emitProgress? := emitProgress?) - let session := - if session.backend == .lean then - recordFileProgress session uri fileProgress? - else - session - updateSession session - pure (withFileProgress (sessionResult session result) fileProgress?, false) - catch e => - let msg := e.toString - if let some resp := decodeJsonRpcError msg then - pure (resp, false) - else - pure (reqError "internalError" msg, false) - -def handleRunWithOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let handle ← - match req.requireHandle with - | .ok handle => pure handle - | .error err => return (reqError "invalidParams" err, false) - let rawHandle ← - match unwrapHandle session handle with - | .ok raw => pure raw - | .error err => return (reqError "contentModified" err, false) - let text ← - match req.requireText with - | .ok text => pure text - | .error err => return (reqError "invalidParams" err, false) - let method ← - match runWithMethod req.backend with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let emitProgress? ← currentFileProgressSink? - let params := Json.mkObj <| - [ ("textDocument", toJson ({ uri := uri : TextDocumentIdentifier })) - , ("handle", rawHandle) - , ("text", toJson text) - ] ++ (match req.storeHandle? with - | some b => [("storeHandle", toJson b)] - | none => []) ++ - (match req.linear? with - | some b => [("linear", toJson b)] - | none => []) - try - let (session, result, fileProgress?) ← - sendRequestJsonTracked session method params - (tracked := some (uri, docState.version)) - (emitProgress? := emitProgress?) - let session := recordFileProgress session uri fileProgress? - updateSession session - pure (withFileProgress (sessionResult session (wrapResultHandle session result)) fileProgress?, false) - catch e => - let msg := e.toString - if let some resp := decodeJsonRpcError msg then - pure (resp, false) - else - pure (reqError "internalError" msg, false) - -def handleReleaseOp (req : Request) (session : Session) : M (Response × Bool) := do - let path ← - match req.requirePath with - | .ok path => pure path - | .error err => return (reqError "invalidParams" err, false) - let handle ← - match req.requireHandle with - | .ok handle => pure handle - | .error err => return (reqError "invalidParams" err, false) - let rawHandle ← - match unwrapHandle session handle with - | .ok raw => pure raw - | .error err => return (reqError "contentModified" err, false) - let method ← - match releaseMethod req.backend with - | .ok method => pure method - | .error err => return (reqError "invalidParams" err, false) - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let emitProgress? ← currentFileProgressSink? - let params := Json.mkObj [ - ("textDocument", toJson ({ uri := uri : TextDocumentIdentifier })), - ("handle", rawHandle) - ] - try - let (session, result, fileProgress?) ← - sendRequestJsonTracked session method params - (tracked := some (uri, docState.version)) - (emitProgress? := emitProgress?) - updateSession session - pure (withFileProgress (sessionResult session result) fileProgress?, false) - catch e => - let msg := e.toString - if let some resp := decodeJsonRpcError msg then - pure (resp, false) - else - pure (reqError "internalError" msg, false) - def currentSession? (backend : Backend) : M (Option Session) := do let state ← get match (getBackendState state backend).session? with @@ -1824,7 +1419,10 @@ private def ensureRequestNotCancelled | none => pure () | some cancelRef => if ← cancelRef.get then - throw <| IO.userError "requestCancelled: client requested cancellation" + throwBrokerFailure { + code := .requestCancelled + message := "client requested cancellation" + } private def cancelMatchingPendingRequests (session : Session) @@ -1908,9 +1506,62 @@ private def withCurrentMatchingSession if sameSessionIdentity current session then k current else - throw <| IO.userError "workerExited: broker backend session changed while request was in flight" + throwBrokerFailure { + code := .workerExited + message := "broker backend session changed while request was in flight" + } | none => - throw <| IO.userError "workerExited: broker backend session exited while request was in flight" + throwBrokerFailure { + code := .workerExited + message := "broker backend session exited while request was in flight" + } + +private def sendCurrentSessionRequestDecode [FromJson α] + (server : ServerRuntime) + (session : Session) + (method : String) + (params : Json) : IO α := do + withCurrentMatchingSession server session fun current => do + let (current, payload) ← sendRequestJson current method params + updateSession current + decodeResponseAs payload + +private structure StartedTrackedBarrier where + session : Session + uri : DocumentUri + version : Nat + priorProgress? : Option SyncFileProgress := none + promise : IO.Promise (Except String PendingResult) + +private def startTrackedDiagnosticsBarrierIO + (server : ServerRuntime) + (req : Request) + (path : System.FilePath) + (emitProgress? : Option (SyncFileProgress → IO Unit) := none) + (emitDiagnostic? : Option (StreamDiagnostic → IO Unit) := none) : + IO StartedTrackedBarrier := do + server.withState do + let session ← ensureSession req.backend + let session ← syncFile session path + let uri := sessionUri (← resolvePath session.root path) + let docState ← requireDocState session uri + let params := toJson (WaitForDiagnosticsParams.mk uri docState.version) + let (session, promise) ← + startRequestJsonTrackedDetailed session "textDocument/waitForDiagnostics" params + (clientRequestId? := req.clientRequestId?) + (tracked := some (uri, docState.version)) + (initialProgress? := docState.fileProgress?) + (emitProgress? := emitProgress?) + (fullDiagnostics := req.fullDiagnostics?.getD false) + (emitDiagnostic? := emitDiagnostic?) + updateSession session + pure { + session + uri + version := docState.version + priorProgress? := docState.fileProgress? + promise + } private def handleCloseWithoutSessionIO (req : Request) : IO (Response × Bool) := do let path ← @@ -1973,6 +1624,16 @@ private structure SaveOleanCompleted where payload : Json fileProgress? : Option SyncFileProgress := none +private def saveCompletedResponse + (saved : SaveOleanCompleted) + (closeAfter : Bool) : Response := + let payload := + if closeAfter then + Json.mkObj [("closed", toJson true), ("saved", saved.payload)] + else + saved.payload + withFileProgress (sessionResult saved.session payload) saved.fileProgress? + private def fetchSyncSaveReadinessIO (server : ServerRuntime) (session : Session) @@ -1986,10 +1647,7 @@ private def fetchSyncSaveReadinessIO : RunAt.Internal.SaveReadinessParams }) let readiness : RunAt.Internal.SaveReadinessResult ← - withCurrentMatchingSession server session fun current => do - let (current, result) ← sendRequestJson current method params - updateSession current - decodeResponseAs result + sendCurrentSessionRequestDecode server session method params pure (syncSaveReadinessOfResult readiness) private def fetchDirectImportsIO @@ -2002,38 +1660,12 @@ private def fetchDirectImportsIO : RunAt.Internal.DirectImportsParams }) let result : RunAt.Internal.DirectImportsResult ← - withCurrentMatchingSession server session fun current => do - let (current, payload) ← sendRequestJson current method params - updateSession current - decodeResponseAs payload + sendCurrentSessionRequestDecode server session method params pure { version := result.version imports := result.imports } -private def staleDirectDepHintJson (hint : StaleDirectDepHint) : Json := - Json.mkObj [ - ("module", toJson hint.module), - ("path", toJson hint.path), - ("needsSave", toJson hint.needsSave), - ("lastSyncSeq", toJson hint.lastSyncSeq), - ("lastSaveSeq", toJson hint.lastSaveSeq) - ] - -private def staleSyncErrorData - (targetPath : String) - (hints : Array StaleDirectDepHint) : Json := - let saveHints := hints.filter (·.needsSave) - let recoveryPlan := - (saveHints.map fun hint => s!"lean-beam save \"{hint.path}\"") ++ - #[s!"lean-beam refresh \"{targetPath}\"", "lake build"] - Json.mkObj [ - ("targetPath", toJson targetPath), - ("staleDirectDeps", Json.arr <| hints.map staleDirectDepHintJson), - ("saveDeps", Json.arr <| saveHints.map (fun hint => toJson hint.path)), - ("recoveryPlan", Json.arr <| recoveryPlan.map toJson) - ] - private def staleSyncErrorResponse (message : String) (targetPath : String) @@ -2049,29 +1681,20 @@ private def collectStaleDirectDepHintsIO pure #[] else let importsResult ← fetchDirectImportsIO server session uri - if importsResult.version != version then - pure #[] - else - withCurrentMatchingSession server session fun current => do - let targetLastSyncSeq := - match current.docs.get? uri with - | some docState => docState.lastSyncSeq - | none => 0 - pure <| importsResult.imports.foldl (init := #[]) fun hints moduleName => - match current.moduleHistory.get? moduleName with - | some history => - if history.lastSaveSeq > targetLastSyncSeq then - hints.push { - module := moduleName - path := history.path - needsSave := history.lastSaveSeq < history.lastSyncSeq - lastSyncSeq := history.lastSyncSeq - lastSaveSeq := history.lastSaveSeq - } - else - hints - | none => - hints + withCurrentMatchingSession server session fun current => do + let targetLastSyncSeq := + match current.docs.get? uri with + | some docState => docState.lastSyncSeq + | none => 0 + let history := + current.moduleHistory.foldl (init := {}) fun acc moduleName moduleHistory => + acc.insert moduleName { + path := moduleHistory.path + lastSyncSeq := moduleHistory.lastSyncSeq + lastSaveSeq := moduleHistory.lastSaveSeq + : ModuleHistorySnapshot + } + pure <| collectStaleDirectDepHints importsResult version targetLastSyncSeq history private def saveOleanIO (server : ServerRuntime) @@ -2082,43 +1705,29 @@ private def saveOleanIO (emitDiagnostic? : Option (StreamDiagnostic → IO Unit) := none) : IO SaveOleanCompleted := do ensureRequestNotCancelled cancelRef? - let (session, uri, version, textHash, textTraceHash, textMTime, leanCmd?, priorProgress?, barrierPromise) ← - server.withState do - let session ← ensureSession req.backend - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let params := toJson (WaitForDiagnosticsParams.mk uri docState.version) - let (session, barrierPromise) ← - startRequestJsonTrackedDetailed session "textDocument/waitForDiagnostics" params - (clientRequestId? := req.clientRequestId?) - (tracked := some (uri, docState.version)) - (initialProgress? := docState.fileProgress?) - (emitProgress? := emitProgress?) - (fullDiagnostics := req.fullDiagnostics?.getD false) - (emitDiagnostic? := emitDiagnostic?) - let leanCmd? := (← get).config.leanCmd? - updateSession session - pure (session, uri, docState.version, docState.textHash, docState.textTraceHash, docState.textMTime, - leanCmd?, docState.fileProgress?, barrierPromise) - propagatePendingCancellation session req.clientRequestId? cancelRef? - let barrier ← awaitPendingResult barrierPromise - let barrierProgress? := effectiveSyncBarrierProgress priorProgress? barrier.progress? barrier.diagnostics + let path ← resolvePath ((← server.withState do pure (← get).config.root)) path + let started ← startTrackedDiagnosticsBarrierIO server req path emitProgress? emitDiagnostic? + let (textHash, textTraceHash, textMTime, leanCmd?) ← server.withState do + let docState ← requireDocState started.session started.uri + pure (docState.textHash, docState.textTraceHash, docState.textMTime, (← get).config.leanCmd?) + propagatePendingCancellation started.session req.clientRequestId? cancelRef? + let barrier ← awaitPendingResult started.promise + let barrierProgress? := effectiveSyncBarrierProgress started.priorProgress? barrier.progress? barrier.diagnostics let (_ : WaitForDiagnostics) ← decodeResponseAs barrier.result - mergeFileProgressIfCurrent server session uri barrierProgress? - ensureSyncBarrierComplete uri version barrierProgress? barrier.diagnostics + mergeFileProgressIfCurrent server started.session started.uri barrierProgress? + ensureSyncBarrierComplete started.uri started.version barrierProgress? barrier.diagnostics ensureRequestNotCancelled cancelRef? - let spec ← mkLeanSaveSpec session.root path { hash := textTraceHash, mtime := textMTime } leanCmd? - let method ← IO.ofExcept <| saveArtifactsMethod session.backend + let spec ← mkLeanSaveSpec started.session.root path { hash := textTraceHash, mtime := textMTime } leanCmd? + let method ← IO.ofExcept <| saveArtifactsMethod started.session.backend let params := toJson ({ - textDocument := ({ uri := uri : TextDocumentIdentifier }) + textDocument := ({ uri := started.uri : TextDocumentIdentifier }) oleanFile := spec.oleanPath.toString ileanFile := spec.ileanPath.toString cFile := spec.cPath.toString bcFile? := spec.bcPath?.map (fun bcPath => System.FilePath.toString bcPath) : RunAt.Internal.SaveArtifactsParams }) - let (session, savePromise) ← withCurrentMatchingSession server session fun current => do + let (session, savePromise) ← withCurrentMatchingSession server started.session fun current => do let (current, savePromise) ← startRequestJsonTrackedDetailed current method params (clientRequestId? := req.clientRequestId?) updateSession current @@ -2126,19 +1735,19 @@ private def saveOleanIO propagatePendingCancellation session req.clientRequestId? cancelRef? let savePending ← awaitPendingResult savePromise let saveResult : RunAt.Internal.SaveArtifactsResult ← decodeResponseAs savePending.result - if saveResult.version != version then + if saveResult.version != started.version then throw <| IO.userError - s!"save_olean saved version {saveResult.version}, expected synced version {version}" + s!"save_olean saved version {saveResult.version}, expected synced version {started.version}" if saveResult.textHash != textHash then throw <| IO.userError s!"save_olean saved text hash {saveResult.textHash}, expected synced hash {textHash}" writeLeanSaveTrace spec pure { session - uri - version + uri := started.uri + version := started.version spec - payload := leanSavePayload spec version textTraceHash + payload := leanSavePayload spec started.version textTraceHash fileProgress? := barrierProgress? } @@ -2155,36 +1764,23 @@ private def handleSyncFileOpIO | .ok path => pure path | .error err => return (reqError "invalidParams" err, false) ensureRequestNotCancelled cancelRef? - let (session, uri, version, priorProgress?, promise) ← server.withState do - let session ← ensureSession req.backend - let session ← syncFile session path - let uri := sessionUri (← resolvePath session.root path) - let docState ← requireDocState session uri - let params := toJson (WaitForDiagnosticsParams.mk uri docState.version) - let (session, promise) ← - startRequestJsonTrackedDetailed session "textDocument/waitForDiagnostics" params - (clientRequestId? := req.clientRequestId?) - (tracked := some (uri, docState.version)) - (initialProgress? := docState.fileProgress?) - (emitProgress? := emitProgress?) - (fullDiagnostics := req.fullDiagnostics?.getD false) - (emitDiagnostic? := emitDiagnostic?) - updateSession session - pure (session, uri, docState.version, docState.fileProgress?, promise) - propagatePendingCancellation session req.clientRequestId? cancelRef? - let pending ← awaitPendingResult promise - let fileProgress? := effectiveSyncBarrierProgress priorProgress? pending.progress? pending.diagnostics - mergeFileProgressIfCurrent server session uri fileProgress? + let path ← resolvePath ((← server.withState do pure (← get).config.root)) path + let started ← startTrackedDiagnosticsBarrierIO server req path emitProgress? emitDiagnostic? + propagatePendingCancellation started.session req.clientRequestId? cancelRef? + let pending ← awaitPendingResult started.promise + let fileProgress? := effectiveSyncBarrierProgress started.priorProgress? pending.progress? pending.diagnostics + mergeFileProgressIfCurrent server started.session started.uri fileProgress? if syncBarrierIncomplete? fileProgress? pending.diagnostics then - let hints ← collectStaleDirectDepHintsIO server session uri version - let message := syncBarrierIncompleteMessage uri version fileProgress? - let targetPath := trackedPathLabel session.root uri + let hints ← collectStaleDirectDepHintsIO server started.session started.uri started.version + let message := syncBarrierIncompleteMessage started.uri started.version fileProgress? + let targetPath := trackedPathLabel started.session.root started.uri return (staleSyncErrorResponse message targetPath hints, false) server.withState do - modifyCurrentSessionIfMatching session (fun current => markDocSyncedVersion current uri version) - let saveReadiness ← fetchSyncSaveReadinessIO server session uri + modifyCurrentSessionIfMatching started.session + (fun current => markDocSyncedVersion current started.uri started.version) + let saveReadiness ← fetchSyncSaveReadinessIO server started.session started.uri let payload := toJson ({ - version := version + version := started.version errorCount := syncErrorCount pending.diagnostics warningCount := syncWarningCount pending.diagnostics stateErrorCount := saveReadiness.stateErrorCount @@ -2193,7 +1789,7 @@ private def handleSyncFileOpIO saveReadyReason := saveReadiness.saveReadyReason : SyncFileResult }) - pure (withFileProgress (sessionResult session payload) fileProgress?, false) + pure (withFileProgress (sessionResult started.session payload) fileProgress?, false) catch e => pure (responseForExceptionMessage e.toString, false) @@ -2212,8 +1808,7 @@ private def handleCloseOpIO try let saved ← saveOleanIO server req path cancelRef? emitProgress? emitDiagnostic? finalizeSavedDoc server saved.session saved.uri saved.version saved.spec true - let payload := Json.mkObj [("closed", toJson true), ("saved", saved.payload)] - pure (withFileProgress (sessionResult saved.session payload) saved.fileProgress?, false) + pure (saveCompletedResponse saved true, false) catch e => pure (responseForExceptionMessage e.toString, false) else @@ -2358,7 +1953,7 @@ private def handleSaveOleanOpIO try let saved ← saveOleanIO server req path cancelRef? emitProgress? emitDiagnostic? finalizeSavedDoc server saved.session saved.uri saved.version saved.spec false - pure (withFileProgress (sessionResult saved.session saved.payload) saved.fileProgress?, false) + pure (saveCompletedResponse saved false, false) catch e => pure (responseForExceptionMessage e.toString, false) @@ -2464,7 +2059,7 @@ private def handleRunWithOpIO let rawHandle ← match unwrapHandle session handle with | .ok raw => pure raw - | .error err => throw <| IO.userError s!"contentModified: {err}" + | .error err => throwBrokerFailure { code := .contentModified, message := err } let session ← syncFile session path let uri := sessionUri (← resolvePath session.root path) let docState ← requireDocState session uri @@ -2518,7 +2113,7 @@ private def handleReleaseOpIO let rawHandle ← match unwrapHandle session handle with | .ok raw => pure raw - | .error err => throw <| IO.userError s!"contentModified: {err}" + | .error err => throwBrokerFailure { code := .contentModified, message := err } let session ← syncFile session path let uri := sessionUri (← resolvePath session.root path) let docState ← requireDocState session uri diff --git a/Beam/Broker/SyncSaveSupport.lean b/Beam/Broker/SyncSaveSupport.lean new file mode 100644 index 00000000..4369eb76 --- /dev/null +++ b/Beam/Broker/SyncSaveSupport.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean +import RunAt.Internal.SaveArtifacts +import Beam.Broker.LakeSave +import Beam.Broker.Protocol + +open Lean +open Lean.Lsp + +namespace Beam.Broker + +def isIncompleteBarrierDiagnostic (diagnostic : Diagnostic) : Bool := + diagnostic.message.contains "Failed to build module dependencies." || + diagnostic.message.contains "error: target is out-of-date and needs to be rebuilt" + +def effectiveSyncDiagnosticSeverity (diagnostic : Diagnostic) : + Option DiagnosticSeverity := + if isIncompleteBarrierDiagnostic diagnostic then + some .error + else + diagnostic.severity? + +def filterSyncDiagnostics (fullDiagnostics : Bool) (diagnostics : Array Diagnostic) : + Array Diagnostic := + if fullDiagnostics then + diagnostics + else + diagnostics.filter (fun diagnostic => effectiveSyncDiagnosticSeverity diagnostic == some .error) + +def syncErrorCount (diagnostics : Array Diagnostic) : Nat := + diagnostics.foldl (init := 0) fun count diagnostic => + if effectiveSyncDiagnosticSeverity diagnostic == some .error then + count + 1 + else + count + +def syncWarningCount (diagnostics : Array Diagnostic) : Nat := + diagnostics.foldl (init := 0) fun count diagnostic => + if effectiveSyncDiagnosticSeverity diagnostic == some .warning then + count + 1 + else + count + +structure SyncSaveReadiness where + stateErrorCount : Nat := 0 + stateCommandErrorCount : Nat := 0 + saveReady : Bool := true + saveReadyReason : String := "ok" + deriving Inhabited + +def syncSaveReadinessOfResult + (result : RunAt.Internal.SaveReadinessResult) : SyncSaveReadiness := + { + stateErrorCount := result.diagnosticErrorCount + stateCommandErrorCount := result.commandErrorCount + saveReady := result.saveReady + saveReadyReason := result.saveReadyReason + } + +def diagnosticsIndicateIncompleteBarrier (diagnostics : Array Diagnostic) : Bool := + diagnostics.any isIncompleteBarrierDiagnostic + +def incompleteBarrierProgress (progress? : Option SyncFileProgress := none) : SyncFileProgress := + match progress? with + | some progress => { progress with done := false } + | none => { done := false } + +def syncBarrierIncompleteMessage + (uri : DocumentUri) + (version : Nat) + (progress? : Option SyncFileProgress) : String := + let progress := incompleteBarrierProgress progress? + s!"Lean diagnostics barrier did not complete for {uri} at version {version}; " ++ + s!"fileProgress={toJson progress |>.compress}. An imported target may be stale or broken, " ++ + s!"or the Lean worker may have exited. Run `lake build` or fix the upstream module first." + +def syncBarrierIncomplete? + (progress? : Option SyncFileProgress) + (diagnostics : Array Diagnostic := #[]) : Bool := + if diagnosticsIndicateIncompleteBarrier diagnostics then + true + else + match progress? with + | some progress => !progress.done + | none => false + +def effectiveSyncBarrierProgress + (priorProgress? : Option SyncFileProgress) + (progress? : Option SyncFileProgress) + (diagnostics : Array Diagnostic) : Option SyncFileProgress := + if diagnosticsIndicateIncompleteBarrier diagnostics then + some <| incompleteBarrierProgress (progress?.or priorProgress?) + else + match progress? with + | some progress => + some progress + | none => + some <| priorProgress?.getD {} + +def leanSavePayload (spec : LeanSaveSpec) (version : Nat) (sourceHash : Lake.Hash) : Json := + Json.mkObj <| + [ + ("path", toJson spec.relPath), + ("module", toJson spec.moduleName.toString), + ("version", toJson version), + ("sourceHash", toJson sourceHash), + ("olean", toJson spec.oleanPath.toString), + ("ilean", toJson spec.ileanPath.toString), + ("c", toJson spec.cPath.toString), + ("trace", toJson spec.tracePath.toString) + ] ++ + (match spec.oleanServerPath? with + | some path => [("oleanServer", toJson path.toString)] + | none => []) ++ + (match spec.oleanPrivatePath? with + | some path => [("oleanPrivate", toJson path.toString)] + | none => []) ++ + (match spec.irPath? with + | some path => [("ir", toJson path.toString)] + | none => []) ++ + (match spec.bcPath? with + | some path => [("bc", toJson path.toString)] + | none => []) + +end Beam.Broker diff --git a/RunAt/Lib/Goals.lean b/RunAt/Lib/Goals.lean new file mode 100644 index 00000000..ab78fb55 --- /dev/null +++ b/RunAt/Lib/Goals.lean @@ -0,0 +1,138 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.FileWorker.RequestHandling +import Lean.Server.Requests +import Lean.Meta.PPGoal +import RunAt.ProofSnapshot +import RunAt.Protocol + +open Lean +open Lean.Elab +open Lean.Server +open Lean.Server.RequestM + +namespace RunAt.Lib + +def ppExprString (e : Expr) : MetaM String := do + let e ← if getPPInstantiateMVars (← getOptions) then instantiateMVars e else pure e + return (← Meta.ppExpr e).pretty + +def ppLetValueString? (tactic : Bool) (value : Expr) : MetaM (Option String) := do + if ← Lean.Meta.ppGoal.shouldShowLetValue tactic value then + some <$> ppExprString value + else + pure none + +def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → MetaM α) : MetaM α := do + let mctx ← getMCtx + let some mvarDecl := mctx.findDecl? goal + | throwError "unknown goal {goal.name}" + let lctx := mvarDecl.lctx |>.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl) + +def addGoalHypBundle + (hyps : Array GoalHyp) + (names : Array String) + (type : Expr) + (value? : Option Expr := none) + (tactic : Bool := false) : MetaM (Array GoalHyp) := do + if names.isEmpty then + pure hyps + else + let renderedValue? ← + match value? with + | some value => ppLetValueString? tactic value + | none => pure none + return hyps.push { + names + type := ← ppExprString type + value? := renderedValue? + } + +def goalOfMVarId (mvarId : MVarId) : MetaM Goal := do + let ppAuxDecls := (← getOptions).getBool `pp.auxDecls false + let ppImplDetailHyps := (← getOptions).getBool `pp.implementationDetailHyps false + withGoalCtx mvarId fun lctx mvarDecl => do + let tactic := mvarDecl.kind.isSyntheticOpaque + let pushPending + (names : Array String) + (type? : Option Expr) + (hyps : Array GoalHyp) : MetaM (Array GoalHyp) := + if names.isEmpty then + pure hyps + else + match type? with + | none => pure hyps + | some type => addGoalHypBundle hyps names type (tactic := tactic) + let mut pendingNames : Array String := #[] + let mut prevType? : Option Expr := none + let mut hyps : Array GoalHyp := #[] + for localDecl in lctx do + if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then + continue + else + match localDecl with + | LocalDecl.cdecl _index _fvarId varName type .. + | LocalDecl.ldecl _index _fvarId varName type (nondep := true) .. => + let varName := toString varName + let type ← instantiateMVars type + if prevType? == none || prevType? == some type then + pendingNames := pendingNames.push varName + else + hyps ← pushPending pendingNames prevType? hyps + pendingNames := #[varName] + prevType? := some type + | LocalDecl.ldecl _index _fvarId varName type val (nondep := false) .. => do + let varName := toString varName + hyps ← pushPending pendingNames prevType? hyps + let type ← instantiateMVars type + let val ← instantiateMVars val + hyps ← addGoalHypBundle hyps #[varName] type (value? := some val) (tactic := tactic) + pendingNames := #[] + prevType? := none + hyps ← pushPending pendingNames prevType? hyps + let userName? := match mvarDecl.userName with + | Name.anonymous => none + | name => some <| toString name.eraseMacroScopes + return { + userName? + goalPrefix := Lean.Meta.getGoalPrefix mvarDecl + target := ← ppExprString (← instantiateMVars mvarDecl.type) + hyps + } + +def proofStateOfGoalList (goals : List MVarId) : MetaM ProofState := do + let goals ← goals.mapM goalOfMVarId + return { goals := goals.toArray } + +def proofStateOfGoals (goals : List MVarId) (ctxInfo : ContextInfo) : RequestM ProofState := do + ctxInfo.runMetaM {} <| proofStateOfGoalList goals + +def mkBasisCtxInfo (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : ContextInfo := + if useAfter then + { result.ctxInfo with mctx := result.tacticInfo.mctxAfter } + else + { result.ctxInfo with mctx := result.tacticInfo.mctxBefore } + +def basisGoals (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : List MVarId := + if useAfter then result.tacticInfo.goalsAfter else result.tacticInfo.goalsBefore + +def basisProofState (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : + RequestM ProofState := do + proofStateOfGoals (basisGoals result useAfter) (mkBasisCtxInfo result useAfter) + +def findProofBasisAt (position : Lean.Lsp.Position) : RequestM (RequestTask (Option GoalsAtResult)) := do + let doc ← RequestM.readDoc + let pos := doc.meta.text.lspPosToUtf8Pos position + RequestM.mapTaskCostly (Lean.Server.FileWorker.findGoalsAt? doc pos) fun + | some (result :: _) => return some result + | _ => return none + +def noProofBasisFoundMessage (position : Lean.Lsp.Position) : String := + s!"position {position} is inside the document, but Lean has no proof goals there; try a position inside a tactic or proof body" + +end RunAt.Lib diff --git a/RunAt/Lib/Handles.lean b/RunAt/Lib/Handles.lean new file mode 100644 index 00000000..105160ea --- /dev/null +++ b/RunAt/Lib/Handles.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.Requests +import RunAt.ProofSnapshot +import RunAt.Protocol + +open Lean +open Lean.Server +open Lean.Server.RequestM + +namespace RunAt.Lib + +inductive StoredHandleState where + | command (snapshot : Snapshots.Snapshot) + | proof (snapshot : ProofSnapshot) + +structure StoredHandle where + uri : Lean.Lsp.DocumentUri + version : Nat + state : StoredHandleState + +structure HandleStore where + nextId : Nat := 0 + handles : Std.TreeMap String StoredHandle := {} + staleHandles : Std.TreeSet String compare := {} + deriving Inhabited + +initialize handleStoreRef : IO.Ref HandleStore ← IO.mkRef {} +initialize workerToken : String ← do + let pid ← IO.Process.getPID + let startedAt ← IO.monoNanosNow + pure s!"{pid}-{startedAt}" + +def docHandleKey (uri : Lean.Lsp.DocumentUri) : String := + s!"{hash uri}" + +structure ParsedHandle where + docKey : String + workerKey : String + +def parseHandle? (handle : Handle) : Option ParsedHandle := + match handle.value.splitOn ":" with + | ["runAt", docKey, workerKey, _id] => some { docKey, workerKey } + | _ => none + +def mkHandleString (uri : Lean.Lsp.DocumentUri) (id : Nat) : String := + s!"runAt:{docHandleKey uri}:{workerToken}:{id}" + +def eraseStoredHandle (handle : Handle) : BaseIO Unit := do + handleStoreRef.modify fun store => + { + store with + handles := store.handles.erase handle.value + staleHandles := store.staleHandles.erase handle.value + } + +def markStoredHandleStale (handle : Handle) : BaseIO Unit := do + handleStoreRef.modify fun store => + { + store with + handles := store.handles.erase handle.value + staleHandles := store.staleHandles.insert handle.value + } + +def pruneDocHandles (uri : Lean.Lsp.DocumentUri) (version : Nat) : BaseIO Unit := do + handleStoreRef.modify fun store => + Id.run do + let mut handles := store.handles + let mut staleHandles := store.staleHandles + for (key, stored) in store.handles.toList do + if stored.uri == uri && stored.version != version then + handles := handles.erase key + staleHandles := staleHandles.insert key + return { store with handles, staleHandles } + +def syncHandleStoreForCurrentDoc : RequestM Unit := do + let doc ← RequestM.readDoc + pruneDocHandles doc.meta.uri doc.meta.version + +def isKnownStaleHandle (handle : Handle) : BaseIO Bool := do + return (← handleStoreRef.get).staleHandles.contains handle.value + +def validateHandleForCurrentDoc (handle : Handle) : RequestM Unit := do + let doc ← RequestM.readDoc + let some parsed := parseHandle? handle + | throw <| RequestError.invalidParams s!"malformed handle '{handle.value}'" + if parsed.docKey != docHandleKey doc.meta.uri then + throw <| RequestError.invalidParams s!"handle '{handle.value}' does not belong to this document" + if parsed.workerKey != workerToken then + throw RequestError.fileChanged + syncHandleStoreForCurrentDoc + if ← isKnownStaleHandle handle then + throw RequestError.fileChanged + +def mintHandle (state : StoredHandleState) : RequestM Handle := do + syncHandleStoreForCurrentDoc + let doc ← RequestM.readDoc + handleStoreRef.modifyGet fun store => + let handle : Handle := { value := mkHandleString doc.meta.uri store.nextId } + let stored : StoredHandle := { + uri := doc.meta.uri + version := doc.meta.version + state + } + (handle, { + nextId := store.nextId + 1 + handles := store.handles.insert handle.value stored + staleHandles := store.staleHandles.erase handle.value + }) + +def releaseStoredHandle (handle : Handle) : RequestM Unit := do + validateHandleForCurrentDoc handle + let removed ← handleStoreRef.modifyGet fun store => + let existed := (store.handles.get? handle.value).isSome + (existed, { store with handles := store.handles.erase handle.value }) + if !removed then + throw <| RequestError.invalidParams s!"unknown handle '{handle.value}'" + +def withStoredHandle (handle : Handle) (linear : Bool) + (k : StoredHandle → RequestM α) : RequestM α := do + validateHandleForCurrentDoc handle + let doc ← RequestM.readDoc + let stored ← handleStoreRef.modifyGet fun store => + let stored? := store.handles.get? handle.value + let handles := + if linear then + store.handles.erase handle.value + else + store.handles + (stored?, { store with handles }) + let some stored := stored + | throw <| RequestError.invalidParams s!"unknown handle '{handle.value}'" + if stored.uri != doc.meta.uri then + markStoredHandleStale handle + throw <| RequestError.invalidParams s!"handle '{handle.value}' does not belong to this document" + if stored.version != doc.meta.version then + markStoredHandleStale handle + throw RequestError.fileChanged + k stored + +def maybeAttachHandle + (result : Result) + (storeHandle : Bool) + (state? : Option StoredHandleState) : RequestM Result := do + if !storeHandle || !result.success then + return result + let some state := state? + | return result + return { result with handle? := some (← mintHandle state) } + +end RunAt.Lib diff --git a/RunAt/Lib/Support.lean b/RunAt/Lib/Support.lean new file mode 100644 index 00000000..7726bbf2 --- /dev/null +++ b/RunAt/Lib/Support.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.FileWorker.RequestHandling +import Lean.Server.Requests +import RunAt.Protocol + +open Lean +open Lean.Elab +open Lean.Server +open Lean.Server.RequestM + +namespace RunAt.Lib + +def mkMessage (severity : MessageSeverity) (text : String) : RunAt.Message := + { severity, text } + +def trimOutput (text : String) : String := + text.trimAscii.toString + +def outputMessage? (output : String) : Option RunAt.Message := + let output := trimOutput output + if output.isEmpty then none else some <| mkMessage .information output + +def errorResult (message : String) (proofState? : Option ProofState := none) : Result := + { + success := false + messages := #[mkMessage .error message] + proofState? + } + +def messagesToProtocol (messages : List Lean.Message) : IO (Array RunAt.Message) := do + messages.toArray.mapM fun message => do + return mkMessage message.severity (← message.data.toString) + +def tracesToStrings (traces : List TraceElem) : IO (Array String) := do + traces.toArray.mapM fun trace => do + return (← trace.msg.toString) + +structure ExecutionArtifacts where + messages : Array RunAt.Message + traces : Array String + hasErrors : Bool + +def mkExecutionArtifacts + (output : String) + (messages : List Lean.Message) + (traces : List TraceElem) : RequestM ExecutionArtifacts := do + let mut protocolMessages ← messagesToProtocol messages + if let some outputMessage := outputMessage? output then + protocolMessages := protocolMessages.push outputMessage + let protocolTraces ← tracesToStrings traces + return { + messages := protocolMessages + traces := protocolTraces + hasErrors := protocolMessages.any (fun message => message.severity == .error) + } + +def mkExecutionResult + (error? : Option String) + (artifacts : ExecutionArtifacts) + (proofState? : Option ProofState := none) : Result := + match error? with + | some error => + if artifacts.hasErrors then + { success := false, messages := artifacts.messages, traces := artifacts.traces, proofState? } + else + { + success := false + messages := artifacts.messages.push (mkMessage .error error) + traces := artifacts.traces + proofState? + } + | none => + { + success := !artifacts.hasErrors + messages := artifacts.messages + traces := artifacts.traces + proofState? + } + +def checkRequestCancelled : RequestM Unit := do + let rc ← readThe RequestContext + if ← rc.cancelTk.wasCancelledByEdit then + throw RequestError.fileChanged + if ← rc.cancelTk.wasCancelledByCancelRequest then + throw RequestError.requestCancelled + +def withInnerCancelToken (k : IO.CancelToken → RequestM α) : RequestM α := do + let rc ← readThe RequestContext + let innerCancelTk ← IO.CancelToken.new + let finished ← IO.Promise.new + let finishedTask : ServerTask Bool := + finished.resultD () |>.asServerTask |>.mapCheap (fun _ => false) + let cancelTasks := + rc.cancelTk.cancellationTasks.map (·.mapCheap (fun _ => true)) ++ [finishedTask] + discard <| ServerTask.BaseIO.asTask do + if ← ServerTask.waitAny cancelTasks then + innerCancelTk.set + try + k innerCancelTk + finally + finished.resolve () + +def runCommandElabMWithCancel + (snap : Snapshots.Snapshot) + (doc : DocumentMeta) + (cancelTk? : Option IO.CancelToken) + (c : Elab.Command.CommandElabM α) : EIO Exception α := do + let ctx : Command.Context := { + cmdPos := snap.stx.getPos? |>.getD 0 + fileName := doc.uri + fileMap := doc.text + snap? := none + cancelTk? + } + c.run ctx |>.run' snap.cmdState + +def lineUtf16Length (text : FileMap) (line : Nat) : Nat := + let start := text.lineStart (line + 1) + let stop := + if line + 1 < text.getLastLine then + text.lineStart (line + 2) + else + text.source.rawEndPos + let lineText := String.Pos.Raw.extract text.source start stop + let lineText := + if lineText.endsWith "\n" then + (lineText.dropEnd 1).copy + else + lineText + lineText.utf16Length + +def validatePosition (position : Lean.Lsp.Position) : RequestM Unit := do + let doc ← RequestM.readDoc + let text := doc.meta.text + let eof := text.utf8PosToLspPos text.source.rawEndPos + let lineTooLarge := position.line > eof.line + let maxCharacter := + if position.line > eof.line then + 0 + else + lineUtf16Length text position.line + let charTooLarge := + if position.line > eof.line then + false + else + position.character > maxCharacter + if lineTooLarge then + throw <| RequestError.invalidParams + s!"position {position} is outside the document: line {position.line} is beyond the last line {eof.line}" + if charTooLarge then + throw <| RequestError.invalidParams + s!"position {position} is outside the document: character {position.character} is beyond max character {maxCharacter} for line {position.line}" + +def noSnapshotFoundMessage (position : Lean.Lsp.Position) : String := + s!"position {position} is inside the document, but Lean has no command or tactic snapshot there; try a position inside a command or proof body, not a standalone comment, blank line, or declaration header" + +def withRunAtSnapAtPos + (position : Lean.Lsp.Position) + (f : Snapshots.Snapshot → RequestM α) : RequestM (RequestTask α) := do + let doc ← RequestM.readDoc + let pos := doc.meta.text.lspPosToUtf8Pos position + RequestM.withWaitFindSnap doc (fun snap => snap.endPos >= pos) + (notFoundX := throw <| RequestError.invalidParams (noSnapshotFoundMessage position)) + (x := f) + +end RunAt.Lib diff --git a/RunAt/Plugin.lean b/RunAt/Plugin.lean index a6fc8dc8..c545863e 100644 --- a/RunAt/Plugin.lean +++ b/RunAt/Plugin.lean @@ -6,727 +6,45 @@ Author: Emilio J. Gallego Arias import Lean.Server.FileWorker.RequestHandling import Lean.Server.Requests -import Lean.Meta.PPGoal -import Lean.Compiler.IR -import RunAt.ProofSnapshot import RunAt.Protocol -import RunAt.Internal.SaveArtifacts +import RunAt.Requests.DirectImports +import RunAt.Requests.Goals +import RunAt.Requests.RunAt +import RunAt.Requests.Save open Lean -open Lean.Elab open Lean.Server -open Lean.Server.RequestM namespace RunAt /-- Root plugin module for the standalone `$/lean/runAt` extension. -The current handler executes the provided Lean text against an isolated basis at a position: - -- if a proof state is available, it runs the text as a tactic -- otherwise it runs the text as a command on the enclosing command snapshot +This module keeps request registration thin. Request implementations live in +`RunAt.Requests.*`. -/ def pluginMethod : String := method -private inductive StoredHandleState where - | command (snapshot : Snapshots.Snapshot) - | proof (snapshot : ProofSnapshot) - -private structure StoredHandle where - uri : Lean.Lsp.DocumentUri - version : Nat - state : StoredHandleState - -private structure HandleStore where - nextId : Nat := 0 - handles : Std.TreeMap String StoredHandle := {} - deriving Inhabited - -initialize handleStoreRef : IO.Ref HandleStore ← IO.mkRef {} -initialize workerToken : String ← do - let pid ← IO.Process.getPID - let startedAt ← IO.monoNanosNow - pure s!"{pid}-{startedAt}" - -private def mkMessage (severity : MessageSeverity) (text : String) : RunAt.Message := - { severity, text } - -private def trimOutput (text : String) : String := - text.trimAscii.toString - -private def outputMessage? (output : String) : Option RunAt.Message := - let output := trimOutput output - if output.isEmpty then none else some <| mkMessage .information output - -private def errorResult (message : String) (proofState? : Option ProofState := none) : Result := - { - success := false - messages := #[mkMessage .error message] - proofState? - } - -private def messagesToProtocol (messages : List Lean.Message) : IO (Array RunAt.Message) := do - messages.toArray.mapM fun message => do - return mkMessage message.severity (← message.data.toString) - -private def tracesToStrings (traces : List TraceElem) : IO (Array String) := do - traces.toArray.mapM fun trace => do - return (← trace.msg.toString) - -private def ppExprString (e : Expr) : MetaM String := do - let e ← if getPPInstantiateMVars (← getOptions) then instantiateMVars e else pure e - return (← Meta.ppExpr e).pretty - -private def ppLetValueString? (tactic : Bool) (value : Expr) : MetaM (Option String) := do - if ← Lean.Meta.ppGoal.shouldShowLetValue tactic value then - some <$> ppExprString value - else - pure none - -private def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → MetaM α) : MetaM α := do - let mctx ← getMCtx - let some mvarDecl := mctx.findDecl? goal - | throwError "unknown goal {goal.name}" - let lctx := mvarDecl.lctx |>.sanitizeNames.run' { options := (← getOptions) } - Meta.withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl) - -private def addGoalHypBundle - (hyps : Array GoalHyp) - (names : Array String) - (type : Expr) - (value? : Option Expr := none) - (tactic : Bool := false) : MetaM (Array GoalHyp) := do - if names.isEmpty then - pure hyps - else - let renderedValue? ← - match value? with - | some value => ppLetValueString? tactic value - | none => pure none - return hyps.push { - names - type := ← ppExprString type - value? := renderedValue? - } - -private def goalOfMVarId (mvarId : MVarId) : MetaM Goal := do - let ppAuxDecls := (← getOptions).getBool `pp.auxDecls false - let ppImplDetailHyps := (← getOptions).getBool `pp.implementationDetailHyps false - withGoalCtx mvarId fun lctx mvarDecl => do - let tactic := mvarDecl.kind.isSyntheticOpaque - let pushPending - (names : Array String) - (type? : Option Expr) - (hyps : Array GoalHyp) : MetaM (Array GoalHyp) := - if names.isEmpty then - pure hyps - else - match type? with - | none => pure hyps - | some type => addGoalHypBundle hyps names type (tactic := tactic) - let mut pendingNames : Array String := #[] - let mut prevType? : Option Expr := none - let mut hyps : Array GoalHyp := #[] - for localDecl in lctx do - if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then - continue - else - match localDecl with - | LocalDecl.cdecl _index _fvarId varName type .. - | LocalDecl.ldecl _index _fvarId varName type (nondep := true) .. => - let varName := toString varName - let type ← instantiateMVars type - if prevType? == none || prevType? == some type then - pendingNames := pendingNames.push varName - else - hyps ← pushPending pendingNames prevType? hyps - pendingNames := #[varName] - prevType? := some type - | LocalDecl.ldecl _index _fvarId varName type val (nondep := false) .. => do - let varName := toString varName - hyps ← pushPending pendingNames prevType? hyps - let type ← instantiateMVars type - let val ← instantiateMVars val - hyps ← addGoalHypBundle hyps #[varName] type (value? := some val) (tactic := tactic) - pendingNames := #[] - prevType? := none - hyps ← pushPending pendingNames prevType? hyps - let userName? := match mvarDecl.userName with - | Name.anonymous => none - | name => some <| toString name.eraseMacroScopes - return { - userName? - goalPrefix := Lean.Meta.getGoalPrefix mvarDecl - target := ← ppExprString (← instantiateMVars mvarDecl.type) - hyps - } - -private structure ExecutionArtifacts where - messages : Array RunAt.Message - traces : Array String - hasErrors : Bool - -private def mkExecutionArtifacts - (output : String) - (messages : List Lean.Message) - (traces : List TraceElem) : RequestM ExecutionArtifacts := do - let mut protocolMessages ← messagesToProtocol messages - if let some outputMessage := outputMessage? output then - protocolMessages := protocolMessages.push outputMessage - let protocolTraces ← tracesToStrings traces - return { - messages := protocolMessages - traces := protocolTraces - hasErrors := protocolMessages.any (fun message => message.severity == .error) - } - -private def mkExecutionResult - (error? : Option String) - (artifacts : ExecutionArtifacts) - (proofState? : Option ProofState := none) : Result := - match error? with - | some error => - if artifacts.hasErrors then - { success := false, messages := artifacts.messages, traces := artifacts.traces, proofState? } - else - { - success := false - messages := artifacts.messages.push (mkMessage .error error) - traces := artifacts.traces - proofState? - } - | none => - { - success := !artifacts.hasErrors - messages := artifacts.messages - traces := artifacts.traces - proofState? - } - -private def proofStateOfGoalList (goals : List MVarId) : MetaM ProofState := do - let goals ← goals.mapM goalOfMVarId - return { goals := goals.toArray } - -private def proofStateOfGoals (goals : List MVarId) (ctxInfo : ContextInfo) : RequestM ProofState := do - ctxInfo.runMetaM {} <| proofStateOfGoalList goals - -private def mkBasisCtxInfo (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : ContextInfo := - if useAfter then - { result.ctxInfo with mctx := result.tacticInfo.mctxAfter } - else - { result.ctxInfo with mctx := result.tacticInfo.mctxBefore } - -private def basisGoals (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : List MVarId := - if useAfter then result.tacticInfo.goalsAfter else result.tacticInfo.goalsBefore - -private def basisProofState (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : - RequestM ProofState := do - proofStateOfGoals (basisGoals result useAfter) (mkBasisCtxInfo result useAfter) - -private def checkRequestCancelled : RequestM Unit := do - let rc ← readThe RequestContext - if ← rc.cancelTk.wasCancelledByEdit then - throw RequestError.fileChanged - if ← rc.cancelTk.wasCancelledByCancelRequest then - throw RequestError.requestCancelled - -private def withInnerCancelToken (k : IO.CancelToken → RequestM α) : RequestM α := do - let rc ← readThe RequestContext - let innerCancelTk ← IO.CancelToken.new - let finished ← IO.Promise.new - let finishedTask : ServerTask Bool := - finished.resultD () |>.asServerTask |>.mapCheap (fun _ => false) - let cancelTasks := - rc.cancelTk.cancellationTasks.map (·.mapCheap (fun _ => true)) ++ [finishedTask] - discard <| ServerTask.BaseIO.asTask do - if ← ServerTask.waitAny cancelTasks then - innerCancelTk.set - try - k innerCancelTk - finally - finished.resolve () - -private def runCommandElabMWithCancel - (snap : Snapshots.Snapshot) - (doc : DocumentMeta) - (cancelTk? : Option IO.CancelToken) - (c : Elab.Command.CommandElabM α) : EIO Exception α := do - let ctx : Command.Context := { - cmdPos := snap.stx.getPos? |>.getD 0 - fileName := doc.uri - fileMap := doc.text - snap? := none - cancelTk? - } - c.run ctx |>.run' snap.cmdState - -private def mkFilePath (path : String) : System.FilePath := - System.FilePath.mk path - -private def ensureParentDir (path : System.FilePath) : IO Unit := do - if let some parent := path.parent then - IO.FS.createDirAll parent - -private def writeIlean - (doc : DocumentMeta) - (headerStx : Syntax) - (mainModule : Name) - (trees : Array Elab.InfoTree) - (ileanFile : System.FilePath) : IO Unit := do - let references := Lean.Server.findModuleRefs doc.text trees (localVars := false) - let (moduleRefs, decls) ← references.toLspModuleRefs - let ilean : Lean.Server.Ilean := { - module := mainModule - directImports := Lean.Server.collectImports ⟨headerStx⟩ - references := moduleRefs - decls - } - ensureParentDir ileanFile - IO.FS.writeFile ileanFile (Json.compress <| toJson ilean) - -private def singleLineText (text : String) : String := - let parts := text.splitOn "\n" - let parts := parts.filterMap fun part => - let trimmed := part.trimAscii.toString - if trimmed.isEmpty then none else some trimmed - String.intercalate " " parts - -private def formatErrorDiagnostic (diagnostic : Lean.Widget.InteractiveDiagnostic) : String := - let line := diagnostic.range.start.line + 1 - let character := diagnostic.range.start.character + 1 - s!"{line}:{character}: {singleLineText diagnostic.message.stripTags}" - -private def summarizeErrorItems (items : Array String) (maxItems : Nat := 3) : String := - let limit := Nat.min maxItems items.size - let shown := items.extract 0 limit - let extra := items.size - shown.size - let suffix := if extra > 0 then s!" (and {extra} more)" else "" - s!"{String.intercalate " | " shown.toList}{suffix}" - -private def saveArtifactsErrorMessage - (diagnosticErrors : Array Lean.Widget.InteractiveDiagnostic) - (commandErrors : Array String) : String := - let detailParts : List String := - [ - if !diagnosticErrors.isEmpty then - some s!"diagnostics: {summarizeErrorItems (diagnosticErrors.map formatErrorDiagnostic)}" - else - none, - if !commandErrors.isEmpty then - some s!"commandMessages: {summarizeErrorItems commandErrors}" - else - none - ].filterMap id - if detailParts.isEmpty then - "cannot save artifacts for a document with errors" - else - s!"cannot save artifacts for a document with errors; {String.intercalate "; " detailParts}" - -private def saveReadinessDocumentErrorsReason : String := - "documentErrors" - -private def saveReadinessNotElaboratedReason : String := - "documentDidNotElaborateSuccessfully" - -private def collectSaveReadiness - (doc : Lean.Server.FileWorker.EditableDocument) : - RequestM - (RunAt.Internal.SaveReadinessResult × - Option Elab.Command.State × - Array Lean.Widget.InteractiveDiagnostic × - Array String) := do - let diagnostics ← doc.diagnosticsRef.get - let diagnosticErrors := diagnostics.filter (fun diag => diag.severity? == some .error) - let some cmdState := Lean.Language.Lean.waitForFinalCmdState? doc.initSnap - | return ({ - version := doc.meta.version - diagnosticErrorCount := diagnosticErrors.size - commandErrorCount := 0 - saveReady := false - saveReadyReason := saveReadinessNotElaboratedReason - : RunAt.Internal.SaveReadinessResult - }, none, diagnosticErrors, #[]) - let mut commandErrors : Array String := #[] - for msg in cmdState.messages.toList do - if msg.severity == MessageSeverity.error then - commandErrors := commandErrors.push (singleLineText (← msg.data.toString)) - let commandErrorCount := commandErrors.size - let saveReady := diagnosticErrors.isEmpty && commandErrors.isEmpty - let readiness : RunAt.Internal.SaveReadinessResult := { - version := doc.meta.version - diagnosticErrorCount := diagnosticErrors.size - commandErrorCount := commandErrorCount - saveReady := saveReady - saveReadyReason := if saveReady then "ok" else saveReadinessDocumentErrorsReason - } - pure (readiness, some cmdState, diagnosticErrors, commandErrors) - -private def saveCurrentArtifacts - (doc : Lean.Server.FileWorker.EditableDocument) - (snaps : List Snapshots.Snapshot) - (p : RunAt.Internal.SaveArtifactsParams) : RequestM RunAt.Internal.SaveArtifactsResult := do - checkRequestCancelled - let (readiness, cmdState?, diagnosticErrors, commandErrors) ← collectSaveReadiness doc - unless readiness.saveReady do - throw <| RequestError.invalidParams (saveArtifactsErrorMessage diagnosticErrors commandErrors) - let some cmdState := cmdState? - | throw <| RequestError.invalidParams "document did not elaborate successfully" - let env := cmdState.env - let mainModule := env.mainModule - let oleanFile := mkFilePath p.oleanFile - let ileanFile := mkFilePath p.ileanFile - let cFile := mkFilePath p.cFile - ensureParentDir oleanFile - ensureParentDir cFile - Lean.writeModule env oleanFile - let trees := snaps.toArray.map (·.infoTree) - writeIlean doc.meta doc.initSnap.stx mainModule trees ileanFile - let cOutput ← IO.ofExcept <| Lean.IR.emitC env mainModule - IO.FS.writeFile cFile cOutput - if let some bcFile := p.bcFile?.map mkFilePath then - ensureParentDir bcFile - Lean.IR.emitLLVM env mainModule bcFile.toString - checkRequestCancelled - pure { - written := true - version := doc.meta.version - textHash := hash doc.meta.text.source - } - -private def docHandleKey (uri : Lean.Lsp.DocumentUri) : String := - s!"{hash uri}" - -private structure ParsedHandle where - docKey : String - workerKey : String - -private def parseHandle? (handle : Handle) : Option ParsedHandle := - match handle.value.splitOn ":" with - | ["runAt", docKey, workerKey, _id] => some { docKey, workerKey } - | _ => none - -private def mkHandleString (uri : Lean.Lsp.DocumentUri) (id : Nat) : String := - s!"runAt:{docHandleKey uri}:{workerToken}:{id}" - -private def eraseStoredHandle (handle : Handle) : BaseIO Unit := do - handleStoreRef.modify fun store => - { store with handles := store.handles.erase handle.value } - -private def validateHandleForCurrentDoc (handle : Handle) : RequestM Unit := do - let doc ← RequestM.readDoc - let some parsed := parseHandle? handle - | throw <| RequestError.invalidParams s!"malformed handle '{handle.value}'" - if parsed.docKey != docHandleKey doc.meta.uri then - throw <| RequestError.invalidParams s!"handle '{handle.value}' does not belong to this document" - if parsed.workerKey != workerToken then - throw RequestError.fileChanged - -private def mintHandle (state : StoredHandleState) : RequestM Handle := do - let doc ← RequestM.readDoc - handleStoreRef.modifyGet fun store => - let handle : Handle := { value := mkHandleString doc.meta.uri store.nextId } - let stored : StoredHandle := { - uri := doc.meta.uri - version := doc.meta.version - state - } - (handle, { - nextId := store.nextId + 1 - handles := store.handles.insert handle.value stored - }) - -private def releaseStoredHandle (handle : Handle) : RequestM Unit := do - validateHandleForCurrentDoc handle - let removed ← handleStoreRef.modifyGet fun store => - let existed := (store.handles.get? handle.value).isSome - (existed, { store with handles := store.handles.erase handle.value }) - if !removed then - throw <| RequestError.invalidParams s!"unknown handle '{handle.value}'" - -private def withStoredHandle (handle : Handle) (linear : Bool) - (k : StoredHandle → RequestM α) : RequestM α := do - validateHandleForCurrentDoc handle - let doc ← RequestM.readDoc - let stored ← handleStoreRef.modifyGet fun store => - let stored? := store.handles.get? handle.value - let handles := - if linear then - store.handles.erase handle.value - else - store.handles - (stored?, { store with handles }) - let some stored := stored - | throw <| RequestError.invalidParams s!"unknown handle '{handle.value}'" - if stored.uri != doc.meta.uri then - eraseStoredHandle handle - throw <| RequestError.invalidParams s!"handle '{handle.value}' does not belong to this document" - if stored.version != doc.meta.version then - eraseStoredHandle handle - throw RequestError.fileChanged - k stored - -private def maybeAttachHandle - (result : Result) - (storeHandle : Bool) - (state? : Option StoredHandleState) : RequestM Result := do - if !storeHandle || !result.success then - return result - let some state := state? - | return result - return { result with handle? := some (← mintHandle state) } - -private def lineUtf16Length (text : FileMap) (line : Nat) : Nat := - let start := text.lineStart (line + 1) - let stop := - if line + 1 < text.getLastLine then - text.lineStart (line + 2) - else - text.source.rawEndPos - let lineText := String.Pos.Raw.extract text.source start stop - let lineText := - if lineText.endsWith "\n" then - (lineText.dropEnd 1).copy - else - lineText - lineText.utf16Length - -private def validatePosition (position : Lean.Lsp.Position) : RequestM Unit := do - let doc ← RequestM.readDoc - let text := doc.meta.text - let eof := text.utf8PosToLspPos text.source.rawEndPos - let lineTooLarge := position.line > eof.line - let maxCharacter := - if position.line > eof.line then - 0 - else - lineUtf16Length text position.line - let charTooLarge := - if position.line > eof.line then - false - else - position.character > maxCharacter - if lineTooLarge then - throw <| RequestError.invalidParams - s!"position {position} is outside the document: line {position.line} is beyond the last line {eof.line}" - if charTooLarge then - throw <| RequestError.invalidParams - s!"position {position} is outside the document: character {position.character} is beyond max character {maxCharacter} for line {position.line}" - -private def noSnapshotFoundMessage (position : Lean.Lsp.Position) : String := - s!"position {position} is inside the document, but Lean has no command or tactic snapshot there; try a position inside a command or proof body, not a standalone comment, blank line, or declaration header" - -private def withRunAtSnapAtPos - (position : Lean.Lsp.Position) - (f : Snapshots.Snapshot → RequestM α) : RequestM (RequestTask α) := do - let doc ← RequestM.readDoc - let pos := doc.meta.text.lspPosToUtf8Pos position - RequestM.withWaitFindSnap doc (fun snap => snap.endPos >= pos) - (notFoundX := throw <| RequestError.invalidParams (noSnapshotFoundMessage position)) - (x := f) - -private def findProofBasisAt (position : Lean.Lsp.Position) : RequestM (RequestTask (Option GoalsAtResult)) := do - let doc ← RequestM.readDoc - let pos := doc.meta.text.lspPosToUtf8Pos position - RequestM.mapTaskCostly (Lean.Server.FileWorker.findGoalsAt? doc pos) fun - | some (result :: _) => return some result - | _ => return none - -private def findProofBasis (p : Params) : RequestM (RequestTask (Option GoalsAtResult)) := - findProofBasisAt p.position - -private def noProofBasisFoundMessage (position : Lean.Lsp.Position) : String := - s!"position {position} is inside the document, but Lean has no proof goals there; try a position inside a tactic or proof body" - -private def runCommandText (snap : Snapshots.Snapshot) (text : String) : RequestM (Result × Option StoredHandleState) := do - checkRequestCancelled - withInnerCancelToken fun innerCancelTk => do - let rc ← readThe RequestContext - let stx ← - match Parser.runParserCategory snap.env `command text "" with - | .ok stx => pure stx - | .error err => return (errorResult err, none) - let (output, response) ← IO.FS.withIsolatedStreams do - EIO.toBaseIO do - runCommandElabMWithCancel snap rc.doc.meta (some innerCancelTk) do - let initialMsgCount := (← get).messages.toList.length - let initialTraceCount := (← getTraces).size - let error? ← try - Elab.Command.elabCommandTopLevel stx - pure none - catch ex => - if ex.isInterrupt then - throw ex - pure (some (← ex.toMessageData.toString)) - let state ← get - let messages := state.messages.toList.drop initialMsgCount - let traces := (← getTraces).toList.drop initialTraceCount - return (error?, messages, traces, state) - let (error?, newMessages, newTraces, newState) ← - match response with - | .ok response => pure response - | .error ex => - checkRequestCancelled - throw <| RequestError.internalError (← ex.toMessageData.toString) - let artifacts ← mkExecutionArtifacts output newMessages newTraces - checkRequestCancelled - let result := mkExecutionResult error? artifacts - let nextHandle? := - if result.success then - some <| StoredHandleState.command { snap with cmdState := newState } - else - none - return (result, nextHandle?) - -private def proofStateOfSnapshot (snapshot : ProofSnapshot) : RequestM ProofState := do - let (proofState, _) ← snapshot.runMetaM <| proofStateOfGoalList snapshot.tacticState.goals - return proofState - -private def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) : - RequestM (Result × Option StoredHandleState) := do - checkRequestCancelled - withInnerCancelToken fun innerCancelTk => do - let snapshot := snapshot.withCancelToken (some innerCancelTk) - let stx ← - match Parser.runParserCategory snapshot.coreState.env `tactic text "" with - | .ok stx => pure stx - | .error err => return (errorResult err (some initialProofState), none) - let (output, ((error?, newMessages, newTraces), proofSnapshot')) ← - try - IO.FS.withIsolatedStreams do - let run := snapshot.runTacticM do - let saved ← Elab.Tactic.saveState - let initialMsgCount := (← Core.getMessageLog).toList.length - let initialTraceCount := (← getTraces).size - let error? ← try - Elab.Tactic.evalTactic stx - pure none - catch ex => - if ex.isInterrupt then - throw ex - saved.restore (restoreInfo := true) - pure (some (← ex.toMessageData.toString)) - let messages := (← Core.getMessageLog).toList.drop initialMsgCount - let traces := (← getTraces).toList.drop initialTraceCount - return ((error?, messages, traces)) - run - catch ex => - checkRequestCancelled - throw ex - let artifacts ← mkExecutionArtifacts output newMessages newTraces - checkRequestCancelled - let proofState ← - if error?.isSome then - pure initialProofState - else - proofStateOfSnapshot proofSnapshot' - let result := mkExecutionResult error? artifacts (proofState? := some proofState) - let nextHandle? := - if result.success then - some <| StoredHandleState.proof proofSnapshot' - else - none - return (result, nextHandle?) - -private def runTacticAtBasis (basis : GoalsAtResult) (text : String) : RequestM (Result × Option StoredHandleState) := do - let ctxInfo := mkBasisCtxInfo basis - let initialProofState ← basisProofState basis - let proofSnapshot ← ProofSnapshot.create ctxInfo (basisGoals basis) - runTacticText proofSnapshot initialProofState text - -private def handleGoalsAt (p : GoalsParams) (useAfter : Bool) : RequestM (RequestTask ProofState) := do - validatePosition p.position - checkRequestCancelled - let proofTask ← findProofBasisAt p.position - RequestM.bindRequestTaskCostly proofTask <| fun - | some basis => do - checkRequestCancelled - return RequestTask.pure (← basisProofState basis useAfter) - | none => - throw <| RequestError.invalidParams (noProofBasisFoundMessage p.position) - -private def handleRunAt (p : Params) : RequestM (RequestTask Result) := do - validatePosition p.position - checkRequestCancelled - let proofTask ← findProofBasis p - RequestM.bindRequestTaskCostly proofTask <| fun - | some basis => do - checkRequestCancelled - let (result, state?) ← runTacticAtBasis basis p.text - return RequestTask.pure (← maybeAttachHandle result (p.storeHandle?.getD false) state?) - | none => - withRunAtSnapAtPos p.position fun snap => do - checkRequestCancelled - let (result, state?) ← runCommandText snap p.text - maybeAttachHandle result (p.storeHandle?.getD false) state? - -private def handleRunWith (p : RunWithParams) : RequestM (RequestTask Result) := do - checkRequestCancelled - withStoredHandle p.handle (p.linear?.getD false) fun stored => do - RequestM.asTask do - checkRequestCancelled - let (result, state?) ← - match stored.state with - | .command snapshot => - runCommandText snapshot p.text - | .proof snapshot => - let initialProofState ← proofStateOfSnapshot snapshot - runTacticText snapshot initialProofState p.text - maybeAttachHandle result (p.storeHandle?.getD false) state? - -private def handleReleaseHandle (p : ReleaseHandleParams) : RequestM (RequestTask Json) := do - releaseStoredHandle p.handle - return RequestTask.pure Json.null - -private def handleSaveArtifacts - (p : RunAt.Internal.SaveArtifactsParams) : RequestM (RequestTask RunAt.Internal.SaveArtifactsResult) := do - let doc ← RequestM.readDoc - let t := doc.cmdSnaps.waitAll - RequestM.mapTaskCostly t fun (snaps, _) => do - saveCurrentArtifacts doc snaps p - -private def handleSaveReadiness - (_p : RunAt.Internal.SaveReadinessParams) : RequestM (RequestTask RunAt.Internal.SaveReadinessResult) := do - let doc ← RequestM.readDoc - let t := doc.cmdSnaps.waitAll - RequestM.mapTaskCostly t fun _ => do - let (readiness, _, _, _) ← collectSaveReadiness doc - pure readiness - -private def handleDirectImports - (_p : RunAt.Internal.DirectImportsParams) : RequestM (RequestTask RunAt.Internal.DirectImportsResult) := do - let doc ← RequestM.readDoc - checkRequestCancelled - let inputCtx := Lean.Parser.mkInputContext doc.meta.text.source doc.meta.uri - let (header, _, _) ← Lean.Parser.parseHeader inputCtx - let imports := - (Lean.Server.collectImports header).foldl (init := #[]) fun acc info => - if acc.contains info.module then - acc - else - acc.push info.module - return RequestTask.pure { - version := doc.meta.version - imports - } - initialize - registerLspRequestHandler method Params Result handleRunAt - registerLspRequestHandler goalsAfterMethod GoalsParams ProofState (fun p => handleGoalsAt p true) - registerLspRequestHandler goalsPrevMethod GoalsParams ProofState (fun p => handleGoalsAt p false) - registerLspRequestHandler runWithMethod RunWithParams Result handleRunWith - registerLspRequestHandler releaseHandleMethod ReleaseHandleParams Json handleReleaseHandle + registerLspRequestHandler method Params Result RunAt.Requests.handleRunAt + registerLspRequestHandler goalsAfterMethod GoalsParams ProofState + (fun p => RunAt.Requests.handleGoalsAt p true) + registerLspRequestHandler goalsPrevMethod GoalsParams ProofState + (fun p => RunAt.Requests.handleGoalsAt p false) + registerLspRequestHandler runWithMethod RunWithParams Result RunAt.Requests.handleRunWith + registerLspRequestHandler releaseHandleMethod ReleaseHandleParams Json + RunAt.Requests.handleReleaseHandle registerLspRequestHandler RunAt.Internal.saveArtifactsMethod RunAt.Internal.SaveArtifactsParams RunAt.Internal.SaveArtifactsResult - handleSaveArtifacts + RunAt.Requests.handleSaveArtifacts registerLspRequestHandler RunAt.Internal.saveReadinessMethod RunAt.Internal.SaveReadinessParams RunAt.Internal.SaveReadinessResult - handleSaveReadiness + RunAt.Requests.handleSaveReadiness registerLspRequestHandler RunAt.Internal.directImportsMethod RunAt.Internal.DirectImportsParams RunAt.Internal.DirectImportsResult - handleDirectImports + RunAt.Requests.handleDirectImports end RunAt diff --git a/RunAt/Requests/DirectImports.lean b/RunAt/Requests/DirectImports.lean new file mode 100644 index 00000000..a07dea44 --- /dev/null +++ b/RunAt/Requests/DirectImports.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.Requests +import RunAt.Internal.SaveArtifacts +import RunAt.Lib.Handles +import RunAt.Lib.Support + +open Lean +open Lean.Server +open Lean.Server.RequestM +open RunAt.Lib + +namespace RunAt.Requests + +def handleDirectImports + (_p : RunAt.Internal.DirectImportsParams) : + RequestM (RequestTask RunAt.Internal.DirectImportsResult) := do + syncHandleStoreForCurrentDoc + let doc ← RequestM.readDoc + checkRequestCancelled + let inputCtx := Lean.Parser.mkInputContext doc.meta.text.source doc.meta.uri + let (header, _, _) ← Lean.Parser.parseHeader inputCtx + let imports := + (Lean.Server.collectImports header).foldl (init := #[]) fun acc info => + if acc.contains info.module then + acc + else + acc.push info.module + return RequestTask.pure { + version := doc.meta.version + imports + } + +end RunAt.Requests diff --git a/RunAt/Requests/Goals.lean b/RunAt/Requests/Goals.lean new file mode 100644 index 00000000..6fcae7a6 --- /dev/null +++ b/RunAt/Requests/Goals.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.Requests +import RunAt.Lib.Goals +import RunAt.Lib.Handles +import RunAt.Lib.Support + +open Lean +open Lean.Server +open Lean.Server.RequestM +open RunAt.Lib + +namespace RunAt.Requests + +def handleGoalsAt (p : GoalsParams) (useAfter : Bool) : RequestM (RequestTask ProofState) := do + syncHandleStoreForCurrentDoc + validatePosition p.position + checkRequestCancelled + let proofTask ← findProofBasisAt p.position + RequestM.bindRequestTaskCostly proofTask <| fun + | some basis => do + checkRequestCancelled + return RequestTask.pure (← basisProofState basis useAfter) + | none => + throw <| RequestError.invalidParams (noProofBasisFoundMessage p.position) + +end RunAt.Requests diff --git a/RunAt/Requests/RunAt.lean b/RunAt/Requests/RunAt.lean new file mode 100644 index 00000000..b9c2d168 --- /dev/null +++ b/RunAt/Requests/RunAt.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Server.FileWorker.RequestHandling +import Lean.Server.Requests +import RunAt.Lib.Goals +import RunAt.Lib.Handles +import RunAt.Lib.Support + +open Lean +open Lean.Elab +open Lean.Server +open Lean.Server.RequestM +open RunAt.Lib + +namespace RunAt.Requests + +def runCommandText (snap : Snapshots.Snapshot) (text : String) : + RequestM (Result × Option StoredHandleState) := do + checkRequestCancelled + withInnerCancelToken fun innerCancelTk => do + let rc ← readThe RequestContext + let stx ← + match Parser.runParserCategory snap.env `command text "" with + | .ok stx => pure stx + | .error err => return (errorResult err, none) + let (output, response) ← IO.FS.withIsolatedStreams do + EIO.toBaseIO do + runCommandElabMWithCancel snap rc.doc.meta (some innerCancelTk) do + let initialMsgCount := (← get).messages.toList.length + let initialTraceCount := (← getTraces).size + let error? ← try + Elab.Command.elabCommandTopLevel stx + pure none + catch ex => + if ex.isInterrupt then + throw ex + pure (some (← ex.toMessageData.toString)) + let state ← get + let messages := state.messages.toList.drop initialMsgCount + let traces := (← getTraces).toList.drop initialTraceCount + return (error?, messages, traces, state) + let (error?, newMessages, newTraces, newState) ← + match response with + | .ok response => pure response + | .error ex => + checkRequestCancelled + throw <| RequestError.internalError (← ex.toMessageData.toString) + let artifacts ← mkExecutionArtifacts output newMessages newTraces + checkRequestCancelled + let result := mkExecutionResult error? artifacts + let nextHandle? := + if result.success then + some <| StoredHandleState.command { snap with cmdState := newState } + else + none + return (result, nextHandle?) + +def proofStateOfSnapshot (snapshot : ProofSnapshot) : RequestM ProofState := do + let (proofState, _) ← snapshot.runMetaM <| proofStateOfGoalList snapshot.tacticState.goals + return proofState + +def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) : + RequestM (Result × Option StoredHandleState) := do + checkRequestCancelled + withInnerCancelToken fun innerCancelTk => do + let snapshot := snapshot.withCancelToken (some innerCancelTk) + let stx ← + match Parser.runParserCategory snapshot.coreState.env `tactic text "" with + | .ok stx => pure stx + | .error err => return (errorResult err (some initialProofState), none) + let (output, ((error?, newMessages, newTraces), proofSnapshot')) ← + try + IO.FS.withIsolatedStreams do + let run := snapshot.runTacticM do + let saved ← Elab.Tactic.saveState + let initialMsgCount := (← Core.getMessageLog).toList.length + let initialTraceCount := (← getTraces).size + let error? ← try + Elab.Tactic.evalTactic stx + pure none + catch ex => + if ex.isInterrupt then + throw ex + saved.restore (restoreInfo := true) + pure (some (← ex.toMessageData.toString)) + let messages := (← Core.getMessageLog).toList.drop initialMsgCount + let traces := (← getTraces).toList.drop initialTraceCount + return ((error?, messages, traces)) + run + catch ex => + checkRequestCancelled + throw ex + let artifacts ← mkExecutionArtifacts output newMessages newTraces + checkRequestCancelled + let proofState ← + if error?.isSome then + pure initialProofState + else + proofStateOfSnapshot proofSnapshot' + let result := mkExecutionResult error? artifacts (proofState? := some proofState) + let nextHandle? := + if result.success then + some <| StoredHandleState.proof proofSnapshot' + else + none + return (result, nextHandle?) + +def runTacticAtBasis (basis : GoalsAtResult) (text : String) : + RequestM (Result × Option StoredHandleState) := do + let ctxInfo := mkBasisCtxInfo basis + let initialProofState ← basisProofState basis + let proofSnapshot ← ProofSnapshot.create ctxInfo (basisGoals basis) + runTacticText proofSnapshot initialProofState text + +def handleRunAt (p : Params) : RequestM (RequestTask Result) := do + syncHandleStoreForCurrentDoc + validatePosition p.position + checkRequestCancelled + let proofTask ← findProofBasisAt p.position + RequestM.bindRequestTaskCostly proofTask <| fun + | some basis => do + checkRequestCancelled + let (result, state?) ← runTacticAtBasis basis p.text + return RequestTask.pure (← maybeAttachHandle result (p.storeHandle?.getD false) state?) + | none => + withRunAtSnapAtPos p.position fun snap => do + checkRequestCancelled + let (result, state?) ← runCommandText snap p.text + maybeAttachHandle result (p.storeHandle?.getD false) state? + +def handleRunWith (p : RunWithParams) : RequestM (RequestTask Result) := do + syncHandleStoreForCurrentDoc + checkRequestCancelled + withStoredHandle p.handle (p.linear?.getD false) fun stored => do + RequestM.asTask do + checkRequestCancelled + let (result, state?) ← + match stored.state with + | .command snapshot => + runCommandText snapshot p.text + | .proof snapshot => + let initialProofState ← proofStateOfSnapshot snapshot + runTacticText snapshot initialProofState p.text + maybeAttachHandle result (p.storeHandle?.getD false) state? + +def handleReleaseHandle (p : ReleaseHandleParams) : RequestM (RequestTask Json) := do + syncHandleStoreForCurrentDoc + releaseStoredHandle p.handle + return RequestTask.pure Json.null + +end RunAt.Requests diff --git a/RunAt/Requests/Save.lean b/RunAt/Requests/Save.lean new file mode 100644 index 00000000..aca72b5a --- /dev/null +++ b/RunAt/Requests/Save.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import Lean.Compiler.IR +import Lean.Server.FileWorker.RequestHandling +import Lean.Server.Requests +import RunAt.Internal.SaveArtifacts +import RunAt.Lib.Handles +import RunAt.Lib.Support + +open Lean +open Lean.Elab +open Lean.Server +open Lean.Server.RequestM +open RunAt.Lib + +namespace RunAt.Requests + +def mkFilePath (path : String) : System.FilePath := + System.FilePath.mk path + +def ensureParentDir (path : System.FilePath) : IO Unit := do + if let some parent := path.parent then + IO.FS.createDirAll parent + +def writeIlean + (doc : DocumentMeta) + (headerStx : Syntax) + (mainModule : Name) + (trees : Array Elab.InfoTree) + (ileanFile : System.FilePath) : IO Unit := do + let references := Lean.Server.findModuleRefs doc.text trees (localVars := false) + let (moduleRefs, decls) ← references.toLspModuleRefs + let ilean : Lean.Server.Ilean := { + module := mainModule + directImports := Lean.Server.collectImports ⟨headerStx⟩ + references := moduleRefs + decls + } + ensureParentDir ileanFile + IO.FS.writeFile ileanFile (Json.compress <| toJson ilean) + +def singleLineText (text : String) : String := + let parts := text.splitOn "\n" + let parts := parts.filterMap fun part => + let trimmed := part.trimAscii.toString + if trimmed.isEmpty then none else some trimmed + String.intercalate " " parts + +def formatErrorDiagnostic (diagnostic : Lean.Widget.InteractiveDiagnostic) : String := + let line := diagnostic.range.start.line + 1 + let character := diagnostic.range.start.character + 1 + s!"{line}:{character}: {singleLineText diagnostic.message.stripTags}" + +def summarizeErrorItems (items : Array String) (maxItems : Nat := 3) : String := + let limit := Nat.min maxItems items.size + let shown := items.extract 0 limit + let extra := items.size - shown.size + let suffix := if extra > 0 then s!" (and {extra} more)" else "" + s!"{String.intercalate " | " shown.toList}{suffix}" + +def saveArtifactsErrorMessage + (diagnosticErrors : Array Lean.Widget.InteractiveDiagnostic) + (commandErrors : Array String) : String := + let detailParts : List String := + [ + if !diagnosticErrors.isEmpty then + some s!"diagnostics: {summarizeErrorItems (diagnosticErrors.map formatErrorDiagnostic)}" + else + none, + if !commandErrors.isEmpty then + some s!"commandMessages: {summarizeErrorItems commandErrors}" + else + none + ].filterMap id + if detailParts.isEmpty then + "cannot save artifacts for a document with errors" + else + s!"cannot save artifacts for a document with errors; {String.intercalate "; " detailParts}" + +def saveReadinessDocumentErrorsReason : String := + "documentErrors" + +def saveReadinessNotElaboratedReason : String := + "documentDidNotElaborateSuccessfully" + +def collectSaveReadiness + (doc : Lean.Server.FileWorker.EditableDocument) : + RequestM + (RunAt.Internal.SaveReadinessResult × + Option Elab.Command.State × + Array Lean.Widget.InteractiveDiagnostic × + Array String) := do + let diagnostics ← doc.diagnosticsRef.get + let diagnosticErrors := diagnostics.filter (fun diag => diag.severity? == some .error) + let some cmdState := Lean.Language.Lean.waitForFinalCmdState? doc.initSnap + | return ({ + version := doc.meta.version + diagnosticErrorCount := diagnosticErrors.size + commandErrorCount := 0 + saveReady := false + saveReadyReason := saveReadinessNotElaboratedReason + : RunAt.Internal.SaveReadinessResult + }, none, diagnosticErrors, #[]) + let mut commandErrors : Array String := #[] + for msg in cmdState.messages.toList do + if msg.severity == MessageSeverity.error then + commandErrors := commandErrors.push (singleLineText (← msg.data.toString)) + let commandErrorCount := commandErrors.size + let saveReady := diagnosticErrors.isEmpty && commandErrors.isEmpty + let readiness : RunAt.Internal.SaveReadinessResult := { + version := doc.meta.version + diagnosticErrorCount := diagnosticErrors.size + commandErrorCount := commandErrorCount + saveReady := saveReady + saveReadyReason := if saveReady then "ok" else saveReadinessDocumentErrorsReason + } + pure (readiness, some cmdState, diagnosticErrors, commandErrors) + +def saveCurrentArtifacts + (doc : Lean.Server.FileWorker.EditableDocument) + (snaps : List Snapshots.Snapshot) + (p : RunAt.Internal.SaveArtifactsParams) : RequestM RunAt.Internal.SaveArtifactsResult := do + checkRequestCancelled + let (readiness, cmdState?, diagnosticErrors, commandErrors) ← collectSaveReadiness doc + unless readiness.saveReady do + throw <| RequestError.invalidParams (saveArtifactsErrorMessage diagnosticErrors commandErrors) + let some cmdState := cmdState? + | throw <| RequestError.invalidParams "document did not elaborate successfully" + let env := cmdState.env + let mainModule := env.mainModule + let oleanFile := mkFilePath p.oleanFile + let ileanFile := mkFilePath p.ileanFile + let cFile := mkFilePath p.cFile + ensureParentDir oleanFile + ensureParentDir cFile + Lean.writeModule env oleanFile + let trees := snaps.toArray.map (·.infoTree) + writeIlean doc.meta doc.initSnap.stx mainModule trees ileanFile + let cOutput ← IO.ofExcept <| Lean.IR.emitC env mainModule + IO.FS.writeFile cFile cOutput + if let some bcFile := p.bcFile?.map mkFilePath then + ensureParentDir bcFile + Lean.IR.emitLLVM env mainModule bcFile.toString + checkRequestCancelled + pure { + written := true + version := doc.meta.version + textHash := hash doc.meta.text.source + } + +def handleSaveArtifacts + (p : RunAt.Internal.SaveArtifactsParams) : + RequestM (RequestTask RunAt.Internal.SaveArtifactsResult) := do + syncHandleStoreForCurrentDoc + let doc ← RequestM.readDoc + let t := doc.cmdSnaps.waitAll + RequestM.mapTaskCostly t fun (snaps, _) => do + saveCurrentArtifacts doc snaps p + +def handleSaveReadiness + (_p : RunAt.Internal.SaveReadinessParams) : + RequestM (RequestTask RunAt.Internal.SaveReadinessResult) := do + syncHandleStoreForCurrentDoc + let doc ← RequestM.readDoc + let t := doc.cmdSnaps.waitAll + RequestM.mapTaskCostly t fun _ => do + let (readiness, _, _, _) ← collectSaveReadiness doc + pure readiness + +end RunAt.Requests diff --git a/RunAtTest/Broker/StartupHandshakeTest.lean b/RunAtTest/Broker/StartupHandshakeTest.lean new file mode 100644 index 00000000..ffff477b --- /dev/null +++ b/RunAtTest/Broker/StartupHandshakeTest.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import RunAtTest.Broker.TestUtil +import Lean + +open Lean + +namespace RunAtTest.Broker.StartupHandshakeTest + +open RunAtTest.Broker.TestUtil + +private def writeFakeServer (root : System.FilePath) : IO System.FilePath := do + let script := root / "fake-lean-startup.sh" + let body := String.intercalate "\n" [ + "#!/usr/bin/env bash", + "set -euo pipefail", + "frame() {", + " local body=\"$1\"", + " printf 'Content-Length: %s\\r\\n\\r\\n%s' \"${#body}\" \"$body\"", + "}", + "notif='{\"jsonrpc\":\"2.0\",\"method\":\"window/logMessage\",\"params\":{\"type\":4,\"message\":\"early startup message\"}}'", + "err='{\"jsonrpc\":\"2.0\",\"id\":0,\"error\":{\"code\":-32603,\"message\":\"initialize failed\"}}'", + "frame \"$notif\"", + "frame \"$err\"", + "sleep 5" + ] ++ "\n" + IO.FS.writeFile script body + let out ← IO.Process.output { + cmd := "chmod" + args := #["+x", script.toString] + } + if out.exitCode != 0 then + throw <| IO.userError s!"failed to chmod fake startup server\n{out.stderr}" + pure script + +def main : IO Unit := do + let port : UInt16 := ((← IO.monoNanosNow) % 20000 + 30000).toUInt16 + let endpoint : Beam.Broker.Endpoint := .tcp port + let root ← mkTempProjectRoot "beam-daemon-startup" + IO.FS.createDirAll root + let fakeServer ← writeFakeServer root + let broker ← spawnLeanBrokerWithPlugin endpoint root (← RunAtTest.TestHarness.pluginPath) fakeServer.toString + try + IO.sleep 200 + let resp ← runClient endpoint { op := .ensure, root? := some root.toString } + if resp.ok then + throw <| IO.userError s!"expected startup handshake failure, got success {(toJson resp).compress}" + let some err := resp.error? + | throw <| IO.userError s!"expected startup handshake error payload, got {(toJson resp).compress}" + if err.code != "internalError" then + throw <| IO.userError s!"expected internalError for startup failure, got {(toJson resp).compress}" + unless err.message.contains "initialize failed" do + throw <| IO.userError s!"expected startup failure to mention initialize failure, got {(toJson resp).compress}" + finally + try + broker.kill + catch _ => + pure () + discard <| broker.tryWait + try + IO.FS.removeDirAll root + catch _ => + pure () + +end RunAtTest.Broker.StartupHandshakeTest diff --git a/RunAtTest/Broker/StartupHandshakeTestMain.lean b/RunAtTest/Broker/StartupHandshakeTestMain.lean new file mode 100644 index 00000000..0935a323 --- /dev/null +++ b/RunAtTest/Broker/StartupHandshakeTestMain.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import RunAtTest.Broker.StartupHandshakeTest + +def main := RunAtTest.Broker.StartupHandshakeTest.main diff --git a/RunAtTest/Handle/LifecycleTest.lean b/RunAtTest/Handle/LifecycleTest.lean new file mode 100644 index 00000000..9c7cf3e6 --- /dev/null +++ b/RunAtTest/Handle/LifecycleTest.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import RunAtTest.Scenario + +open Lean +open RunAtTest.Scenario + +namespace RunAtTest.Handle.LifecycleTest + +private def contentModifiedJson : Json := + Json.mkObj [("code", toJson "contentModified")] + +private def expectHandleResultErrorTwice + (doc : DocHandle) + (handle : RunAt.Handle) + (text : String) : ScenarioM Unit := do + let reqA ← runWithHandle doc handle { text } + expectErrorContains reqA contentModifiedJson + let reqB ← runWithHandle doc handle { text } + expectErrorContains reqB contentModifiedJson + +private def checkEditPruning : ScenarioM Unit := do + let cmd ← openDoc "tests/scenario/docs/CommandA.lean" + let mintReq ← sendRunAt cmd { + line := 0 + character := 2 + text := "def tempLifecycle : Nat := 1" + storeHandle := true + } + let mint : RunAt.Result ← awaitResponseAs mintReq + let some handle := mint.handle? + | throw <| IO.userError "expected lifecycle edit handle" + + changeDoc cmd { line := 0, character := 23, insert := " " } + syncDoc cmd + + let freshReq ← sendRunAt cmd { + line := 0 + character := 2 + text := "#check Nat" + storeHandle := true + } + let _fresh : RunAt.Result ← awaitResponseAs freshReq + + expectHandleResultErrorTwice cmd handle "#check tempLifecycle" + closeDoc cmd + +private def checkClosePruning : ScenarioM Unit := do + let branch ← openDoc "tests/scenario/docs/BranchProof.lean" + let mintReq ← sendRunAt branch { + line := 0 + character := 27 + text := "constructor" + storeHandle := true + } + let mint : RunAt.Result ← awaitResponseAs mintReq + let some handle := mint.handle? + | throw <| IO.userError "expected lifecycle close handle" + closeDoc branch + + let branch2 ← openDoc "tests/scenario/docs/BranchProof.lean" + let freshReq ← sendRunAt branch2 { + line := 0 + character := 27 + text := "constructor" + storeHandle := true + } + let _fresh : RunAt.Result ← awaitResponseAs freshReq + + expectHandleResultErrorTwice branch2 handle "exact trivial" + closeDoc branch2 + +def main : IO Unit := RunAtTest.Scenario.run do + checkEditPruning + checkClosePruning + +end RunAtTest.Handle.LifecycleTest + +def main := RunAtTest.Handle.LifecycleTest.main diff --git a/RunAtTest/RequestSurfaceTest.lean b/RunAtTest/RequestSurfaceTest.lean new file mode 100644 index 00000000..0c2e537e --- /dev/null +++ b/RunAtTest/RequestSurfaceTest.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Emilio J. Gallego Arias +-/ + +import RunAtTest.Scenario + +open Lean +open RunAtTest.Scenario + +namespace RunAtTest.RequestSurfaceTest + +private def expectFileExists (label : String) (path : System.FilePath) : ScenarioM Unit := do + unless ← path.pathExists do + throw <| IO.userError s!"{label}: expected file {path} to exist" + +private def requireSingleGoalTarget (label expectedNeedle : String) (state : RunAt.ProofState) : + ScenarioM Unit := do + let some goal := state.goals[0]? + | throw <| IO.userError s!"{label}: expected one goal" + unless goal.target.contains expectedNeedle do + throw <| IO.userError s!"{label}: expected target to contain '{expectedNeedle}', got '{goal.target}'" + +private def mkTmpDir (stem : String) : ScenarioM System.FilePath := do + let dir := System.FilePath.mk s!"/tmp/{stem}-{← IO.monoNanosNow}" + IO.FS.createDirAll dir + pure dir + +private def checkGoalsRequests : ScenarioM Unit := do + let doc ← openDoc "tests/save_olean_project/GoalSmoke.lean" + + let goalsPrevReq ← sendGoals doc { line := 1, character := 2, useAfter := false } + let goalsPrev : RunAt.ProofState ← awaitResponseAs goalsPrevReq + if goalsPrev.goals.size != 1 then + throw <| IO.userError s!"goals prev: expected one goal, got {goalsPrev.goals.size}" + requireSingleGoalTarget "goals prev" "True" goalsPrev + + let goalsAfterReq ← sendGoals doc { line := 1, character := 2, useAfter := true } + let goalsAfter : RunAt.ProofState ← awaitResponseAs goalsAfterReq + if goalsAfter.goals.size != 0 then + throw <| IO.userError s!"goals after: expected solved proof state, got {goalsAfter.goals.size} goals" + + closeDoc doc + +private def checkDirectImportsAndSave : ScenarioM Unit := do + let doc ← openDoc "RunAtTest/Deps/DepA.lean" + + let importsReq ← sendDirectImports doc + let imports : RunAt.Internal.DirectImportsResult ← awaitResponseAs importsReq + if imports.version != 1 then + throw <| IO.userError s!"directImports: expected version 1, got {imports.version}" + if imports.imports != #["RunAtTest.Deps.DepB"] then + throw <| IO.userError s!"directImports: unexpected imports {(toJson imports.imports).compress}" + + let readinessReq ← sendSaveReadiness doc + let readiness : RunAt.Internal.SaveReadinessResult ← awaitResponseAs readinessReq + if !readiness.saveReady then + throw <| IO.userError s!"saveReadiness: expected saveReady = true, got {(toJson readiness).compress}" + if readiness.saveReadyReason != "ok" then + throw <| IO.userError s!"saveReadiness: expected reason = ok, got {readiness.saveReadyReason}" + + let outDir ← mkTmpDir "runat-request-surface" + let saveReq ← sendSaveArtifacts doc { + oleanFile := (outDir / "DepA.olean").toString + ileanFile := (outDir / "DepA.ilean").toString + cFile := (outDir / "DepA.c").toString + } + let saved : RunAt.Internal.SaveArtifactsResult ← awaitResponseAs saveReq + if !saved.written then + throw <| IO.userError "saveArtifacts: expected written = true" + if saved.version != 1 then + throw <| IO.userError s!"saveArtifacts: expected version 1, got {saved.version}" + expectFileExists "saveArtifacts olean" (outDir / "DepA.olean") + expectFileExists "saveArtifacts ilean" (outDir / "DepA.ilean") + expectFileExists "saveArtifacts c" (outDir / "DepA.c") + + changeDoc doc { + line := 8 + character := 18 + delete := "depB" + insert := "\"oops\"" + } + syncDoc doc + + let brokenReq ← sendSaveReadiness doc + let broken : RunAt.Internal.SaveReadinessResult ← awaitResponseAs brokenReq + if broken.saveReady then + throw <| IO.userError s!"broken saveReadiness: expected saveReady = false, got {(toJson broken).compress}" + if broken.saveReadyReason != "documentErrors" then + throw <| IO.userError + s!"broken saveReadiness: expected reason = documentErrors, got {broken.saveReadyReason}" + if broken.diagnosticErrorCount == 0 then + throw <| IO.userError s!"broken saveReadiness: expected diagnosticErrorCount > 0, got {(toJson broken).compress}" + + closeDoc doc + +def main : IO Unit := RunAtTest.Scenario.run do + checkGoalsRequests + checkDirectImportsAndSave + +end RunAtTest.RequestSurfaceTest + +def main := RunAtTest.RequestSurfaceTest.main diff --git a/RunAtTest/Scenario.lean b/RunAtTest/Scenario.lean index b136dc1e..f85df2c5 100644 --- a/RunAtTest/Scenario.lean +++ b/RunAtTest/Scenario.lean @@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias import Lean import Lean.Data.Lsp.Ipc import RunAt.Protocol +import RunAt.Internal.SaveArtifacts import RunAtTest.TestHarness open Lean @@ -38,6 +39,19 @@ structure RunWithSpec where linear : Bool := false deriving Inhabited, Repr, ToJson +structure GoalsSpec where + line : Nat + character : Nat + useAfter : Bool := true + deriving Inhabited, Repr, ToJson + +structure SaveArtifactsSpec where + oleanFile : String + ileanFile : String + cFile : String + bcFile? : Option String := none + deriving Inhabited, Repr, ToJson + instance : FromJson ChangeSpec where fromJson? j := do let line ← j.getObjValAs? Nat "line" @@ -141,6 +155,19 @@ private def sendRequest (method : String) (params : Json) : ScenarioM RequestID modify fun s => { s with nextRequestNo := s.nextRequestNo + 1 } pure id +private def registerRequest (requestID : RequestID) (params : Json) : ScenarioM ReqHandle := do + let s ← get + let req : ReqHandle := { id := s.nextReqHandle } + set { + s with + nextReqHandle := s.nextReqHandle + 1 + requests := s.requests.insert req.id { + requestID + params + } + } + pure req + private partial def waitForRequestOutcome (expectedID : RequestID) : ScenarioM RequestOutcome := do if let some outcome ← takeQueuedResponse? expectedID then return outcome @@ -286,17 +313,7 @@ def sendRunAt (doc : DocHandle) (spec : SendRunAtSpec) : ScenarioM ReqHandle := storeHandle? := if spec.storeHandle then some true else none } let requestID ← sendRequest RunAt.method (toJson params) - let s ← get - let req : ReqHandle := { id := s.nextReqHandle } - set { - s with - nextReqHandle := s.nextReqHandle + 1 - requests := s.requests.insert req.id { - requestID - params := toJson params - } - } - pure req + registerRequest requestID (toJson params) def runWithHandle (doc : DocHandle) (handle : RunAt.Handle) (spec : RunWithSpec) : ScenarioM ReqHandle := do let docState ← getDocState doc @@ -308,17 +325,45 @@ def runWithHandle (doc : DocHandle) (handle : RunAt.Handle) (spec : RunWithSpec) linear? := if spec.linear then some true else none } let requestID ← sendRequest RunAt.runWithMethod (toJson params) - let s ← get - let req : ReqHandle := { id := s.nextReqHandle } - set { - s with - nextReqHandle := s.nextReqHandle + 1 - requests := s.requests.insert req.id { - requestID - params := toJson params - } + registerRequest requestID (toJson params) + +def sendGoals (doc : DocHandle) (spec : GoalsSpec) : ScenarioM ReqHandle := do + let docState ← getDocState doc + let params : RunAt.GoalsParams := { + textDocument := { uri := docState.uri } + position := { line := spec.line, character := spec.character } } - pure req + let method := if spec.useAfter then RunAt.goalsAfterMethod else RunAt.goalsPrevMethod + let requestID ← sendRequest method (toJson params) + registerRequest requestID (toJson params) + +def sendSaveArtifacts (doc : DocHandle) (spec : SaveArtifactsSpec) : ScenarioM ReqHandle := do + let docState ← getDocState doc + let params : RunAt.Internal.SaveArtifactsParams := { + textDocument := { uri := docState.uri } + oleanFile := spec.oleanFile + ileanFile := spec.ileanFile + cFile := spec.cFile + bcFile? := spec.bcFile? + } + let requestID ← sendRequest RunAt.Internal.saveArtifactsMethod (toJson params) + registerRequest requestID (toJson params) + +def sendSaveReadiness (doc : DocHandle) : ScenarioM ReqHandle := do + let docState ← getDocState doc + let params : RunAt.Internal.SaveReadinessParams := { + textDocument := { uri := docState.uri } + } + let requestID ← sendRequest RunAt.Internal.saveReadinessMethod (toJson params) + registerRequest requestID (toJson params) + +def sendDirectImports (doc : DocHandle) : ScenarioM ReqHandle := do + let docState ← getDocState doc + let params : RunAt.Internal.DirectImportsParams := { + textDocument := { uri := docState.uri } + } + let requestID ← sendRequest RunAt.Internal.directImportsMethod (toJson params) + registerRequest requestID (toJson params) def releaseHandle (doc : DocHandle) (handle : RunAt.Handle) : ScenarioM Unit := do let docState ← getDocState doc diff --git a/lakefile.lean b/lakefile.lean index 91966616..97d50134 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -49,12 +49,18 @@ lean_exe "runAt-handle-api-test" where lean_exe "runAt-handle-restart-test" where root := `RunAtTest.Handle.RestartTest +lean_exe "runAt-handle-lifecycle-test" where + root := `RunAtTest.Handle.LifecycleTest + lean_exe "runAt-mcts-proof-search-test" where root := `RunAtTest.Scenario.MctsProofSearchTest lean_exe "runAt-nested-handle-failure-test" where root := `RunAtTest.Handle.NestedHandleFailureTest +lean_exe "runAt-request-surface-test" where + root := `RunAtTest.RequestSurfaceTest + lean_exe "runAt-search-workload-report" where root := `RunAtTest.Scenario.SearchWorkloadReport @@ -78,5 +84,8 @@ lean_exe "beam-daemon-save-stream-test" where lean_exe "beam-daemon-request-stream-test" where root := `RunAtTest.Broker.RequestStreamContractTestMain +lean_exe "beam-daemon-startup-handshake-test" where + root := `RunAtTest.Broker.StartupHandshakeTestMain + lean_exe "beam-daemon-rocq-smoke-test" where root := `RunAtTest.Broker.RocqSmokeTest diff --git a/tests/test-broker-fast.sh b/tests/test-broker-fast.sh index f3e5621b..016f00a6 100644 --- a/tests/test-broker-fast.sh +++ b/tests/test-broker-fast.sh @@ -17,8 +17,10 @@ lake build \ beam-daemon-smoke-test \ beam-daemon-save-stream-test \ beam-daemon-request-stream-test \ + beam-daemon-startup-handshake-test \ > /dev/null .lake/build/bin/beam-daemon-smoke-test > /dev/null .lake/build/bin/beam-daemon-save-stream-test > /dev/null .lake/build/bin/beam-daemon-request-stream-test > /dev/null +.lake/build/bin/beam-daemon-startup-handshake-test > /dev/null diff --git a/tests/test.sh b/tests/test.sh index f0c11e69..099f2100 100644 --- a/tests/test.sh +++ b/tests/test.sh @@ -8,7 +8,7 @@ set -euo pipefail cd "$(dirname "$0")/.." -lake build RunAt:shared runAt-test runAt-scenario-test runAt-scenario-api-test runAt-scenario-stress-test runAt-handle-api-test runAt-handle-restart-test runAt-mcts-proof-search-test runAt-nested-handle-failure-test runAt-search-workload-report > /dev/null +lake build RunAt:shared runAt-test runAt-scenario-test runAt-scenario-api-test runAt-scenario-stress-test runAt-handle-api-test runAt-handle-restart-test runAt-handle-lifecycle-test runAt-mcts-proof-search-test runAt-nested-handle-failure-test runAt-request-surface-test runAt-search-workload-report > /dev/null run_case() { local name="$1" @@ -48,6 +48,11 @@ run_handle_restart_case() { .lake/build/bin/runAt-handle-restart-test > /dev/null } +run_handle_lifecycle_case() { + echo "handle-lifecycle" + .lake/build/bin/runAt-handle-lifecycle-test > /dev/null +} + run_mcts_proof_search_case() { echo "mcts-proof-search" .lake/build/bin/runAt-mcts-proof-search-test > /dev/null @@ -91,6 +96,11 @@ run_nested_handle_failure_case() { .lake/build/bin/runAt-nested-handle-failure-test > /dev/null } +run_request_surface_case() { + echo "request-surface" + .lake/build/bin/runAt-request-surface-test > /dev/null +} + run_case asyncEditAwait run_case commandBasis run_case commandBlankLine @@ -132,6 +142,8 @@ run_scenario_api_case run_scenario_stress_case run_handle_api_case run_handle_restart_case +run_handle_lifecycle_case run_mcts_proof_search_case +run_request_surface_case run_search_workload_case run_nested_handle_failure_case