From 9108886b3332dc4a36bdbf076c1e1a641c658d9b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Nov 2026 05:12:27 -0800 Subject: [PATCH 1/4] fix: retain significant spans across profiling traces --- Beam/LSP/RunAt/Profile.lean | 244 ++++++++++++------ docs/MCP.md | 12 +- .../lean-beam/references/workflow-details.md | 7 +- .../LSP/Requests/RunAt/ProfileTest.lean | 41 +++ 4 files changed, 226 insertions(+), 78 deletions(-) diff --git a/Beam/LSP/RunAt/Profile.lean b/Beam/LSP/RunAt/Profile.lean index 1602ded6..ee93abaf 100644 --- a/Beam/LSP/RunAt/Profile.lean +++ b/Beam/LSP/RunAt/Profile.lean @@ -36,8 +36,8 @@ structure Result where def initialThresholdMs : Nat := 1 def maxSpans : Nat := 1024 -def maxVisited : Nat := 8192 -def maxDepth : Nat := 128 +def maxVisited : Nat := 16384 +def maxDepth : Nat := 256 def maxTopSpans : Nat := 10 def maxLabelChars : Nat := 160 private def maxSnippetSourceBytes : Nat := 8192 @@ -139,7 +139,6 @@ private structure Projection where spans : Array Span := #[] /-- Temporary references only, bounded with spans and dropped before publishing a result. -/ headers : Array MessageData := #[] - visited : Nat := 0 truncated : Bool := false private def boundedNameString (name : Name) (limit : Nat) : String × Bool := Id.run do @@ -200,79 +199,178 @@ private def snippetRange? (text : String) (ref : Syntax) : Option Lean.Lsp.Range let fileMap := text.toFileMap return { start := fileMap.utf8PosToLspPos start, «end» := fileMap.utf8PosToLspPos stop } -private def visit (origin stop : Float) (thread : UInt64) (fuel : Nat) - (heartbeatClock : Bool) (wrap : MessageData → MessageData) - (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 header children => - let mut parent? := parent? - -- Exclude untimed nodes and invalid intervals. The request-clock bounds also prevent traces - -- inherited from a saved snapshot from being presented as work done by this request. - -- TraceData has no clock tag. Lean's message context records the surrounding options; - -- never reinterpret a known heartbeat-clock node as seconds, even if its numbers happen - -- to lie in the request interval. A child's own context can restore wall-clock collection. - if heartbeatClock then - modify fun s => { s with truncated := true } - else if data.startTime >= origin && data.stopTime >= data.startTime && data.stopTime <= stop then - let index := (← get).spans.size - let (category, categoryTruncated) := boundedNameString data.cls 160 - let tag := (data.tag.take 256).toString - modify fun s => { s with - truncated := s.truncated || categoryTruncated || tag != data.tag - spans := s.spans.push { - parent?, thread, category, tag - startMs := (data.startTime - origin) * 1000 - durationMs := (data.stopTime - data.startTime) * 1000 - range? - } - headers := s.headers.push (wrap header) +private structure Observation where + key : List Nat + span : Span + -- Temporary original header references; no rendering/evaluation, bounded by valid visits. + header : MessageData + deriving Inhabited + +private structure Frame where + thread : UInt64 + fuel : Nat + heartbeat : Bool := false + wrap : MessageData → MessageData := id + parent? : Option Nat := none + pathRev : List Nat + range? : Option Lsp.Range := none + +private inductive Work where + | states (index : Nat) + | roots (stateIndex traceIndex : Nat) + | children (items : Array MessageData) (next : Nat) (frame : Frame) + | single (msg : MessageData) (frame : Frame) + +private structure Explored where + observations : Array Observation := #[] + visited : Nat := 0 + depthStops : Nat := 0 + incompatible : Nat := 0 + clipped : Bool := false + pendingAtStop : Nat := 0 + deriving Inhabited + +private def Explored.complete (e : Explored) : Bool := e.pendingAtStop == 0 && e.depthStops == 0 + +private def dispatch (origin stop : Float) (msg : MessageData) (f : Frame) + (e : Explored) : Explored × Array Work := Id.run do + if f.fuel == 0 then return ({e with depthStops := e.depthStops + 1}, #[]) + let mut e := {e with visited := e.visited + 1} + let f := {f with fuel := f.fuel - 1} + match msg with + | .trace data header children => + let mut f := f + if f.heartbeat then e := {e with incompatible := e.incompatible + 1} + else if data.startTime >= origin && data.stopTime >= data.startTime && data.stopTime <= stop then + let (category, clipped) := boundedNameString data.cls 160 + let tag := (data.tag.take 256).toString + let index := e.observations.size + let span : Span := { + parent? := f.parent? + thread := f.thread + category + tag + startMs := (data.startTime - origin) * 1000 + durationMs := (data.stopTime - data.startTime) * 1000 + range? := f.range? + } + e := {e with + observations := e.observations.push { + key := f.pathRev.reverse + span + header := f.wrap header } - 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 heartbeatClock wrap parent? none child - | .withContext context msg => - visit origin stop thread fuel (trace.profiler.useHeartbeats.get context.opts) - (fun m => wrap (.withContext context m)) parent? range? msg - | .withNamingContext context msg => - visit origin stop thread fuel heartbeatClock - (fun m => wrap (.withNamingContext context m)) parent? range? msg - | .nest _ msg | .group msg | .tagged _ msg | .ofWidget _ msg - | .ofOriginatingSyntax _ msg => visit origin stop thread fuel heartbeatClock wrap parent? range? msg - | .compose left right => - visit origin stop thread fuel heartbeatClock wrap parent? range? left - visit origin stop thread fuel heartbeatClock wrap parent? range? right - | _ => pure () - -private def project (startNs stopNs : Nat) (states : Array TraceState) (text : String) : Projection := Id.run do + clipped := e.clipped || clipped || tag != data.tag + } + f := {f with parent? := some index} + return (e, if children.isEmpty then #[] else #[.children children 0 {f with range? := none}]) + | .withContext context inner => + let innerFrame := {f with + heartbeat := trace.profiler.useHeartbeats.get context.opts + wrap := fun m => f.wrap (.withContext context m) + pathRev := 0 :: f.pathRev + } + return (e, #[.single inner innerFrame]) + | .withNamingContext context inner => + let innerFrame := {f with + wrap := fun m => f.wrap (.withNamingContext context m) + pathRev := 0 :: f.pathRev + } + return (e, #[.single inner innerFrame]) + | .nest _ inner | .group inner | .tagged _ inner | .ofWidget _ inner | .ofOriginatingSyntax _ inner => + return (e, #[.single inner {f with pathRev := 0 :: f.pathRev}]) + | .compose left right => return (e, #[.single left {f with pathRev := 0 :: f.pathRev}, + .single right {f with pathRev := 1 :: f.pathRev}]) + | _ => return (e, #[]) + +private def Work.level : Work → Nat + | .states .. | .roots .. => 0 + | .single _ frame | .children _ _ frame => maxDepth - frame.fuel + +/-- Visit complete shallow levels before deep descendants. Sequence cursors avoid expanding a +wide array into a work queue. Both retained candidates and pending cursors are bounded by visits. +Context wrappers count as levels, matching the existing depth limit. -/ +private def explore (startNs stopNs : Nat) (states : Array TraceState) (text : String) : Explored := 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 false id none (snippetRange? text trace.ref) trace.msg - let (_, projection) := project.run {} - return projection + let mut levels : Array (List Work) := Array.replicate (maxDepth + 1) [] + if !states.isEmpty then levels := levels.set! 0 [.states 0] + let mut e : Explored := {} + for depth in [:maxDepth + 1] do + for _ in [:3 * maxVisited + 1] do + if e.visited >= maxVisited then break + let work :: rest := levels[depth]! | break + levels := levels.set! depth rest + let mut tasks := #[] + match work with + | .states index => + e := {e with visited := e.visited + 1} + if !states[index]!.traces.isEmpty then tasks := tasks.push (.roots index 0) + if index + 1 < states.size then tasks := tasks.push (.states (index + 1)) + | .roots si ri => + let state := states[si]! + let item := state.traces[ri]! + let frame : Frame := { + thread := state.tid + fuel := maxDepth + pathRev := [ri, si] + range? := snippetRange? text item.ref + } + (e, tasks) := dispatch origin stop item.msg frame e + if ri + 1 < state.traces.size then tasks := tasks.push (.roots si (ri + 1)) + | .children items next frame => + (e, tasks) := dispatch origin stop items[next]! {frame with pathRev := next :: frame.pathRev} e + if next + 1 < items.size then tasks := tasks.push (.children items (next + 1) frame) + | .single msg frame => (e, tasks) := dispatch origin stop msg frame e + for task in tasks.reverse do + levels := levels.modify task.level (task :: ·) + if e.visited >= maxVisited then break + return {e with pendingAtStop := levels.foldl (fun n xs => n + xs.length) 0} + +private def sourceLT (a b : Observation) : Bool := compare a.key b.key == .lt + +/-- Rank inclusive observations, retaining all ancestors inside the same output budget. +Equal durations use original trace-tree order, independent of traversal scheduling. -/ +private def retain (e : Explored) (cap : Nat) : Array Nat := Id.run do + let ranked := (Array.range e.observations.size).qsort fun a b => + let x := e.observations[a]! + let y := e.observations[b]! + x.span.durationMs > y.span.durationMs || + (x.span.durationMs == y.span.durationMs && sourceLT x y) + let mut selected := #[] + let mut kept := Array.replicate e.observations.size false + for i in ranked do + if selected.size == cap then break + if kept[i]! then continue + let mut additions := #[i] + let mut parent := e.observations[i]!.span.parent? + for _ in [:maxDepth] do + let some p := parent | break + if kept[p]! then break + additions := additions.push p + parent := e.observations[p]!.span.parent? + if selected.size + additions.size <= cap then + for j in additions do + selected := selected.push j + kept := kept.set! j true + return selected.qsort (fun a b => sourceLT e.observations[a]! e.observations[b]!) + +private def materialize (explored : Explored) (cap : Nat) : Projection := Id.run do + let selected := retain explored cap + let mut indices : Array (Option Nat) := Array.replicate explored.observations.size none + let mut result : Projection := {truncated := !explored.complete || explored.incompatible > 0 || + explored.clipped || selected.size < explored.observations.size} + for i in selected do + let observation := explored.observations[i]! + let parent? := observation.span.parent?.bind (indices[·]!) + indices := indices.set! i (some result.spans.size) + result := {result with + spans := result.spans.push {observation.span with parent?} + headers := result.headers.push observation.header} + return result + +private def project (startNs stopNs : Nat) (states : Array TraceState) (text : String) : Projection := + materialize (explore startNs stopNs states text) maxSpans private def Projection.result (projection : Projection) (startNs stopNs : Nat) : Result := { elapsedMs := (stopNs - startNs).toFloat / 1000000 diff --git a/docs/MCP.md b/docs/MCP.md index 277ddb58..e3dc5135 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -475,9 +475,15 @@ UTF-16 character offsets; its end is exclusive. A range is not a document coordi that Lean can map the span to a source occurrence. If the source snippet exceeds 8192 UTF-8 bytes, Beam omits span ranges. -Profiling returns at most 1024 spans, limits traversal visits to 8192 (including trace-state entries), -and limits `MessageData` nesting to 128. Context and formatting wrappers count toward both traversal -bounds, so the retained span tree can stop below depth 128. `truncated: true` means projection omitted +Profiling returns at most 1024 spans, limits traversal visits to 16384 (including trace-state entries), +and limits `MessageData` nesting to 256. Traversal considers roots and shallow message nodes before +deeper descendants. Among visited timed nodes, retention ranks inclusive duration, breaking ties by +original trace-tree order. A node is admitted with all its timed ancestors only when the group fits +the remaining span budget. Results retain their original parent-before-child order with remapped +indices. Small forests that fit the bounds keep every span. Neither this selection nor the summary +claims global coverage when traversal stops; even fully visited phases may be excluded by the span budget. +Context and formatting wrappers count toward both traversal +bounds, so the retained span tree can stop below depth 256. `truncated: true` means projection omitted trace nodes or clipped raw category/tag identifiers; it does not identify which bound was reached. It can also report clock-incompatible nodes as described above. These traversal bounds do not bound Lean's upstream trace allocation or selected-label rendering. Profiled results preserve ordinary warnings and errors in `messages`, diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 7171485e..48e02f4a 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -160,8 +160,11 @@ a document position or a guaranteed mapping to a source occurrence. If the sourc Profiled results retain ordinary warnings and errors, but suppress ordinary Lean trace text from both `messages` and `traces`; `traces` is `[]`. Each continuation profile measures only that call, not earlier work represented by its handle. Nested and parallel spans overlap, so do not sum their -durations. The profile has at most 1024 spans, 8192 traversal visits (including trace-state entries), -and `MessageData` nesting depth 128. Context and formatting wrappers count, so span depth can be lower. +durations. The profile has at most 1024 spans, 16384 traversal visits (including trace-state entries), +and `MessageData` nesting depth 256. Shallow nodes are visited before deep descendants; retained +spans are chosen by inclusive duration with their ancestors, then returned in original tree order. +This favors significant work across the visited forest, but neither complete traversal nor retention +of every phase is guaranteed. Context and formatting wrappers count, so span depth can be lower. These limits do not bound Lean's trace allocation. Profiling adds overhead. For candidate comparisons, keep the same snapshot or handle and loaded environment, repeat the comparison, and check the candidate from the document or an ordinary handle with profiling disabled before treating a speed difference as an optimization. diff --git a/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean b/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean index 1a37c370..1d3e4519 100644 --- a/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean +++ b/tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean @@ -42,6 +42,46 @@ private def hasCategory (profile : Beam.LSP.RunAt.Profile.Result) (category : St private def awaitResult (request : ReqHandle) : ScenarioM Beam.LSP.RunAt.Result := awaitResponseAs request +/-- Oversubscribed profiles must preserve later costly work, deterministic ties and ancestry. -/ +def checkRetention : IO Unit := do + let forced ← IO.mkRef false + let label := MessageData.ofLazy (fun _ => do + forced.set true + pure <| Dynamic.mk (m!"unused")) (fun _ => false) + let timed := fun cls start stop children => MessageData.trace + { cls, startTime := start, stopTime := stop } label children + let small := (Array.range (Beam.LSP.RunAt.Profile.maxSpans + 20)).map fun i => + MessageData.trace {cls := `small, tag := toString i, startTime := 1.1, stopTime := 1.18} label #[] + -- An asynchronous child's inclusive interval can outlast the enclosing scope. + let family := timed `parent 1.1 1.12 #[timed `largeChild 1.1 1.9 #[]] + let root := timed `body 1.0 1.95 (small.push family) + let traces := ({} : PersistentArray TraceElem).push {ref := .missing, msg := root} + let late := ({} : PersistentArray TraceElem).push {ref := .missing, msg := timed `Kernel 1.7 1.95 #[]} + let result := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 + #[{tid := 1, traces}, {tid := 2, traces := late}] "" + require (result.truncated && result.spans.size == Beam.LSP.RunAt.Profile.maxSpans) + "retention must respect the output cap and report omitted timed nodes" + require (result.spans.any (·.category == "Kernel")) "late large root was starved" + let some child := result.spans.find? (·.category == "largeChild") + | throw <| IO.userError "large child was lost" + let some parent := child.parent? | throw <| IO.userError "ancestor closure lost parent" + require (result.spans[parent]!.category == "parent") "child was reparented incorrectly" + let ties := result.spans.filter (·.category == "small") + require (ties.map (·.tag) == (Array.range ties.size).map toString) + "equal-duration retention must follow original order" + for i in [:result.spans.size] do + if let some parent := result.spans[i]!.parent? then + require (parent < i && result.spans[parent]!.thread == result.spans[i]!.thread) + "retention broke parent order or thread identity" + let wide := timed `body 1.0 1.95 + (Array.replicate (Beam.LSP.RunAt.Profile.maxVisited + 1) (m!"untimed")) + let exhausted := Beam.LSP.RunAt.Profile.collect 1000000000 2000000000 + #[{tid := 1, traces := ({} : PersistentArray TraceElem).push {ref := .missing, msg := wide}}, + {tid := 2, traces := late}] "" + require (exhausted.truncated && exhausted.spans.any (·.category == "Kernel")) + "visit exhaustion must remain truthful after reaching late roots" + require (!(← forced.get)) "retention evaluated a lazy header" + def checkProjection : IO Unit := do let forced ← IO.mkRef false let label := MessageData.ofLazy (fun _ => do @@ -388,6 +428,7 @@ def checkCancellationAndStaleness : ScenarioM Unit := do def run : ScenarioM Unit := do checkProjection + checkRetention ProfileContractsTest.run ProfileSummaryTest.run checkProofs From 13641ddf936d2f8b7e0d298aa68925677a0b7305 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Nov 2026 05:13:19 -0800 Subject: [PATCH 2/4] docs: describe profiling retention coverage --- CHANGELOG.md | 7 +++++++ docs/TESTING.md | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index df5c8d47..718c8cba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,13 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ## Unreleased +### Fixed + +- Retain significant speculative profiling spans across the visited trace forest instead of + filling the response from its first subtree. Shallow-first traversal and duration-ranked + ancestor closure preserve later costly work within bounded traversal and output budgets + ([#420](https://github.com/leanprover/lean-beam/pull/420), @ejgallego). + ### Added - Add inclusive summaries and Lean trace labels to CLI/MCP speculative profiling results. diff --git a/docs/TESTING.md b/docs/TESTING.md index ef4c613b..8aa89169 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -98,7 +98,7 @@ Current LSP coverage includes: - full registered LSP request coverage through request-family tests under [tests/lean/BeamTest/LSP/Requests](../tests/lean/BeamTest/LSP/Requests), aggregated by [tests/lean/BeamTest/LSP/RequestSurfaceTest.lean](../tests/lean/BeamTest/LSP/RequestSurfaceTest.lean), including `$/lean/todo` and `$/lean/runAt` composition; the agent corpus [tests/save_olean_project/TodoAgentSmoke.lean](../tests/save_olean_project/TodoAgentSmoke.lean) pins one whole-file `todo` item per common proof mistake, with its goal, and a `runAt` solution for each at the item's position, including term placeholders and a handle continued from one - tactic-sequence parsing in [RunAt/BasicTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean): newline- and `;`-separated tactics, comments and nested bullets, more-indented argument continuation, a line break that must end `intro`'s binders instead of naming one after the next tactic, the same text through a `runWith` continuation, rollback of a continuation whose second tactic fails (no successor handle; a non-linear parent stays reusable, a linear parent is consumed), and a clear error for comment-only text - placeholder probes in the same file: tactics at an unfilled `sorry`, `_`, or `?x` term run against its goal, with its local context and instances, from its first character through its end, inside a tactic proof as well; a hole that elaboration filled keeps the command basis, and a `?_` whose goal a later tactic solved or closed with `sorry` keeps the tactic basis; a stored handle continues goals the tactics leave; placeholder contexts with `let` values, local instances, open namespaces, local notation, and section or header universes; a local introduced by one probe visible only through its stored handle, also across concurrent probes; handles stored at a placeholder invalidated by an edit; and the documented self-reference limitation (a probe may use the declaration being proved, while later declarations stay unknown) -- opt-in profiling in [ProfileTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean): timed tactic and asynchronous command execution, failure evidence before rollback, placeholder and handle continuation, concurrent trace isolation, cancellation and edits, bounded non-rendering trace projection, filtering heartbeat-clock nodes using recorded options, source-level profiler overrides, documented/attributed declaration boundaries, and restoration of visible profiler options. [ProfileContractsTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileContractsTest.lean) covers direct, scoped and macro-expanded trace assertions, unexecuted quoted syntax, deferred realization, mandatory profiling on successor handles, and rejected linear calls preserving their handles. [ProfileSummaryTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileSummaryTest.lean) checks inclusive path ranking, selection of substantial inner members past wrappers but before tiny leaves, the half-duration boundary and zero-duration cases, branching and partial trees, separate collapsed/omitted counts including undisplayed tails, observed phases, selected headers rendered once with their context, output capture and Unicode clipping without marking the projection truncated, unchanged timing, and cancellation between formatters. The resource-limit cases in `RunAt/BasicTest.lean` also cover profiled direct probes and both handle continuation modes +- opt-in profiling in [ProfileTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileTest.lean): timed tactic and asynchronous command execution, failure evidence before rollback, placeholder and handle continuation, concurrent trace isolation, cancellation and edits, bounded non-rendering trace projection, late roots after early fine-grained work, duration retention with ancestor closure and stable ties, visit exhaustion, filtering heartbeat-clock nodes using recorded options, source-level profiler overrides, documented/attributed declaration boundaries, and restoration of visible profiler options. [ProfileContractsTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileContractsTest.lean) covers direct, scoped and macro-expanded trace assertions, unexecuted quoted syntax, deferred realization, mandatory profiling on successor handles, and rejected linear calls preserving their handles. [ProfileSummaryTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/ProfileSummaryTest.lean) checks inclusive path ranking, selection of substantial inner members past wrappers but before tiny leaves, the half-duration boundary and zero-duration cases, branching and partial trees, separate collapsed/omitted counts including undisplayed tails, observed phases, selected headers rendered once with their context, output capture and Unicode clipping without marking the projection truncated, unchanged timing, and cancellation between formatters. The resource-limit cases in `RunAt/BasicTest.lean` also cover profiled direct probes and both handle continuation modes - auxiliary-declaration conformance in [AuxiliaryDeclarationTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/AuxiliaryDeclarationTest.lean), comparing `runAt` with identical tactic replacements through ordinary LSP document edits, including private and nested proofs, stored-handle branches, and failure isolation - proof-context combinations in the same fixture: universe-polymorphic kernel `decide` and `grind`, rollback within `first`, local instances and dependent induction across handle branches, native computation, `conv` under binders, and bitvector solver success and counterexamples - available-goal execution in [AvailabilityTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/AvailabilityTest.lean): a later tactic signals entry and waits on a gate; goal inspection and `runAt` must finish before that gate is released, with both synchronous and asynchronous elaboration From a13d97fd7e6531f8ca7cd039cd03724070c7e6b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Nov 2026 06:21:15 -0800 Subject: [PATCH 3/4] fix: bound retained profiling spans to 192 --- Beam/LSP/RunAt/Profile.lean | 2 +- docs/MCP.md | 2 +- skills/lean-beam/references/workflow-details.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Beam/LSP/RunAt/Profile.lean b/Beam/LSP/RunAt/Profile.lean index ee93abaf..f6268a39 100644 --- a/Beam/LSP/RunAt/Profile.lean +++ b/Beam/LSP/RunAt/Profile.lean @@ -35,7 +35,7 @@ structure Result where deriving FromJson, ToJson def initialThresholdMs : Nat := 1 -def maxSpans : Nat := 1024 +def maxSpans : Nat := 192 def maxVisited : Nat := 16384 def maxDepth : Nat := 256 def maxTopSpans : Nat := 10 diff --git a/docs/MCP.md b/docs/MCP.md index e3dc5135..fe5d137f 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -475,7 +475,7 @@ UTF-16 character offsets; its end is exclusive. A range is not a document coordi that Lean can map the span to a source occurrence. If the source snippet exceeds 8192 UTF-8 bytes, Beam omits span ranges. -Profiling returns at most 1024 spans, limits traversal visits to 16384 (including trace-state entries), +Profiling returns at most 192 spans, limits traversal visits to 16384 (including trace-state entries), and limits `MessageData` nesting to 256. Traversal considers roots and shallow message nodes before deeper descendants. Among visited timed nodes, retention ranks inclusive duration, breaking ties by original trace-tree order. A node is admitted with all its timed ancestors only when the group fits diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 48e02f4a..60947d37 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -160,7 +160,7 @@ a document position or a guaranteed mapping to a source occurrence. If the sourc Profiled results retain ordinary warnings and errors, but suppress ordinary Lean trace text from both `messages` and `traces`; `traces` is `[]`. Each continuation profile measures only that call, not earlier work represented by its handle. Nested and parallel spans overlap, so do not sum their -durations. The profile has at most 1024 spans, 16384 traversal visits (including trace-state entries), +durations. The profile has at most 192 spans, 16384 traversal visits (including trace-state entries), and `MessageData` nesting depth 256. Shallow nodes are visited before deep descendants; retained spans are chosen by inclusive duration with their ancestors, then returned in original tree order. This favors significant work across the visited forest, but neither complete traversal nor retention From f8a33b9bc8a25c0ecf684ec7efac0231b18c9e42 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Nov 2026 09:52:40 -0800 Subject: [PATCH 4/4] fix: cap speculative profiles at 128 retained spans --- Beam/LSP/RunAt/Profile.lean | 2 +- docs/MCP.md | 2 +- skills/lean-beam/references/workflow-details.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Beam/LSP/RunAt/Profile.lean b/Beam/LSP/RunAt/Profile.lean index f6268a39..4db860d2 100644 --- a/Beam/LSP/RunAt/Profile.lean +++ b/Beam/LSP/RunAt/Profile.lean @@ -35,7 +35,7 @@ structure Result where deriving FromJson, ToJson def initialThresholdMs : Nat := 1 -def maxSpans : Nat := 192 +def maxSpans : Nat := 128 def maxVisited : Nat := 16384 def maxDepth : Nat := 256 def maxTopSpans : Nat := 10 diff --git a/docs/MCP.md b/docs/MCP.md index fe5d137f..dfe57e31 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -475,7 +475,7 @@ UTF-16 character offsets; its end is exclusive. A range is not a document coordi that Lean can map the span to a source occurrence. If the source snippet exceeds 8192 UTF-8 bytes, Beam omits span ranges. -Profiling returns at most 192 spans, limits traversal visits to 16384 (including trace-state entries), +Profiling returns at most 128 spans, limits traversal visits to 16384 (including trace-state entries), and limits `MessageData` nesting to 256. Traversal considers roots and shallow message nodes before deeper descendants. Among visited timed nodes, retention ranks inclusive duration, breaking ties by original trace-tree order. A node is admitted with all its timed ancestors only when the group fits diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 60947d37..615141c6 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -160,7 +160,7 @@ a document position or a guaranteed mapping to a source occurrence. If the sourc Profiled results retain ordinary warnings and errors, but suppress ordinary Lean trace text from both `messages` and `traces`; `traces` is `[]`. Each continuation profile measures only that call, not earlier work represented by its handle. Nested and parallel spans overlap, so do not sum their -durations. The profile has at most 192 spans, 16384 traversal visits (including trace-state entries), +durations. The profile has at most 128 spans, 16384 traversal visits (including trace-state entries), and `MessageData` nesting depth 256. Shallow nodes are visited before deep descendants; retained spans are chosen by inclusive duration with their ancestors, then returned in original tree order. This favors significant work across the visited forest, but neither complete traversal nor retention