From e34f35a9940e26775485ac38d60995018261139d Mon Sep 17 00:00:00 2001 From: Beam Install Test Date: Tue, 22 Sep 2026 11:09:24 +0200 Subject: [PATCH 1/2] test source provenance refresh From c21730ee95601e8fab0051812152238cfa6a60c0 Mon Sep 17 00:00:00 2001 From: Beam Install Test Date: Tue, 22 Sep 2026 12:01:55 +0200 Subject: [PATCH 2/2] Add opt-in declaration and whole-proof profiling --- Beam/Broker/Protocol.lean | 12 +- Beam/Broker/Server.lean | 10 +- Beam/Cli/Args.lean | 8 + Beam/Cli/Commands.lean | 10 +- Beam/Cli/LeanOperation.lean | 10 +- Beam/Cli/Usage.lean | 8 +- Beam/LSP/RunAt.lean | 121 +++++++--- Beam/LSP/RunAt/Profile.lean | 154 ++++++++++++ Beam/Lean/Operation.lean | 66 ++++- Beam/Mcp/Projection.lean | 10 +- docs/MCP.md | 11 + docs/SETUP.md | 32 +++ docs/STATUS.md | 32 ++- skills/lean-beam/SKILL.md | 29 +++ tests/lean/BeamTest/Broker/CliDaemonTest.lean | 23 ++ .../BeamTest/Broker/McpProjectionTest.lean | 75 ++++++ tests/lean/BeamTest/Broker/ProtocolTest.lean | 36 +++ .../lean/BeamTest/LSP/RequestSurfaceTest.lean | 2 + .../LSP/Requests/RunAt/ProfileTest.lean | 227 ++++++++++++++++++ tests/lean/BeamTest/LSP/Scenario.lean | 4 + tests/lsp-coverage/cases.json | 24 ++ tests/lsp-coverage/methods.json | 2 + tests/scenario/docs/ProfileProof.lean | 33 +++ tests/test-mcp-stdio.py | 24 ++ 24 files changed, 910 insertions(+), 53 deletions(-) create mode 100644 Beam/LSP/RunAt/Profile.lean create mode 100644 tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean create mode 100644 tests/scenario/docs/ProfileProof.lean diff --git a/Beam/Broker/Protocol.lean b/Beam/Broker/Protocol.lean index 08eaccd7..2d6d07ed 100644 --- a/Beam/Broker/Protocol.lean +++ b/Beam/Broker/Protocol.lean @@ -264,6 +264,7 @@ structure CloseRequest extends RequestFile where structure RunAtRequest extends RequestPosition where text : String storeHandle? : Option Bool := none + profile? : Option Bool := none structure ReferencesRequest extends RequestPosition where includeDeclaration? : Option Bool := none @@ -294,6 +295,7 @@ structure RunWithRequest where text : String storeHandle? : Option Bool := none linear? : Option Bool := none + profile? : Option Bool := none handle : Handle structure ReleaseRequest where @@ -433,7 +435,7 @@ private def Op.requestFields (op : Op) : Array String := #["path", "diagnosticScope", "diagnosticsInResult"] | .close => #["path", "diagnosticScope", "saveArtifacts"] | .runAt => - #["path", "version", "line", "character", "text", "storeHandle"] + #["path", "version", "line", "character", "text", "storeHandle", "profile"] | .hover | .signatureHelp | .definition => #["path", "version", "line", "character"] | .references => @@ -453,7 +455,7 @@ private def Op.requestFields (op : Op) : Array String := "suggest" ] | .runWith => - #["path", "text", "storeHandle", "linear", "handle"] + #["path", "text", "storeHandle", "linear", "profile", "handle"] | .release => #["path", "handle"] | .initWorkspace => #["workspaceMode", "root", "leanCmd", "leanPlugin", "rocqCmd"] @@ -501,7 +503,8 @@ private def RequestPayload.jsonFields : RequestPayload → List (String × Json) | .runAt request => request.toRequestPosition.jsonFields ++ [("text", toJson request.text)] ++ - optionalJsonField "storeHandle" request.storeHandle? + optionalJsonField "storeHandle" request.storeHandle? ++ + optionalJsonField "profile" request.profile? | .hover request | .signatureHelp request | .definition request => request.jsonFields | .references request => @@ -532,6 +535,7 @@ private def RequestPayload.jsonFields : RequestPayload → List (String × Json) [("path", toJson request.path), ("text", toJson request.text)] ++ optionalJsonField "storeHandle" request.storeHandle? ++ optionalJsonField "linear" request.linear? ++ + optionalJsonField "profile" request.profile? ++ [("handle", toJson request.handle)] | .release request => [("path", toJson request.path), ("handle", toJson request.handle)] @@ -681,6 +685,7 @@ instance : FromJson Request where toRequestPosition := target text := ← requiredField j "text" storeHandle? := ← optionalField? (α := Bool) j "storeHandle" + profile? := ← optionalField? (α := Bool) j "profile" } | .hover | .signatureHelp | .definition => do let target ← decodeRequestPosition j backend @@ -737,6 +742,7 @@ instance : FromJson Request where text := ← requiredField j "text" storeHandle? := ← optionalField? (α := Bool) j "storeHandle" linear? := ← optionalField? (α := Bool) j "linear" + profile? := ← optionalField? (α := Bool) j "profile" handle } | .release => do diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean index 356111d9..dd138868 100644 --- a/Beam/Broker/Server.lean +++ b/Beam/Broker/Server.lean @@ -2212,10 +2212,11 @@ private def handleRunAtOp [ ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier })) , ("position", toJson ({ line := request.line, character := request.character : Lsp.Position })) , ("text", toJson request.text) - ] ++ - match request.storeHandle? with + ] ++ (match request.storeHandle? with | some b => [("storeHandle", toJson b)] - | none => []) + | none => []) ++ (match request.profile? with + | some b => [("profile", toJson b)] + | none => [])) trackedDocumentVersion (expectedVersion? := some request.version) (clientRequestId? := req.clientRequestId?) @@ -2516,6 +2517,9 @@ private def handleRunWithOp | none => []) ++ (match request.linear? with | some b => [("linear", toJson b)] + | none => []) ++ + (match request.profile? with + | some b => [("profile", toJson b)] | none => [])) trackedDocumentVersion (clientRequestId? := req.clientRequestId?) diff --git a/Beam/Cli/Args.lean b/Beam/Cli/Args.lean index 0023b9f8..2ece3caa 100644 --- a/Beam/Cli/Args.lean +++ b/Beam/Cli/Args.lean @@ -65,6 +65,14 @@ def parseTextArg (cmdHead : String) (args : List String) : IO ParsedTextArg := d | throw <| IO.userError (textArgUsage cmdHead) pure { text, source := "argv" } +/-- Consume the optional profiling selector before a text input selector. -/ +def parseProfileArg (args : List String) : IO (Bool × List String) := do + match args with + | "--profile" :: "--profile" :: _ => + throw <| IO.userError "duplicate --profile" + | "--profile" :: rest => pure (true, rest) + | _ => pure (false, args) + def parseJsonText (label text : String) : IO Json := do match Json.parse text with | .ok json => pure json diff --git a/Beam/Cli/Commands.lean b/Beam/Cli/Commands.lean index e6496d4a..5780926e 100644 --- a/Beam/Cli/Commands.lean +++ b/Beam/Cli/Commands.lean @@ -96,11 +96,13 @@ private def runLeanRunAt let version ← parseNatArg "version" versionText let line ← parseNatArg "line" lineText let character ← parseNatArg "character" characterText + let (profile, textArgs) ← parseProfileArg textArgs let parsedText ← parseTextArg s!"{action} " textArgs let root ← projectRoot opts .lean withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => do let req ← withEnvClientRequestId <| - leanRunAtRequest path version line character parsedText.text (storeHandle := storeHandle) + leanRunAtRequest path version line character parsedText.text + (storeHandle := storeHandle) (profile := profile) maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text callBrokerWithProgress root client req (leanRunAtWaitSpec action path line character) @@ -114,16 +116,18 @@ private def runLeanRunWith | [] => [] | "--handle-file" :: _ :: rest => rest | _ :: rest => rest - if handleArgReadsStdin args && textArgReadsStdin textArgs then + let (_, profileFreeTextArgs) ← parseProfileArg textArgs + if handleArgReadsStdin args && textArgReadsStdin profileFreeTextArgs then throw <| IO.userError <| String.intercalate "\n" [ textArgUsage s!"{action} >", "cannot read both handle json and continuation text from stdin; pass the handle inline, use --handle-file, or use --text-file for the text" ] let (handle, textArgs) ← parseHandleInput s!"{action} " args + let (profile, textArgs) ← parseProfileArg textArgs let parsedText ← parseTextArg s!"{action} >" textArgs let root ← projectRoot opts .lean let req ← withEnvClientRequestId <| - leanRunWithRequest path handle parsedText.text (linear := linear) + leanRunWithRequest path handle parsedText.text (linear := linear) (profile := profile) maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => callBrokerWithProgress root client req (leanRunWithWaitSpec path (linear := linear)) diff --git a/Beam/Cli/LeanOperation.lean b/Beam/Cli/LeanOperation.lean index fe072c3c..939e02db 100644 --- a/Beam/Cli/LeanOperation.lean +++ b/Beam/Cli/LeanOperation.lean @@ -17,16 +17,18 @@ def leanRunAtRequest (version : Nat) (line character : Nat) (text : String) - (storeHandle : Bool := false) : Request := - ({ path, version, line, character, text } : Beam.Lean.RunAtInput).toBrokerRequest + (storeHandle : Bool := false) + (profile : Bool := false) : Request := + ({ path, version, line, character, text, profile? := if profile then some true else none } : Beam.Lean.RunAtInput).toBrokerRequest (storeHandle := storeHandle) def leanRunWithRequest (path : String) (handle : Handle) (text : String) - (linear : Bool := false) : Request := - ({ path, handle, text } : Beam.Lean.RunWithInput).toBrokerRequest + (linear : Bool := false) + (profile : Bool := false) : Request := + ({ path, handle, text, profile? := if profile then some true else none } : Beam.Lean.RunWithInput).toBrokerRequest (linear := linear) def leanReleaseRequest (path : String) (handle : Handle) : Request := diff --git a/Beam/Cli/Usage.lean b/Beam/Cli/Usage.lean index d0641c13..6bd1d677 100644 --- a/Beam/Cli/Usage.lean +++ b/Beam/Cli/Usage.lean @@ -14,8 +14,8 @@ def usage : String := " lean-beam --version", " lean-beam version", " lean-beam [--root PATH] [--session-dir DIR] serve [lean|rocq]", - " lean-beam [--root PATH] run-at (--stdin | --text-file | -- | )", - " lean-beam [--root PATH] run-at-handle (--stdin | --text-file | -- | )", + " lean-beam [--root PATH] run-at [--profile] (--stdin | --text-file | -- | )", + " lean-beam [--root PATH] run-at-handle [--profile] (--stdin | --text-file | -- | )", " lean-beam [--root PATH] hover ", " lean-beam [--root PATH] signature-help ", " lean-beam [--root PATH] definition ", @@ -24,8 +24,8 @@ def usage : String := " lean-beam [--root PATH] workspace-symbols ", " lean-beam [--root PATH] goals before|after ", " lean-beam [--root PATH] todo [--kind ...] [--suggest none|basic]", - " lean-beam [--root PATH] run-with > (--stdin | --text-file | -- | )", - " lean-beam [--root PATH] run-with-linear > (--stdin | --text-file | -- | )", + " lean-beam [--root PATH] run-with > [--profile] (--stdin | --text-file | -- | )", + " lean-beam [--root PATH] run-with-linear > [--profile] (--stdin | --text-file | -- | )", " lean-beam [--root PATH] release >", " lean-beam [--root PATH] update ", " lean-beam [--root PATH] sync [+all-diagnostics]", diff --git a/Beam/LSP/RunAt.lean b/Beam/LSP/RunAt.lean index b7ac96fd..d62b29f5 100644 --- a/Beam/LSP/RunAt.lean +++ b/Beam/LSP/RunAt.lean @@ -9,6 +9,7 @@ import Lean.Server.Requests import Beam.LSP.Lib.Goal import Beam.LSP.Lib.Request import Beam.LSP.RunAt.Handles +import Beam.LSP.RunAt.Profile open Lean open Lean.Elab @@ -61,6 +62,7 @@ structure Params where position : Lean.Lsp.Position text : String storeHandle? : Option Bool := none + profile? : Option Bool := none deriving FromJson, ToJson -- Lean v4.28 compatibility shim: `Lean.Lsp.FileSource.fileSource` returns `FileIdent` there, but @@ -76,6 +78,7 @@ structure RunWithParams where text : String storeHandle? : Option Bool := none linear? : Option Bool := none + profile? : Option Bool := none deriving FromJson, ToJson instance : Lean.Lsp.FileSource RunWithParams where @@ -113,6 +116,7 @@ Current frozen response semantics: - proof goals are structured into target, hypotheses, and optional case name - solved proof states use `proofState.goals = #[]` - `traces` stays as a plain array; empty traces are represented as `#[]` +- opt-in `profile` reports bounded timing metadata and replaces rendered `traces` with `#[]` - positions outside the document produce transport `invalidParams` - in-document positions with no usable command/proof snapshot may also produce transport `invalidParams` - in-document whitespace/comment positions may still resolve to a nearby execution basis @@ -128,6 +132,7 @@ structure Result where traces : Array String := #[] handle? : Option Handle := none proofState? : Option ProofState := none + profile? : Option Profile.Result := none deriving FromJson, ToJson def mkMessage (severity : MessageSeverity) (text : String) : Message := @@ -272,15 +277,29 @@ private def oneCommandOnlyResult (err : String) : Result := errorResult s!"{runAtSupportsOneCommandOnlyCode}: command-mode runAt accepts exactly one Lean command, not a top-level command sequence. Use a stored handle continuation for explicit speculative sequencing, or write the sequence to the file and sync it. Original parse error: {err}" +-- Parse the same sequence accepted after `by`, retaining the submitted source positions. +-- A whole proof can contain several tactics and nested, indented goal blocks. +private def parseTacticText (env : Environment) (text : String) : Except String Syntax := + let p := Parser.andthenFn Parser.whitespace Parser.Tactic.tacticSeq.fn + let ictx := Parser.mkInputContext text "" + let s := p.run ictx { env, options := {} } (Parser.getTokenTable env) (Parser.mkParserState text) + if !s.allErrors.isEmpty then + .error (s.toErrorMsg ictx) + else if ictx.atEnd s.pos then + .ok s.stxStack.back + else + .error ((s.mkError "end of input").toErrorMsg ictx) + -- With `Elab.async`, `elabCommandTopLevel` may return before nested work has produced its -- diagnostics. Top-level theorem commands use this path for proof-body elaboration, so these -- snapshot messages are part of the command-mode `runAt` result even though unrelated full-file -- diagnostics remain out of scope. private def collectSnapshotTaskArtifacts - (tasks : Array (Language.SnapshotTask Language.SnapshotTree)) : - BaseIO (List Lean.Message × List TraceElem) := do + (tasks : Array (Language.SnapshotTask Language.SnapshotTree)) + (profile : Bool := false) : + BaseIO (List Lean.Message × List TraceElem × Array TraceState) := do if tasks.isEmpty then - return ([], []) + return ([], [], #[]) let tree := Language.SnapshotTree.mk { diagnostics := .empty } tasks let waitTask ← tree.waitAll -- Force every child snapshot before reading the tree; otherwise theorem proof failures can be @@ -289,11 +308,12 @@ private def collectSnapshotTaskArtifacts let snapshots := tree.getAll let messages := snapshots.foldl (init := []) fun acc snapshot => acc ++ snapshot.diagnostics.msgLog.toList - let traces := snapshots.foldl (init := []) fun acc snapshot => + let traces := if profile then [] else snapshots.foldl (init := []) fun acc snapshot => acc ++ snapshot.traces.traces.toList - return (messages, traces) + let profileStates := if profile then snapshots.map (·.traces) else #[] + return (messages, traces, profileStates) -def runCommandText (snap : Snapshots.Snapshot) (text : String) : +def runCommandText (snap : Snapshots.Snapshot) (text : String) (profile : Bool := false) : RequestM (Result × Option StoredHandleState) := do checkRequestCancelled withInnerCancelToken fun innerCancelTk => do @@ -303,12 +323,19 @@ def runCommandText (snap : Snapshots.Snapshot) (text : String) : | .ok stx => pure stx | .extraInput err => return (oneCommandOnlyResult err, none) | .error err => return (errorResult err, none) + let startNs ← if profile then IO.monoNanosNow else pure 0 let (output, response) ← IO.FS.withIsolatedStreams do EIO.toBaseIO do runCommandElabMWithCancel snap rc.doc.meta (some innerCancelTk) do -- The incoming snapshot can carry already-accounted-for async work from the saved file. -- A speculative command result should include only tasks spawned by this command. modify fun state => { state with snapshotTasks := #[] } + if profile then + let tid ← IO.getTID + modify fun state => { state with + traceState := { tid } + scopes := state.scopes.map fun scope => { scope with opts := Profile.options scope.opts } + } let initialMsgCount := (← get).messages.toList.length let initialTraceCount := (← getTraces).size let error? ← try @@ -320,25 +347,34 @@ def runCommandText (snap : Snapshots.Snapshot) (text : String) : pure (some (← ex.toMessageData.toString)) let state ← get let messages := state.messages.toList.drop initialMsgCount - let traces := (← getTraces).toList.drop initialTraceCount - let (snapshotMessages, snapshotTraces) ← - collectSnapshotTaskArtifacts state.snapshotTasks + let traces ← if profile then pure [] else pure <| (← getTraces).toList.drop initialTraceCount + let (snapshotMessages, snapshotTraces, profileStates) ← + collectSnapshotTaskArtifacts state.snapshotTasks profile + let profile? ← if profile then do + let stopNs ← IO.monoNanosNow + pure <| some <| Profile.collect startNs stopNs (#[state.traceState] ++ profileStates) text + else pure none + let state := if profile then { state with + scopes := Profile.restoreScopes snap.cmdState.scopes state.scopes + traceState := snap.cmdState.traceState + } else state return ( error?, messages ++ snapshotMessages, traces ++ snapshotTraces, -- Completed snapshot tasks have been folded into the result. Do not leak them into a -- stored command handle, where a later `runWith` would report them again. - { state with snapshotTasks := #[] }) - let (error?, newMessages, newTraces, newState) ← + { state with snapshotTasks := #[] }, profile?) + let (error?, newMessages, newTraces, newState, profile?) ← match response with | .ok response => pure response | .error ex => checkRequestCancelled throw <| RequestError.internalError (← ex.toMessageData.toString) - let artifacts ← mkExecutionArtifacts output newMessages newTraces + -- Profiling returns structured metadata instead of formatting the profiler's trace tree. + let artifacts ← mkExecutionArtifacts output newMessages (if profile then [] else newTraces) checkRequestCancelled - let result := mkExecutionResult error? artifacts + let result := { mkExecutionResult error? artifacts with profile? } let nextHandle? := if result.success then some <| StoredHandleState.command { snap with cmdState := newState } @@ -382,12 +418,15 @@ private structure TacticExecutionOutcome where error? : Option String messages : List Lean.Message traces : List TraceElem + /-- Preserve failed execution evidence before restoring the proof state. -/ + profileState? : Option Core.State := none private def collectNewTacticArtifacts (initialMsgCount : Nat) - (initialTraceCount : Nat) : Elab.Tactic.TacticM (List Lean.Message × List TraceElem) := do + (initialTraceCount : Nat) + (profile : Bool := false) : Elab.Tactic.TacticM (List Lean.Message × List TraceElem) := do let messages := (← Core.getMessageLog).toList.drop initialMsgCount - let traces := (← getTraces).toList.drop initialTraceCount + let traces ← if profile then pure [] else pure <| (← getTraces).toList.drop initialTraceCount pure (messages, traces) private def classifyTacticException @@ -408,15 +447,25 @@ private def classifyTacticException | _ => pure (some (← ex.toMessageData.toString)) -def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) : +def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) + (profile : Bool := false) : 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 + match parseTacticText snapshot.coreState.env text with | .ok stx => pure stx | .error err => return (errorResult err (some initialProofState), none) + let originalSnapshot := snapshot + let snapshot ← if profile then do + let tid ← IO.getTID + pure { snapshot with + coreContext := { snapshot.coreContext with options := Profile.options snapshot.coreContext.options } + coreState := { snapshot.coreState with traceState := { tid }, snapshotTasks := #[] } + } + else pure snapshot + let startNs ← if profile then IO.monoNanosNow else pure 0 let (output, (outcome, proofSnapshot')) ← try IO.FS.withIsolatedStreams do @@ -426,30 +475,46 @@ def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (t let initialTraceCount := (← getTraces).size try Elab.Tactic.evalTactic stx - let (messages, traces) ← collectNewTacticArtifacts initialMsgCount initialTraceCount + let (messages, traces) ← collectNewTacticArtifacts initialMsgCount initialTraceCount profile return { disposition := .keepAdvanced, error? := none, messages, traces } catch ex => - let (messages, traces) ← collectNewTacticArtifacts initialMsgCount initialTraceCount + let (messages, traces) ← collectNewTacticArtifacts initialMsgCount initialTraceCount profile let error? ← classifyTacticException ex messages + let profileState? ← if profile then some <$> getThe Core.State else pure none saved.restore (restoreInfo := true) - return { disposition := .restoreInitial, error?, messages, traces } + return { disposition := .restoreInitial, error?, messages, traces, profileState? } run catch ex => checkRequestCancelled throw ex - let artifacts ← mkExecutionArtifacts output outcome.messages outcome.traces + let (profileMessages, profile?, proofSnapshot') ← if profile then do + let state := outcome.profileState?.getD proofSnapshot'.coreState + let (messages, _, states) ← collectSnapshotTaskArtifacts state.snapshotTasks true + let stopNs ← IO.monoNanosNow + let result := Profile.collect startNs stopNs (#[state.traceState] ++ states) text + let restored := { proofSnapshot' with + coreContext := originalSnapshot.coreContext + coreState := { proofSnapshot'.coreState with + traceState := originalSnapshot.coreState.traceState + snapshotTasks := originalSnapshot.coreState.snapshotTasks + } + } + pure (messages, some result, restored) + else pure ([], none, proofSnapshot') + let artifacts ← mkExecutionArtifacts output (outcome.messages ++ profileMessages) + (if profile then [] else outcome.traces) checkRequestCancelled let proofState ← outcome.disposition.proofState initialProofState proofSnapshot' - let result := mkExecutionResult outcome.error? artifacts (proofState? := some proofState) + let result := { mkExecutionResult outcome.error? artifacts (proofState? := some proofState) with profile? } let nextHandle? := outcome.disposition.nextHandleState? result proofSnapshot' return (result, nextHandle?) -def runTacticAtBasis (basis : GoalsAtResult) (text : String) : +def runTacticAtBasis (basis : GoalsAtResult) (text : String) (profile : Bool := false) : RequestM (Result × Option StoredHandleState) := do let ctxInfo := mkBasisCtxInfo basis let initialProofState ← basisProofState basis let proofSnapshot ← ProofSnapshot.create ctxInfo (basisGoals basis) - runTacticText proofSnapshot initialProofState text + runTacticText proofSnapshot initialProofState text profile def handleRunAt (p : Params) : RequestM (RequestTask Result) := do requireDocumentVersion p.textDocument @@ -460,12 +525,12 @@ def handleRunAt (p : Params) : RequestM (RequestTask Result) := do RequestM.bindRequestTaskCostly proofTask <| fun | some basis => do checkRequestCancelled - let (result, state?) ← runTacticAtBasis basis p.text + let (result, state?) ← runTacticAtBasis basis p.text (p.profile?.getD false) 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 + let (result, state?) ← runCommandText snap p.text (p.profile?.getD false) maybeAttachHandle result (p.storeHandle?.getD false) state? def handleRunWith (p : RunWithParams) : RequestM (RequestTask Result) := do @@ -477,10 +542,10 @@ def handleRunWith (p : RunWithParams) : RequestM (RequestTask Result) := do let (result, state?) ← match stored.state with | .command snapshot => - runCommandText snapshot p.text + runCommandText snapshot p.text (p.profile?.getD false) | .proof snapshot => let initialProofState ← proofStateOfSnapshot snapshot - runTacticText snapshot initialProofState p.text + runTacticText snapshot initialProofState p.text (p.profile?.getD false) maybeAttachHandle result (p.storeHandle?.getD false) state? def handleReleaseHandle (p : ReleaseHandleParams) : RequestM (RequestTask Json) := do diff --git a/Beam/LSP/RunAt/Profile.lean b/Beam/LSP/RunAt/Profile.lean new file mode 100644 index 00000000..a7cf21cb --- /dev/null +++ b/Beam/LSP/RunAt/Profile.lean @@ -0,0 +1,154 @@ +/- +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 + +open Lean + +namespace Beam.LSP.RunAt.Profile + +/-- A timed, instrumented Lean scope. Parent indices refer to earlier entries in `spans`. +Ranges, when available, are relative to the submitted text, never the tracked document. -/ +structure Span where + parent? : Option Nat := none + thread : UInt64 + category : String + tag : String + startMs : Float + durationMs : Float + range? : Option Lean.Lsp.Range := none + deriving FromJson, ToJson, Inhabited + +/-- Wall-clock evidence from one speculative execution in its already-loaded environment. +Span durations overlap and must not be summed to obtain `elapsedMs`. -/ +structure Result where + elapsedMs : Float + thresholdMs : Nat := 1 + spans : Array Span := #[] + truncated : Bool := false + deriving FromJson, ToJson + +def thresholdMs : Nat := 1 +def maxSpans : Nat := 1024 +def maxVisited : Nat := 8192 +def maxDepth : Nat := 128 + +/-- Retain structured trace data in memory. An explicitly present empty export path is Lean's +retention switch; Beam never calls the frontend's profile file writer or HTTP server. -/ +def options (opts : Options) : Options := + opts.setBool `trace.profiler true + |>.set `trace.profiler.threshold thresholdMs + |>.setBool `trace.profiler.useHeartbeats false + |>.set `trace.profiler.output ("") + |>.setBool `trace.profiler.serve false + +private def restoreOption [KVMap.Value α] (key : Name) (before after : Options) : Options := + match before.get? (α := α) key with + | some value => after.set key value + | none => after.erase key + +/-- Remove only instrumentation options; retain unrelated options changed by the submitted command. -/ +def restoreOptions (before after : Options) : Options := + restoreOption (α := Bool) `trace.profiler before after + |> restoreOption (α := Nat) `trace.profiler.threshold before + |> restoreOption (α := Bool) `trace.profiler.useHeartbeats before + |> restoreOption (α := String) `trace.profiler.output before + |> restoreOption (α := Bool) `trace.profiler.serve before + +/-- Align scopes from the outermost scope, allowing the command to open or close a namespace. +New scopes inherit the original active scope's profiling options. -/ +def restoreScopes (before after : List Elab.Command.Scope) : List Elab.Command.Scope := Id.run do + let originals := before.reverse.toArray + let fallback := before.head?.map (·.opts) |>.getD {} + let restored := after.reverse.toArray.mapIdx fun i scope => + { scope with opts := restoreOptions ((originals[i]?).map (·.opts) |>.getD fallback) scope.opts } + return restored.toList.reverse + +private structure Projection where + spans : Array Span := #[] + visited : Nat := 0 + truncated : Bool := false + +private def snippetRange? (text : String) (ref : Syntax) : Option Lean.Lsp.Range := do + -- Bounds alone cannot establish provenance: a custom trace may carry syntax from another file. + let source ← ref.getSubstring? + guard (source.str == text) + let start ← ref.getPos? + let stop ← ref.getTailPos? + guard (start <= stop && stop.byteIdx <= text.utf8ByteSize) + let fileMap := text.toFileMap + return { start := fileMap.utf8PosToLspPos start, «end» := fileMap.utf8PosToLspPos stop } + +private def visit (origin stop : Float) (thread : UInt64) (fuel : Nat) + (parent? : Option Nat) (range? : Option Lean.Lsp.Range) (msg : MessageData) : + StateM Projection Unit := do + let state ← get + if state.visited >= maxVisited || state.spans.size >= maxSpans then + modify fun s => { s with truncated := true } + return + match fuel with + | 0 => modify fun s => { s with truncated := true } + | fuel + 1 => + modify fun s => { s with visited := s.visited + 1 } + match msg with + | .trace data _ children => + let mut parent? := parent? + -- Exclude untimed nodes and invalid/non-finite intervals. The bounds also prevent traces + -- inherited from a saved snapshot from being presented as work done by this request. + if data.startTime >= origin && data.stopTime >= data.startTime && data.stopTime <= stop then + let index := (← get).spans.size + let fullCategory := data.cls.toString + let category := (fullCategory.take 160).toString + let tag := (data.tag.take 256).toString + modify fun s => { s with + truncated := s.truncated || category != fullCategory || tag != data.tag + spans := s.spans.push { + parent?, thread + category, tag + startMs := (data.startTime - origin) * 1000 + durationMs := (data.stopTime - data.startTime) * 1000 + range? + } } + parent? := some index + for child in children do + if (← get).visited >= maxVisited || (← get).spans.size >= maxSpans then + modify fun s => { s with truncated := true } + break + -- Nested MessageData does not retain a trustworthy source reference on all supported + -- Lean versions. Do not copy an enclosing range onto a child. + visit origin stop thread fuel parent? none child + | .withContext _ msg | .withNamingContext _ msg | .nest _ msg | .group msg + | .tagged _ msg | .ofWidget _ msg => visit origin stop thread fuel parent? range? msg + | .compose left right => + visit origin stop thread fuel parent? range? left + visit origin stop thread fuel parent? range? right + | _ => pure () + +/-- Project a bounded forest without evaluating lazy labels or pretty-printing expressions. +The limits bound this projection and its response, not Lean's upstream trace allocation. -/ +def collect (startNs stopNs : Nat) (states : Array TraceState) (text : String) : Result := Id.run do + let origin := startNs.toFloat / 1000000000 + let stop := stopNs.toFloat / 1000000000 + let project : StateM Projection Unit := do + for state in states do + if (← get).visited >= maxVisited then + modify fun s => { s with truncated := true } + return + modify fun s => { s with visited := s.visited + 1 } + for trace in state.traces do + if (← get).visited >= maxVisited || (← get).spans.size >= maxSpans then + modify fun s => { s with truncated := true } + return + visit origin stop state.tid maxDepth none (snippetRange? text trace.ref) trace.msg + let (_, projection) := project.run {} + return { + elapsedMs := (stopNs - startNs).toFloat / 1000000 + thresholdMs + spans := projection.spans + truncated := projection.truncated + } + +end Beam.LSP.RunAt.Profile diff --git a/Beam/Lean/Operation.lean b/Beam/Lean/Operation.lean index 36fc0d15..dc3556b9 100644 --- a/Beam/Lean/Operation.lean +++ b/Beam/Lean/Operation.lean @@ -154,11 +154,15 @@ private def rangeEndCharacterField : String × Json := ("end_character", Beam.JsonSchema.natural "Zero-based UTF-16 LSP end character.") private def runAtTextField : String × Json := - ("text", Beam.JsonSchema.string "One Lean command or tactic block to run at the selected position. Top-level command sequences are not accepted by one runAt call.") + ("text", Beam.JsonSchema.string "One Lean command or tactic block to run at the selected position. To profile an existing declaration, submit its complete source at its start position in the synced version. To profile a proof body, submit its full tactic sequence without by at the first tactic's position. Top-level command sequences are not accepted by one runAt call.") private def continuationTextField : String × Json := ("text", Beam.JsonSchema.string "One Lean continuation command or tactic block to run from the stored handle.") +private def profileField : String × Json := + ("profile", Beam.JsonSchema.bool + "When true, return profile.elapsedMs and bounded profile.spans, including timed tactic scopes with a 1ms profiler threshold. These overlapping wall timings include profiling overhead; do not sum span durations. Profiling applies only to this execution.") + private def handleField : String × Json := ("handle", Beam.JsonSchema.object "Opaque broker-wrapped Lean handle from a previous tool result.") @@ -221,7 +225,7 @@ private def documentFields : List (String × Json) := open Beam.JsonSchema in def Operation.inputSchema : Operation → Json | .runAt | .runAtHandle => - inputObject (positionFields ++ [runAtTextField]) #["path", "version", "line", "character", "text"] + inputObject (positionFields ++ [runAtTextField, profileField]) #["path", "version", "line", "character", "text"] | .hover | .signatureHelp | .definition => inputObject positionFields #["path", "version", "line", "character"] | .references => @@ -238,7 +242,7 @@ def Operation.inputSchema : Operation → Json | .codeActionResolve => inputObject (documentFields ++ [codeActionField]) #["path", "version", "code_action"] | .runWith | .runWithLinear => - inputObject [pathField, handleField, continuationTextField] #["path", "handle", "text"] + inputObject [pathField, handleField, continuationTextField, profileField] #["path", "handle", "text"] | .release => inputObject [pathField, releaseHandleField] #["path", "handle"] | .update => @@ -261,7 +265,38 @@ structure RunAtInput where line : Nat character : Nat text : String - deriving FromJson, ToJson + profile? : Option Bool := none + +private def profileField? (j : Json) : Except String (Option Bool) := do + match j.getObjVal? "profile" with + | .ok value => + match fromJson? value with + | .ok profile => pure (some profile) + | .error err => throw s!"invalid 'profile': {err}" + | .error _ => pure none + +instance : ToJson RunAtInput where + toJson input := + Json.mkObj <| [ + ("path", toJson input.path), + ("version", toJson input.version), + ("line", toJson input.line), + ("character", toJson input.character), + ("text", toJson input.text) + ] ++ + match input.profile? with + | some profile => [("profile", toJson profile)] + | none => [] + +instance : FromJson RunAtInput where + fromJson? j := do + let path ← j.getObjValAs? String "path" + let version ← j.getObjValAs? Nat "version" + let line ← j.getObjValAs? Nat "line" + let character ← j.getObjValAs? Nat "character" + let text ← j.getObjValAs? String "text" + let profile? ← profileField? j + pure { path, version, line, character, text, profile? } /-- Input for position-based Lean inspection operations. -/ structure PositionInput where @@ -417,7 +452,26 @@ structure RunWithInput where path : String handle : Beam.Broker.Handle text : String - deriving FromJson, ToJson + profile? : Option Bool := none + +instance : ToJson RunWithInput where + toJson input := + Json.mkObj <| [ + ("path", toJson input.path), + ("handle", toJson input.handle), + ("text", toJson input.text) + ] ++ + match input.profile? with + | some profile => [("profile", toJson profile)] + | none => [] + +instance : FromJson RunWithInput where + fromJson? j := do + let path ← j.getObjValAs? String "path" + let handle ← j.getObjValAs? Beam.Broker.Handle "handle" + let text ← j.getObjValAs? String "text" + let profile? ← profileField? j + pure { path, handle, text, profile? } /-- Input for explicit handle release. -/ structure ReleaseInput where @@ -483,6 +537,7 @@ def RunAtInput.toBrokerRequest character := input.character text := input.text storeHandle? := if storeHandle then some true else none + profile? := input.profile? } } @@ -589,6 +644,7 @@ def RunWithInput.toBrokerRequest text := input.text storeHandle? := some true linear? := some linear + profile? := input.profile? handle := input.handle } } diff --git a/Beam/Mcp/Projection.lean b/Beam/Mcp/Projection.lean index cd8f0064..121c920f 100644 --- a/Beam/Mcp/Projection.lean +++ b/Beam/Mcp/Projection.lean @@ -303,6 +303,7 @@ structure RunAtBrokerResult where success : Bool := true messages : Array Beam.LSP.RunAt.Message := #[] traces : Array String := #[] + profile? : Option Beam.LSP.RunAt.Profile.Result := none handle? : Option Beam.Broker.Handle := none proofState? : Option Beam.LSP.Lib.ProofState := none @@ -311,12 +312,14 @@ instance : FromJson RunAtBrokerResult where let success? ← optionalField? (α := Bool) j "success" let messages? ← optionalField? (α := Array Beam.LSP.RunAt.Message) j "messages" let traces? ← optionalField? (α := Array String) j "traces" + let profile? ← optionalField? (α := Beam.LSP.RunAt.Profile.Result) j "profile" let handle? ← optionalField? (α := Beam.Broker.Handle) j "handle" let proofState? ← optionalField? (α := Beam.LSP.Lib.ProofState) j "proofState" pure { success := success?.getD true messages := messages?.getD #[] traces := traces?.getD #[] + profile? handle? proofState? } @@ -344,13 +347,16 @@ The MCP surface uses `next_handle` and `proof_state` rather than the Lean/LSP pa back unchanged. -/ def runAtResultJson (result : RunAtBrokerResult) : Json := - Json.mkObj [ + Json.mkObj <| [ ("success", toJson result.success), ("messages", toJson result.messages), ("traces", toJson result.traces), ("proof_state", optionJson result.proofState?), ("next_handle", optionJson result.handle?) - ] + ] ++ + match result.profile? with + | some profile => [("profile", toJson profile)] + | none => [] def normalizeRunAtResult (result : Json) : Except ToolError Json := do match fromJson? (α := RunAtBrokerResult) result with diff --git a/docs/MCP.md b/docs/MCP.md index 8b80af57..af9a5b2a 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -259,6 +259,17 @@ first edit and save the Lean file with the client's normal file-editing tool. Th before another snapshot-bound operation, or call `lean_sync` when a diagnostics/readiness barrier is needed. Both commands read the current on-disk file; neither applies or recovers speculative text. +### Opt-in timing profiles + +`lean_run_at`, `lean_run_at_handle`, `lean_run_with`, and `lean_run_with_linear` accept an optional +boolean `profile`. When it is `true`, the returned run result includes `profile`; it is omitted when +the argument is absent or false. A parse failure also has no profile. Profiled requests return +`traces: []`; ordinary messages and proof success or failure are unchanged. The profile contract, +limits, timing interpretation, and source-range rules are in [Opt-in proof profiling](STATUS.md#opt-in-proof-profiling). +For whole-proof timing, send a complete tactic block at the first tactic's before-state or a full +theorem command at a command position. Existing declarations and full files are not automatically +replayed for profiling. + `lean_code_action_resolve` takes a `code_action` payload previously returned by `lean_todo`. Clients apply any returned LSP `WorkspaceEdit` themselves, then call `lean_update` or `lean_sync` again so Beam observes the edited file and reports the new version. Use `lean_sync` instead of `lean_update` diff --git a/docs/SETUP.md b/docs/SETUP.md index 627df973..73e4ad97 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -332,6 +332,38 @@ printf '%s\n' 'example : True := by' ' trivial' | lean-beam run-at "Foo.lean" "$version" 10 2 --stdin ``` +Add `--profile` immediately before the text selector to return a bounded timing profile for that +speculative execution: + +```bash +lean-beam run-at "Foo.lean" "$version" 10 2 --profile --stdin +``` + +The same selector works with `run-at-handle`, `run-with`, and `run-with-linear`. Profiled responses +have `profile` timing metadata and `traces: []`; ordinary messages and proof success/failure remain +available. Put a literal `--profile` after the `--` text separator. Read the [profile +contract](STATUS.md#opt-in-proof-profiling) for collection limits and timing interpretation. + +To measure a declaration you just wrote, save and sync the file, then submit that declaration's +complete source at its starting position with the returned version. Beam uses the preceding +snapshot, so the declaration can keep its existing name. This re-elaborates just the submitted +declaration, including its proof, against the loaded environment; it does not run a full build. +For example, if this theorem starts on line 11 (zero-based line 10): + +```bash +cat <<'EOF' | lean-beam run-at "Foo.lean" "$version" 10 0 --profile --stdin +theorem measured : True := by + exact trivial +EOF +``` + +Use `profile.elapsedMs` for the speculative elaboration's elapsed wall time. The `profile.spans` +array includes Lean's timed tactic scopes (`category: "Elab.step"`, with tactic syntax kinds in +`tag`), using a 1ms profiler threshold. Parent and child durations overlap. Alternatively, submit the +complete tactic sequence, without `by`, at the first tactic's position to measure only the proof +body. Include its indentation and nested goal blocks. Declaration selection by name is not part +of this API: the caller supplies the source and position from the same synced file version. + Read those commands like this: - `lean-beam update` opens or updates the broker's LSP mirror and returns the current document diff --git a/docs/STATUS.md b/docs/STATUS.md index 61655e51..c19d3ec7 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -16,7 +16,8 @@ Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md - standalone Lean plugin for `$/lean/runAt` - internal proof-first, command-fallback basis selection -- typed response payload with messages, traces, optional proof state, and optional follow-up handle +- typed response payload with messages, traces, optional proof state, optional follow-up handle, and + opt-in bounded timing profiles - optional follow-up execution through `$/lean/runWith` and `$/lean/releaseHandle` - agent-oriented `$/lean/todo` range inspection for actionable items such as sorries, holes, diagnostics, code actions, and incomplete proofs, exposed through the broker, `lean-beam todo`, @@ -103,6 +104,35 @@ The base request remains intentionally small: Request-level failures stay at the transport layer. Semantic Lean outcomes stay in the normal typed response payload. +### Opt-in proof profiling + +`runAt` and `runWith` accept an optional `profile: true` selector. A completed execution profile +adds `profile` to the normal response with wall-clock `elapsedMs`, a fixed `thresholdMs: 1`, and a +flat span forest. Each span has an earlier `parent` index when known, its Lean thread identity, +category, tag, start offset, duration, and an optional range relative to the submitted text when +the trace source bytes and bounds match that text. `elapsedMs` excludes request parsing, document readiness, +and response formatting; it includes registered Lean snapshot tasks owned by the speculative +execution. Unregistered background work is outside the profile. It is wall time, not CPU time, and +profiling itself perturbs the measured execution. + +Profile projection is limited to 1,024 spans, 8,192 visited metadata nodes, and depth 128, with +bounded category and tag text. `truncated: true` reports a projection limit. These limits bound +Beam's response work and payload; Lean's upstream profiler allocation remains unbounded. Profiles +do not use heartbeat timings, preserve normal cancellation limits, and replace rendered `traces` +with `[]` for that request. Messages and proof success or failure remain in the normal result. +Parse failures have no profile. Lean records only emitted profiler scopes: the 1ms threshold normally +omits small scopes, explicitly enabled trace classes can include shorter scopes, and user-suppressed +scopes are absent. This is bounded timing metadata rather than +an exhaustive CPU profile. Parent spans contain child work and spans can overlap; never sum their +durations to obtain `elapsedMs`. + +For useful whole-proof timing, submit a complete tactic block at the first tactic's before-state, or +submit a full theorem command at a command position. To measure an existing declaration, submit +its source at its start position in the synced version: the preceding snapshot lets it keep its +original name. Selection by declaration name and automatic whole-file profiling are unsupported. +This measures fresh speculative elaboration against a loaded environment, not the earlier edit's +timing or cold import/build cost. See the [single-declaration workflow](SETUP.md#use-beam-from-a-lean-project). + Follow-up handles exist, but they should be treated as pre-stable support APIs rather than as a frozen long-term contract. They are opaque, workspace- and document-bound, invalidated by same-document edits, document close, worker or daemon restart, and reset/drop of their owning workspace. Exact diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index f3be1b63..a9e035a1 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -241,6 +241,35 @@ batch-equivalence check rather than one-file probing. `lean-beam run-at` is a speculative execution request against one explicit broker document version. Read it as "try this Lean text here", not as "edit the file here". +Add `--profile` immediately before the text input selector when timing one speculative execution: + +```bash +lean-beam run-at "Foo.lean" "$version" 10 2 --profile -- "exact trivial" +``` + +For a whole proof, select the first tactic's before-state and pass the complete tactic sequence, +without a leading `by`: + +```bash +cat <<'EOF' | lean-beam run-at "Foo.lean" "$version" 10 2 --profile --stdin +constructor +· exact trivial +· exact trivial +EOF +``` + +Profiled responses return bounded `profile` metadata and `traces: []`; messages and the normal +proof result are unchanged. To pass `--profile` as literal Lean text, put it after the `--` text +separator. Read [the profile contract](../../docs/STATUS.md#opt-in-proof-profiling) before using +timings for comparisons. + +To measure an existing declaration, sync the saved file and submit its complete source at the +declaration's start position with that version and `--profile`. The preceding snapshot permits +the original name and avoids a project rebuild. Use `profile.elapsedMs` for elapsed elaboration +time and `profile.spans` for timed scopes, including `Elab.step` tactic kinds. These are fresh +speculative timings with a 1ms profiler threshold; overlapping spans must not be summed. +There is no declaration-name selector: use the source and position from the synced version. + What `lean-beam run-at` does not do: - it does not edit the source file or create a new on-disk baseline for the next request diff --git a/tests/lean/BeamTest/Broker/CliDaemonTest.lean b/tests/lean/BeamTest/Broker/CliDaemonTest.lean index a3078e56..d395fb05 100644 --- a/tests/lean/BeamTest/Broker/CliDaemonTest.lean +++ b/tests/lean/BeamTest/Broker/CliDaemonTest.lean @@ -724,6 +724,9 @@ private def checkLeanOperationRequests : IO Unit := do requireRequestJson "runAt handle request should share the Lean operation adapter" (Beam.Cli.leanRunAtRequest path 12 4 2 "exact h" (storeHandle := true)) (runAtInput.toBrokerRequest (storeHandle := true)) + requireRequestJson "profiled runAt request should share the Lean operation adapter" + (Beam.Cli.leanRunAtRequest path 12 4 2 "exact h" (profile := true)) + ({ runAtInput with profile? := some true }).toBrokerRequest expectIoErrorContains "runAt missing text should fail at the CLI boundary" "usage: lean-beam" (Beam.Cli.parseTextArg "run-at Demo.lean 12 4 2" []) @@ -780,6 +783,9 @@ private def checkLeanOperationRequests : IO Unit := do requireRequestJson "runWith linear request should share the Lean operation adapter" (Beam.Cli.leanRunWithRequest path sampleBrokerHandle "simp" (linear := true)) (runWithInput.toBrokerRequest (linear := true)) + requireRequestJson "profiled runWith request should share the Lean operation adapter" + (Beam.Cli.leanRunWithRequest path sampleBrokerHandle "simp" (profile := true)) + ({ runWithInput with profile? := some true }).toBrokerRequest expectIoErrorContains "runWith missing text should fail at the CLI boundary" "usage: lean-beam" (Beam.Cli.parseTextArg "run-with Demo.lean HANDLE" []) @@ -837,6 +843,22 @@ private def checkDiagnosticScopeArgs : IO Unit := do pure <| err.toString.contains "+all-diagnostics" require s!"{label} diagnostic scope should reject obsolete +full" obsoleteRejected +private def checkProfileArgs : IO Unit := do + let (enabled, profiledTextArgs) ← Beam.Cli.parseProfileArg ["--profile", "--stdin"] + require "profile selector should enable profiling" enabled + require "profile selector should leave the text input selector" (profiledTextArgs == ["--stdin"]) + + let (escapedEnabled, escapedTextArgs) ← Beam.Cli.parseProfileArg ["--", "--profile"] + require "escaped profile text should not enable profiling" !escapedEnabled + let escapedText ← Beam.Cli.parseTextArg "run-at Demo.lean 12 4 2" escapedTextArgs + require "escaped --profile should remain literal Lean text" (escapedText.text == "--profile") + + expectIoErrorContains "repeated profile selector should fail" + "duplicate --profile" (Beam.Cli.parseProfileArg ["--profile", "--profile", "exact trivial"]) + let (_, malformedTextArgs) ← Beam.Cli.parseProfileArg ["--profile", "--stdin", "extra"] + expectIoErrorContains "profiled malformed text selector should fail at the text boundary" + "usage: lean-beam" (Beam.Cli.parseTextArg "run-at Demo.lean 12 4 2" malformedTextArgs) + private def checkDaemonFailureContext : IO Unit := do let root := System.FilePath.mk s!"/tmp/beam-daemon-failure-context-{← IO.monoNanosNow}" try @@ -1721,6 +1743,7 @@ def main : IO Unit := do checkProjectRootAmbiguity checkLeanOperationRequests checkDiagnosticScopeArgs + checkProfileArgs checkDaemonFailureContext checkDaemonFailureUnreadableStartupLog checkTypedDaemonFailureClassification diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean index d4a5f307..424de5eb 100644 --- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean +++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean @@ -539,6 +539,65 @@ private def checkBrokerRequestAdapters : IO Unit := do require "save tool rejection identifies diagnostics_in_result" (err.contains "diagnostics_in_result") +private def checkProfileRequestAdapters : IO Unit := do + let root := "/repo" + let workspaceId := "local:/repo" + let inWorkspace (json : Json) : Json := + json.setObjVal! "workspace" (toJson ({ root } : Beam.Workspace.Descriptor)) + + let runAtInput : Beam.Mcp.RunAtInput := { + path := "Demo.lean" + version := 12 + line := 4 + character := 2 + text := "exact h" + } + let runAtReq ← expectOk "unprofiled runAt tool request" <| + Beam.Mcp.leanOperationToBrokerRequest .runAt workspaceId (inWorkspace <| toJson runAtInput) + let runAt ← expectRequestPayload "unprofiled runAt tool request" runAtReq fun + | .runAt request => some request + | _ => none + require "runAt does not profile by default" runAt.profile?.isNone + requireFieldAbsent "runAt input json" "profile" (toJson runAtInput) + + let profiledRunAtInput : Beam.Mcp.RunAtInput := { runAtInput with profile? := some true } + let profiledRunAtReq ← expectOk "profiled runAt tool request" <| + Beam.Mcp.leanOperationToBrokerRequest .runAt workspaceId + (inWorkspace <| toJson profiledRunAtInput) + let profiledRunAt ← expectRequestPayload "profiled runAt tool request" profiledRunAtReq fun + | .runAt request => some request + | _ => none + require "profiled runAt forwards profile" (profiledRunAt.profile? == some true) + requireJsonBool "profiled runAt input json" "profile" true (toJson profiledRunAtInput) + match Beam.Mcp.leanOperationToBrokerRequest .runAt workspaceId (inWorkspace <| Json.mkObj [ + ("path", toJson "Demo.lean"), ("version", toJson 12), ("line", toJson 4), + ("character", toJson 2), ("text", toJson "exact h"), ("profile", toJson "true")]) with + | .ok _ => throw <| IO.userError "runAt accepted a non-boolean profile" + | .error _ => pure () + + let runWithInput : Beam.Mcp.RunWithInput := { + path := "Demo.lean" + handle := sampleBrokerHandle + text := "simp" + } + let runWithReq ← expectOk "unprofiled runWith tool request" <| + Beam.Mcp.leanOperationToBrokerRequest .runWith workspaceId + (inWorkspace <| toJson runWithInput) + let runWith ← expectRequestPayload "unprofiled runWith tool request" runWithReq fun + | .runWith request => some request + | _ => none + require "runWith does not profile by default" runWith.profile?.isNone + requireFieldAbsent "runWith input json" "profile" (toJson runWithInput) + + let profiledRunWithInput : Beam.Mcp.RunWithInput := { runWithInput with profile? := some true } + let profiledRunWithReq ← expectOk "profiled runWith tool request" <| + Beam.Mcp.leanOperationToBrokerRequest .runWith workspaceId + (inWorkspace <| toJson profiledRunWithInput) + let profiledRunWith ← expectRequestPayload "profiled runWith tool request" profiledRunWithReq fun + | .runWith request => some request + | _ => none + require "profiled runWith forwards profile" (profiledRunWith.profile? == some true) + private def checkRunAtNormalization : IO Unit := do let semanticFailure := Json.mkObj [("success", toJson false)] let normalizedFailure ← expectToolOk "normalize semantic failure" <| @@ -548,6 +607,21 @@ private def checkRunAtNormalization : IO Unit := do requireJsonNull "semantic failure result" "next_handle" normalizedFailure requireJsonNull "semantic failure result" "proof_state" normalizedFailure requireFieldAbsent "semantic failure result" "ok" normalizedFailure + + let unprofiledSuccess := Json.mkObj [ + ("success", toJson true), + ("messages", toJson (#[] : Array Beam.LSP.RunAt.Message)), + ("traces", toJson (#[] : Array String)) + ] + let normalizedUnprofiled ← expectToolOk "normalize unprofiled result" <| + Beam.Mcp.normalizeBrokerResponse (.leanOperation .runAt) (Beam.Broker.Response.success unprofiledSuccess) + requireFieldAbsent "unprofiled result" "profile" normalizedUnprofiled + + let profile : Beam.LSP.RunAt.Profile.Result := { elapsedMs := 3.5 } + let profiledSuccess := unprofiledSuccess.setObjVal! "profile" (toJson profile) + let normalizedProfiled ← expectToolOk "normalize profiled result" <| + Beam.Mcp.normalizeBrokerResponse (.leanOperation .runAt) (Beam.Broker.Response.success profiledSuccess) + discard <| requireObjVal "profiled result" "profile" normalizedProfiled requireFieldAbsent "semantic failure result" "handle" normalizedFailure requireFieldAbsent "semantic failure result" "proofState" normalizedFailure @@ -744,6 +818,7 @@ def main : IO Unit := do checkToolNames checkToolDescriptors checkBrokerRequestAdapters + checkProfileRequestAdapters checkRunAtNormalization checkSyncAndSaveNormalization checkTransportErrorNormalization diff --git a/tests/lean/BeamTest/Broker/ProtocolTest.lean b/tests/lean/BeamTest/Broker/ProtocolTest.lean index 9f9d9396..2c97f67c 100644 --- a/tests/lean/BeamTest/Broker/ProtocolTest.lean +++ b/tests/lean/BeamTest/Broker/ProtocolTest.lean @@ -753,6 +753,42 @@ private def checkStaleDirectDepHints : IO Unit := do noopSyncHints.isEmpty private def checkRequestBoundary : IO Unit := do + let profiledRunAt : Request := { payload := .runAt { + path := "Demo.lean" + version := 7 + line := 1 + character := 2 + text := "exact trivial" + profile? := some true + } } + requireJsonBool "profiled run_at request" "profile" true (toJson profiledRunAt) + let decodedProfiledRunAt ← expectOk "decode profiled run_at request" <| + fromJson? (α := Request) (toJson profiledRunAt) + match decodedProfiledRunAt.payload with + | .runAt request => require "profiled run_at survives decode" (request.profile? == some true) + | _ => throw <| IO.userError "profiled run_at decoded as another operation" + let profiledRunWith : Request := { payload := .runWith { + path := "Demo.lean" + text := "exact trivial" + profile? := some false + handle := sampleHandle + } } + requireJsonBool "profiled run_with request" "profile" false (toJson profiledRunWith) + let decodedProfiledRunWith ← expectOk "decode profiled run_with request" <| + fromJson? (α := Request) (toJson profiledRunWith) + match decodedProfiledRunWith.payload with + | .runWith request => require "profiled run_with survives decode" (request.profile? == some false) + | _ => throw <| IO.userError "profiled run_with decoded as another operation" + expectDecodeFailure Request "run_at request rejects non-boolean profile" <| Json.mkObj [ + ("op", toJson "run_at"), + ("backend", toJson "lean"), + ("path", toJson "Demo.lean"), + ("version", toJson 7), + ("line", toJson 1), + ("character", toJson 2), + ("text", toJson "exact trivial"), + ("profile", toJson "true") + ] expectDecodeFailure Request "run_at request missing version" <| Json.mkObj [ ("op", toJson "run_at"), ("backend", toJson "lean"), diff --git a/tests/lean/BeamTest/LSP/RequestSurfaceTest.lean b/tests/lean/BeamTest/LSP/RequestSurfaceTest.lean index 60b8d2d4..5cca63ab 100644 --- a/tests/lean/BeamTest/LSP/RequestSurfaceTest.lean +++ b/tests/lean/BeamTest/LSP/RequestSurfaceTest.lean @@ -9,6 +9,7 @@ import BeamTest.LSP.Handle.Lifecycle import BeamTest.LSP.Requests.DiagnosticsBarrier.BasicTest import BeamTest.LSP.Requests.Goals.BasicTest import BeamTest.LSP.Requests.RunAt.BasicTest +import BeamTest.LSP.Requests.RunAt.ProfileTest import BeamTest.LSP.Requests.Save.BasicTest import BeamTest.LSP.Requests.Todo.BasicTest @@ -16,6 +17,7 @@ namespace BeamTest.LSP.RequestSurfaceTest def main : IO Unit := BeamTest.LSP.Scenario.run do BeamTest.LSP.Requests.RunAt.BasicTest.run + BeamTest.LSP.Requests.RunAt.ProfileTest.run BeamTest.LSP.Requests.Goals.BasicTest.run BeamTest.LSP.Requests.Todo.BasicTest.run BeamTest.LSP.Requests.DiagnosticsBarrier.BasicTest.run diff --git a/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean b/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean new file mode 100644 index 00000000..51e69f48 --- /dev/null +++ b/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean @@ -0,0 +1,227 @@ +/- +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 BeamTest.LSP.Requests.Support + +open Lean +open BeamTest.LSP.Scenario +open BeamTest.LSP.Requests.Support + +namespace BeamTest.LSP.Requests.RunAt.ProfileTest + +private def require (condition : Bool) (message : String) : IO Unit := + unless condition do throw <| IO.userError message + +private def profileOf (result : Beam.LSP.RunAt.Result) : ScenarioM Beam.LSP.RunAt.Profile.Result := do + let some profile := result.profile? + | throw <| IO.userError s!"missing profile: {(toJson result).compress}" + require (profile.elapsedMs > 0) "profile elapsed time must be positive" + require (!profile.truncated) "small profile unexpectedly truncated" + require (profile.thresholdMs == 1) "profile threshold changed" + for i in [:profile.spans.size] do + let span := profile.spans[i]! + require (span.startMs >= 0 && span.durationMs >= 0) "negative span time" + require (span.startMs + span.durationMs <= profile.elapsedMs + 0.01) + "span exceeds execution interval" + if let some parent := span.parent? then + require (parent < i) "span parent must precede child" + require (profile.spans[parent]!.thread == span.thread) "parent crosses execution threads" + return profile + +private def hasCategory (profile : Beam.LSP.RunAt.Profile.Result) (category : String) : Bool := + profile.spans.any (·.category == category) + +private def awaitResult (request : ReqHandle) : ScenarioM Beam.LSP.RunAt.Result := + awaitResponseAs request + +def checkProjection : IO Unit := do + let forced ← IO.mkRef false + let label := MessageData.ofLazy (fun _ => do + forced.set true + pure <| Dynamic.mk (m!"expensive label")) (fun _ => false) + let child : MessageData := .trace { + cls := `child, startTime := 1.2, stopTime := 1.4, tag := "child" + } label #[] + let root : MessageData := .trace { + cls := `root, startTime := 1.1, stopTime := 1.9, tag := "root" + } label #[child] + let state : TraceState := { tid := 7, traces := ({} : PersistentArray TraceElem).push { ref := .missing, msg := root } } + let profile := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 #[state] "" + require (profile.spans.size == 2 && profile.spans[1]!.parent? == some 0) + "projection lost nested parent relation" + require (profile.spans.all (·.thread == 7)) "projection lost thread identity" + require (profile.spans.all (·.range?.isNone)) "projection invented a missing source location" + require (!profile.truncated && profile.elapsedMs == 1000) "unexpected projection summary" + require (!(← forced.get)) "projection evaluated a lazy trace label" + + let wide : MessageData := .trace { cls := `root, startTime := 1.1, stopTime := 1.9 } + label (Array.replicate (Beam.LSP.RunAt.Profile.maxSpans + 1) child) + let bounded := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 + #[{ state with traces := ({} : PersistentArray TraceElem).push { ref := .missing, msg := wide } }] "" + require (bounded.truncated && bounded.spans.size == Beam.LSP.RunAt.Profile.maxSpans) + "wide profile exceeded response budget or omitted truncation" + let deep := (List.range (Beam.LSP.RunAt.Profile.maxDepth + 1)).foldl (fun msg _ => .group msg) root + let depthBounded := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 + #[{ state with traces := ({} : PersistentArray TraceElem).push { ref := .missing, msg := deep } }] "" + require depthBounded.truncated "deep profile did not report truncation" + let old : MessageData := .trace { cls := `inherited, startTime := 0.1, stopTime := 0.2 } label #[] + let filtered := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 + #[{ state with traces := ({} : PersistentArray TraceElem).push { ref := .missing, msg := old } }] "" + require filtered.spans.isEmpty "projection attributed pre-request work to the request" + require (!(← forced.get)) "bounded projection evaluated lazy labels" + + let original : Options := ({} : Options).setBool `trace.profiler false |>.set `pp.width (41 : Nat) + let changed := (Beam.LSP.RunAt.Profile.options original).set `pp.width (72 : Nat) + let restored := Beam.LSP.RunAt.Profile.restoreOptions original changed + require (!trace.profiler.get restored && (trace.profiler.output.get? restored).isNone) + "option restoration retained instrumentation" + require (restored.get (α := Nat) `pp.width 0 == 72) "option restoration discarded command option changes" + +def checkProofs : ScenarioM Unit := do + let doc ← openDoc "tests/scenario/docs/ProfileProof.lean" + syncDoc doc + let complete ← sendRunAt doc { + line := 25, character := 2, text := "profile_left; profile_right; trivial", profile := true + } + let result ← awaitResult complete + require (result.success && result.proofState?.any (·.goals.isEmpty)) "whole proof did not solve" + let profile ← profileOf result + require (hasCategory profile "beam.profile.left" && hasCategory profile "beam.profile.right") + "whole proof must include both tactic phases" + require (result.traces.isEmpty) "profile should not pretty-print the trace tree" + + let multiline ← sendRunAt doc { + line := 25, character := 2 + text := "-- a complete proof block\nprofile_left\nhave h : True ∧ True := by\n constructor\n · trivial\n · trivial\nprofile_right\nexact h.1" + profile := true + } + let multilineResult ← awaitResult multiline + require (multilineResult.success && multilineResult.proofState?.any (·.goals.isEmpty)) + "multiline proof with nested goals failed" + + let failed ← sendRunAt doc { + line := 25, character := 2, text := "profile_left; exact (0 : Nat)", profile := true + } + let failure ← awaitResult failed + require (!failure.success && failure.messages.any (·.severity == .error)) "expected semantic proof failure" + let failureProfile ← profileOf failure + require (hasCategory failureProfile "beam.profile.left") "failure lost execution evidence on rollback" + + let left ← sendRunAt doc { + line := 25, character := 2, text := "profile_left; trivial", profile := true + } + let right ← sendRunAt doc { + line := 25, character := 2, text := "profile_right; trivial", profile := true + } + let leftProfile ← profileOf (← awaitResult left) + let rightProfile ← profileOf (← awaitResult right) + require (hasCategory leftProfile "beam.profile.left" && !hasCategory leftProfile "beam.profile.right") + "concurrent right probe leaked into left profile" + require (hasCategory rightProfile "beam.profile.right" && !hasCategory rightProfile "beam.profile.left") + "concurrent left probe leaked into right profile" + + let mint ← sendRunAt doc { + line := 25, character := 2, text := "profile_left", profile := true, storeHandle := true + } + let minted ← awaitResult mint + let some handle := minted.handle? | throw <| IO.userError "missing profiled proof handle" + let plain ← runWithHandle doc handle { text := "profile_check_off; trivial" } + let plainResult ← awaitResult plain + require (plainResult.success && plainResult.profile?.isNone && plainResult.traces.isEmpty) + "profiling leaked into unprofiled continuation" + let next ← runWithHandle doc handle { text := "profile_right; trivial", profile := true } + let nextProfile ← profileOf (← awaitResult next) + require (hasCategory nextProfile "beam.profile.right" && !hasCategory nextProfile "beam.profile.left") + "profiled continuation reported parent work" + + let plainRoot ← sendRunAt doc { + line := 25, character := 2, text := "profile_check_off; trivial" + } + let plainRootResult ← awaitResult plainRoot + require (plainRootResult.success && plainRootResult.profile?.isNone) "real proof state was modified" + let parseFailure ← sendRunAt doc { line := 25, character := 2, text := "(", profile := true } + let parsed ← awaitResult parseFailure + require (!parsed.success && parsed.profile?.isNone) "parse failure must not claim execution evidence" + closeDoc doc + +def checkCommands : ScenarioM Unit := do + let doc ← openDoc "tests/scenario/docs/ProfileProof.lean" + syncDoc doc + -- Re-elaborate the declaration already present in the synced file at its start position. + -- The preceding snapshot must not include that declaration or unrelated later work. + let existing ← sendRunAt doc { + line := 27, character := 0 + text := "theorem existingProfiledDeclaration : True ∧ True := by\n constructor\n · profile_left\n trivial\n · profile_right\n trivial" + profile := true + } + let existingResult ← awaitResult existing + require existingResult.success "profiling an existing declaration used the wrong snapshot" + let existingProfile ← profileOf existingResult + require (hasCategory existingProfile "beam.profile.left" && hasCategory existingProfile "beam.profile.right") + "existing declaration omitted part of its tactic breakdown" + let theoremReq ← sendRunAt doc { + line := 22, character := 0 + text := "theorem profiledWholeTheorem : True := by\n profile_left\n profile_right\n trivial" + profile := true, storeHandle := true + } + let result ← awaitResult theoremReq + require result.success "whole theorem profiling failed" + let profile ← profileOf result + require (hasCategory profile "beam.profile.left" && hasCategory profile "beam.profile.right") + "whole theorem omitted asynchronous proof body" + let some handle := result.handle? | throw <| IO.userError "missing command handle" + let check ← runWithHandle doc handle { text := "profile_check_command" } + let checked ← awaitResult check + require (checked.success && checked.profile?.isNone && checked.traces.isEmpty) + "command handle retained profiling options or traces" + let continued ← runWithHandle doc handle { + text := "example : True := by profile_right; trivial", profile := true + } + let continuationProfile ← profileOf (← awaitResult continued) + require (!hasCategory continuationProfile "beam.profile.left") "command handle retained old task traces" + let failed ← sendRunAt doc { + line := 22, character := 0 + text := "theorem profiledFailedTheorem : False := by\n profile_left\n trivial" + profile := true + } + let failure ← awaitResult failed + require (!failure.success) "expected asynchronous theorem failure" + require (hasCategory (← profileOf failure) "beam.profile.left") "failed theorem lost async profile" + closeDoc doc + +def checkCancellationAndStaleness : ScenarioM Unit := do + let doc ← openDoc "tests/scenario/docs/SlowPoll.lean" + syncDoc doc + let request ← sendRunAt doc { line := 28, character := 2, text := "poll_sleep_tac", profile := true } + IO.sleep 100 + cancelReq request + expectErrorContains request <| Json.mkObj [("code", toJson "requestCancelled")] + let survivor ← sendRunAt doc { line := 28, character := 2, text := "custom_trivial", profile := true } + require (← awaitResult survivor).success "cancelled profile affected the next probe" + let theoremRequest ← sendRunAt doc { + line := 25, character := 0 + text := "example : True := by poll_sleep_tac", profile := true + } + IO.sleep 100 + cancelReq theoremRequest + expectErrorContains theoremRequest <| Json.mkObj [("code", toJson "requestCancelled")] + let theoremSurvivor ← sendRunAt doc { + line := 25, character := 0, text := "example : True := by trivial", profile := true + } + require (← awaitResult theoremSurvivor).success "cancelled async profile affected the next theorem" + let stale ← sendRunAt doc { line := 28, character := 2, text := "poll_sleep_tac", profile := true } + IO.sleep 100 + changeDoc doc { line := 0, character := 0, insert := "\n" } + expectContentModified stale + closeDoc doc + +def run : ScenarioM Unit := do + checkProjection + checkProofs + checkCommands + checkCancellationAndStaleness + +end BeamTest.LSP.Requests.RunAt.ProfileTest diff --git a/tests/lean/BeamTest/LSP/Scenario.lean b/tests/lean/BeamTest/LSP/Scenario.lean index 9d7db620..b820055b 100644 --- a/tests/lean/BeamTest/LSP/Scenario.lean +++ b/tests/lean/BeamTest/LSP/Scenario.lean @@ -39,12 +39,14 @@ structure SendRunAtSpec where character : Nat text : String storeHandle : Bool := false + profile : Bool := false deriving Inhabited, Repr, ToJson structure RunWithSpec where text : String storeHandle : Bool := false linear : Bool := false + profile : Bool := false deriving Inhabited, Repr, ToJson structure GoalsSpec where @@ -426,6 +428,7 @@ def sendRunAt (doc : DocHandle) (spec : SendRunAtSpec) : ScenarioM ReqHandle := position := { line := spec.line, character := spec.character } text := spec.text storeHandle? := if spec.storeHandle then some true else none + profile? := if spec.profile then some true else none } let requestID ← sendRequest Beam.LSP.RunAt.method (toJson params) registerRequest requestID (toJson params) @@ -438,6 +441,7 @@ def runWithHandle (doc : DocHandle) (handle : Beam.LSP.RunAt.Handle) (spec : Run text := spec.text storeHandle? := if spec.storeHandle then some true else none linear? := if spec.linear then some true else none + profile? := if spec.profile then some true else none } let requestID ← sendRequest Beam.LSP.RunAt.runWithMethod (toJson params) registerRequest requestID (toJson params) diff --git a/tests/lsp-coverage/cases.json b/tests/lsp-coverage/cases.json index 7da13b6e..46fdfd03 100644 --- a/tests/lsp-coverage/cases.json +++ b/tests/lsp-coverage/cases.json @@ -1,5 +1,29 @@ { "cases": [ + { + "id": "runAt.profiling", + "method": "$/lean/runAt", + "coverage": ["profiling", "isolation", "theorem-proof-failure", "mixed-concurrency"], + "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean#checkProofs" + }, + { + "id": "runAt.profiling-async-theorem", + "method": "$/lean/runAt", + "coverage": ["profiling", "theorem-proof-failure"], + "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean#checkCommands" + }, + { + "id": "runAt.profiling-cancel-stale", + "method": "$/lean/runAt", + "coverage": ["profiling", "cancellation", "stale-edit"], + "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean#checkCancellationAndStaleness" + }, + { + "id": "runWith.profiling-isolation", + "method": "$/lean/runWith", + "coverage": ["profiling", "handle-continuation"], + "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean#checkProofs" + }, { "id": "runAt.tactic-position", "method": "$/lean/runAt", diff --git a/tests/lsp-coverage/methods.json b/tests/lsp-coverage/methods.json index 423380f9..cd7e96fa 100644 --- a/tests/lsp-coverage/methods.json +++ b/tests/lsp-coverage/methods.json @@ -6,6 +6,7 @@ "registrySymbol": "Beam.LSP.RunAt.method", "definition": "Beam/LSP/RunAt.lean#method", "requiredCoverage": [ + "profiling", "isolation", "tactic-position", "single-command-limit", @@ -25,6 +26,7 @@ "registrySymbol": "Beam.LSP.RunAt.runWithMethod", "definition": "Beam/LSP/RunAt.lean#runWithMethod", "requiredCoverage": [ + "profiling", "handle-continuation", "handle-invalidation", "linear-handle", diff --git a/tests/scenario/docs/ProfileProof.lean b/tests/scenario/docs/ProfileProof.lean new file mode 100644 index 00000000..009a2102 --- /dev/null +++ b/tests/scenario/docs/ProfileProof.lean @@ -0,0 +1,33 @@ +import Lean + +open Lean Elab Tactic Command + +elab "profile_left" : tactic => do + withTraceNode `beam.profile.left (fun _ => pure "left") do + IO.sleep 15 + +elab "profile_right" : tactic => do + withTraceNode `beam.profile.right (fun _ => pure "right") do + IO.sleep 15 + +elab "profile_check_off" : tactic => do + let opts ← getOptions + if trace.profiler.get opts || (trace.profiler.output.get? opts).isSome then + throwError "profiling options leaked into continuation" + +elab "profile_check_command" : command => do + let opts ← getOptions + if trace.profiler.get opts || (trace.profiler.output.get? opts).isSome then + throwError "profiling options leaked into command continuation" + +def profileAnchor : Nat := 0 + +example : True := by + trivial + +theorem existingProfiledDeclaration : True ∧ True := by + constructor + · profile_left + trivial + · profile_right + trivial diff --git a/tests/test-mcp-stdio.py b/tests/test-mcp-stdio.py index c85c7727..5341f66d 100644 --- a/tests/test-mcp-stdio.py +++ b/tests/test-mcp-stdio.py @@ -1014,6 +1014,25 @@ def run_iteration(client, suffix): ) require_success("lean_run_at multiline probe", probe) require(probe.get("next_handle") is None, f"plain lean_run_at leaked a follow-up handle: {probe}") + require("profile" not in probe, f"plain lean_run_at unexpectedly returned profiling: {probe}") + + profiled = client.call_tool( + "lean_run_at", + { + "path": "PositionEmptyLine.lean", + "version": version, + "line": 1, + "character": 0, + "text": f"theorem mcpProfile{suffix} : True ∧ True := by\n constructor\n · trivial\n · trivial", + "profile": True, + }, + ) + require_success("profiled whole theorem", profiled) + timing = profiled.get("profile") + require(isinstance(timing, dict), f"MCP dropped the declaration profile: {profiled}") + require(timing.get("elapsedMs", 0) > 0, f"profile omitted elapsed time: {timing}") + require(isinstance(timing.get("spans"), list), f"profile omitted timed scopes: {timing}") + require(profiled.get("traces") == [], f"profile rendered trace strings: {profiled}") broken = client.call_tool( "lean_run_at", @@ -1036,9 +1055,11 @@ def run_iteration(client, suffix): "line": 1, "character": 0, "text": f"def mcpBase{suffix} : Nat := 1", + "profile": True, }, ) require_success("handle mint probe", minted) + require(isinstance(minted.get("profile"), dict), f"profiled handle lost timing: {minted}") base_handle = minted.get("next_handle") require(isinstance(base_handle, dict), f"handle mint did not return next_handle: {minted}") @@ -1048,9 +1069,11 @@ def run_iteration(client, suffix): "path": "PositionEmptyLine.lean", "handle": base_handle, "text": f"def mcpNext{suffix} : Nat := mcpBase{suffix} + 1", + "profile": True, }, ) require_success("handle continuation probe", continued) + require(isinstance(continued.get("profile"), dict), f"profiled continuation lost timing: {continued}") next_handle = continued.get("next_handle") require(isinstance(next_handle, dict), f"handle continuation did not return next_handle: {continued}") @@ -1063,6 +1086,7 @@ def run_iteration(client, suffix): }, ) require_success("linear handle continuation probe", linear) + require("profile" not in linear, f"profiling leaked into a later continuation: {linear}") linear_handle = linear.get("next_handle") require(isinstance(linear_handle, dict), f"linear continuation did not return next_handle: {linear}")