From bcfca4eab63cda88573aa06b4b1fb5cc27fd7e53 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 5 Nov 2026 18:43:57 -0800 Subject: [PATCH 1/3] fix: omit repeated inner labels from profile summaries --- Beam/Output.lean | 14 +++-- docs/MCP.md | 5 +- .../lean-beam/references/workflow-details.md | 4 +- .../BeamTest/Broker/McpProjectionTest.lean | 52 +++++++++++++++++++ 4 files changed, 68 insertions(+), 7 deletions(-) diff --git a/Beam/Output.lean b/Beam/Output.lean index 31210170..b1b247d5 100644 --- a/Beam/Output.lean +++ b/Beam/Output.lean @@ -151,15 +151,19 @@ private def profileJson (profile : Beam.LSP.RunAt.Profile.Result) : Json := Id.r -- Selection depends only on the unchanged span forest and timings, never rendered labels. -- Reusing the pure selector avoids storing a second, potentially stale summary in Result. let selection := Beam.LSP.RunAt.Profile.select profile.spans - let fields := fun index => + let fields := fun index (outerLabel? : Option String) => let span := profile.spans[index]! [("span", toJson index), ("category", toJson span.category), ("duration_ms", toJson span.durationMs)] ++ (if span.tag.isEmpty then [] else [("tag", toJson span.tag)]) ++ - (match span.label? with | some label => [("label", toJson label)] | none => []) - let entry := fun index => Json.mkObj (fields index) - let chainEntry := fun (chain : Beam.LSP.RunAt.Profile.Chain) => Json.mkObj <| fields chain.outer ++ - if chain.inner == chain.outer then [] else [("inner_span", entry chain.inner)] + (match span.label? with + | some label => if outerLabel? == some label then [] else [("label", toJson label)] + | none => []) + let entry := fun index => Json.mkObj (fields index none) + let chainEntry := fun (chain : Beam.LSP.RunAt.Profile.Chain) => Json.mkObj <| fields chain.outer none ++ + -- Equal displayed text (possibly clipped) does not make the two measurements equivalent. + if chain.inner == chain.outer then [] else + [("inner_span", Json.mkObj <| fields chain.inner profile.spans[chain.outer]!.label?)] return Json.mkObj [ ("elapsed_ms", toJson profile.elapsedMs), ("initial_threshold_ms", toJson profile.initialThresholdMs), ("summary", Json.mkObj [ diff --git a/docs/MCP.md b/docs/MCP.md index 277ddb58..050c6b43 100644 --- a/docs/MCP.md +++ b/docs/MCP.md @@ -426,7 +426,10 @@ Start with `elapsed_ms` and `summary`: `Elab.def.maxSharing`, `addDecl`, `Elab.definition.value` and `Elab.lint`, in that order. These are individual observations, not phase totals. Missing categories are omitted, never reported as zero. - Each entry has `span` (its zero-based index in `profile.spans`), `category`, and `duration_ms`. - Nonempty `tag` and available `label` are included. The same index can appear in both views; + Nonempty `tag` and available `label` are included, except that an `inner_span.label` identical + to its outer entry's displayed label is omitted. The inner span's index, tag and own duration + remain: equal text, including equal clipped previews, does not establish equivalent operations. + The same index can appear in both views; it is the same observation and its label is rendered once. - `collapsed_spans` counts members of the shown paths that do not get separate top-level entries, including tails beyond the displayed inner members. `omitted_from_top` counts retained spans in paths outside the diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 7171485e..6c775524 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -123,12 +123,14 @@ theorem demo_add_zero (n : Nat) : n + 0 = n := by Inspect `success` and ordinary warnings/errors first, then `profile.elapsed_ms` and `profile.summary`. `summary.top_spans` groups retained single-child paths and ranks up to ten by outer inclusive duration. Optional `inner_span` gives the deepest member retaining at least half the positive outer -duration, with its own index, duration and label; it is omitted if no descendant qualifies. This +duration, with its own index, duration and available label; it is omitted if no descendant qualifies. This display heuristic does not identify a cause or guarantee a tactic node. The entire path remains grouped, including any smaller tail; the outer duration is not the inner step's cost. `summary.phase_spans` shows the largest observed span for each known declaration-phase category, not totals or zeros for missing phases. Entries have `span` indices into `profile.spans`, plus category, duration and available Lean-rendered labels. An entry in both views is the same observation. +An inner label identical to its outer entry's displayed label is omitted; the inner index, tag +and own duration remain. Equal labels, including clipped previews, do not imply equivalent operations. `summary.collapsed_spans` counts members folded into shown top entries; `summary.omitted_from_top` counts retained spans in paths outside the top list. Together with the top entry count they equal the raw span count; neither counts unrecorded work. diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean index d6221442..a9825ac5 100644 --- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean +++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean @@ -831,6 +831,58 @@ private def checkCrossSurfaceResultParity : IO Unit := do requireFieldAbsent "phase is an individual observation" "inner_span" phases[0]! requireJsonInt "all descendants collapsed, including the undisplayed tail" "collapsed_spans" 2 summary requireJsonInt "all retained spans shown" "omitted_from_top" 0 summary + + -- Repeated display text is noise, but distinct indices, tags and costs remain evidence. + -- Equal clipped previews in particular do not establish equivalent underlying operations. + let clippedLabel := ("".pushn 'λ' 159) ++ "…" + let labelCases : Array (Option String × Option String × Option String) := #[ + (some "grind", some "grind", none), + (some clippedLabel, some clippedLabel, none), + (some "simp", some "grind", some "grind"), + (none, some "grind", some "grind"), + (some "grind", none, none), + (none, none, none)] + for (outerLabel?, innerLabel?, expectedInnerLabel?) in labelCases do + let response := Beam.Broker.Response.success <| toJson ({ + profile? := some { elapsedMs := 130, spans := #[ + { thread := 0, category := "Elab.step", tag := "Lean.Parser.Tactic.tacticSeq", + startMs := 0, durationMs := 100, label? := outerLabel? }, + { thread := 0, parent? := some 0, category := "Elab.step", tag := "Lean.Parser.Tactic.grind", + startMs := 10, durationMs := 60, label? := innerLabel? }, + { thread := 0, category := "Kernel", tag := "", startMs := 100, durationMs := 30, + label? := some "grind" }] } + } : Beam.LSP.RunAt.Result) + let mcp ← expectToolOk "MCP profile label omission" <| + Beam.Mcp.normalizeBrokerResponse (.leanOperation .runAt) response + let cliEnvelope ← expectToolOk "CLI profile label omission" <| + (Beam.Cli.prepareOperationResponse (.broker .runAt) response).map (·.json) + let cli ← requireObjVal "CLI label omission envelope" "result" cliEnvelope + require "CLI/MCP profile label omission parity" (cli == mcp) + let p ← requireObjVal "label omission result" "profile" cli + let s ← requireObjVal "label omission profile" "summary" p + let tops ← IO.ofExcept <| s.getObjValAs? (Array Json) "top_spans" + let phaseEntries ← IO.ofExcept <| s.getObjValAs? (Array Json) "phase_spans" + let child ← requireObjVal "distinct inner measurement retained" "inner_span" tops[0]! + match outerLabel? with + | some label => requireJsonString "outer label retained" "label" label tops[0]! + | none => requireFieldAbsent "missing outer label not invented" "label" tops[0]! + match expectedInnerLabel? with + | some label => requireJsonString "distinct or only available inner label retained" "label" label child + | none => requireFieldAbsent "repeated or unavailable inner label omitted" "label" child + requireJsonInt "distinct inner index retained" "span" 1 child + requireJsonString "distinct inner tag retained" "tag" "Lean.Parser.Tactic.grind" child + require "distinct inner duration retained" ((← requireObjVal "inner" "duration_ms" child) == toJson (60 : Float)) + require "outer duration retained" ((← requireObjVal "outer" "duration_ms" tops[0]!) == toJson (100 : Float)) + require "independent phase keeps its label in both views" (phaseEntries[0]! == tops[1]!) + requireJsonString "independent phase label retained" "label" "grind" phaseEntries[0]! + requireJsonInt "label omission does not alter grouping" "collapsed_spans" 1 s + requireJsonInt "label omission does not alter retained omissions" "omitted_from_top" 0 s + requireJsonBool "label omission does not truncate evidence" "truncated" false p + let raw ← IO.ofExcept <| p.getObjValAs? (Array Json) "spans" + require "raw spans retained" (raw.size == 3) + requireJsonInt "raw parent retained" "parent" 0 raw[1]! + require "raw inner duration retained" ((← requireObjVal "raw inner" "duration_ms" raw[1]!) == toJson (60 : Float)) + let emptyProfile := Beam.Broker.Response.success <| toJson ({ profile? := some { elapsedMs := 0 } } : Beam.LSP.RunAt.Result) From ffc15f7825ade83daee1b534bf35eaad77ef6708 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 5 Nov 2026 18:44:30 -0800 Subject: [PATCH 2/3] docs: record profile label deduplication --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index df5c8d47..50bfb9e8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -23,6 +23,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ### Fixed +- Omit an inner profile label when it repeats the outer entry's displayed text on CLI/MCP. + The inner span keeps its distinct index, tag and duration, including when clipped previews coincide + ([#419](https://github.com/leanprover/lean-beam/pull/419), @ejgallego). - `save` refusals that suggest `lake build` (`saveUnsupportedSetup`, `saveTraceStale`) and the deferred-compilation readiness message in `sync` now say to stop the CLI owner or drop the MCP workspace and confirm cleanup before building, then start a fresh session. Building while the session was live left dependencies marked as needing a save, From 6840d5125147656c68ec32ecf1dcd70a9d9b96ae Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 6 Nov 2026 05:39:35 -0800 Subject: [PATCH 3/3] test: isolate profile label omission cases --- .../BeamTest/Broker/McpProjectionTest.lean | 107 +++++++++--------- 1 file changed, 56 insertions(+), 51 deletions(-) diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean index a9825ac5..7e727ad4 100644 --- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean +++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean @@ -832,57 +832,6 @@ private def checkCrossSurfaceResultParity : IO Unit := do requireJsonInt "all descendants collapsed, including the undisplayed tail" "collapsed_spans" 2 summary requireJsonInt "all retained spans shown" "omitted_from_top" 0 summary - -- Repeated display text is noise, but distinct indices, tags and costs remain evidence. - -- Equal clipped previews in particular do not establish equivalent underlying operations. - let clippedLabel := ("".pushn 'λ' 159) ++ "…" - let labelCases : Array (Option String × Option String × Option String) := #[ - (some "grind", some "grind", none), - (some clippedLabel, some clippedLabel, none), - (some "simp", some "grind", some "grind"), - (none, some "grind", some "grind"), - (some "grind", none, none), - (none, none, none)] - for (outerLabel?, innerLabel?, expectedInnerLabel?) in labelCases do - let response := Beam.Broker.Response.success <| toJson ({ - profile? := some { elapsedMs := 130, spans := #[ - { thread := 0, category := "Elab.step", tag := "Lean.Parser.Tactic.tacticSeq", - startMs := 0, durationMs := 100, label? := outerLabel? }, - { thread := 0, parent? := some 0, category := "Elab.step", tag := "Lean.Parser.Tactic.grind", - startMs := 10, durationMs := 60, label? := innerLabel? }, - { thread := 0, category := "Kernel", tag := "", startMs := 100, durationMs := 30, - label? := some "grind" }] } - } : Beam.LSP.RunAt.Result) - let mcp ← expectToolOk "MCP profile label omission" <| - Beam.Mcp.normalizeBrokerResponse (.leanOperation .runAt) response - let cliEnvelope ← expectToolOk "CLI profile label omission" <| - (Beam.Cli.prepareOperationResponse (.broker .runAt) response).map (·.json) - let cli ← requireObjVal "CLI label omission envelope" "result" cliEnvelope - require "CLI/MCP profile label omission parity" (cli == mcp) - let p ← requireObjVal "label omission result" "profile" cli - let s ← requireObjVal "label omission profile" "summary" p - let tops ← IO.ofExcept <| s.getObjValAs? (Array Json) "top_spans" - let phaseEntries ← IO.ofExcept <| s.getObjValAs? (Array Json) "phase_spans" - let child ← requireObjVal "distinct inner measurement retained" "inner_span" tops[0]! - match outerLabel? with - | some label => requireJsonString "outer label retained" "label" label tops[0]! - | none => requireFieldAbsent "missing outer label not invented" "label" tops[0]! - match expectedInnerLabel? with - | some label => requireJsonString "distinct or only available inner label retained" "label" label child - | none => requireFieldAbsent "repeated or unavailable inner label omitted" "label" child - requireJsonInt "distinct inner index retained" "span" 1 child - requireJsonString "distinct inner tag retained" "tag" "Lean.Parser.Tactic.grind" child - require "distinct inner duration retained" ((← requireObjVal "inner" "duration_ms" child) == toJson (60 : Float)) - require "outer duration retained" ((← requireObjVal "outer" "duration_ms" tops[0]!) == toJson (100 : Float)) - require "independent phase keeps its label in both views" (phaseEntries[0]! == tops[1]!) - requireJsonString "independent phase label retained" "label" "grind" phaseEntries[0]! - requireJsonInt "label omission does not alter grouping" "collapsed_spans" 1 s - requireJsonInt "label omission does not alter retained omissions" "omitted_from_top" 0 s - requireJsonBool "label omission does not truncate evidence" "truncated" false p - let raw ← IO.ofExcept <| p.getObjValAs? (Array Json) "spans" - require "raw spans retained" (raw.size == 3) - requireJsonInt "raw parent retained" "parent" 0 raw[1]! - require "raw inner duration retained" ((← requireObjVal "raw inner" "duration_ms" raw[1]!) == toJson (60 : Float)) - let emptyProfile := Beam.Broker.Response.success <| toJson ({ profile? := some { elapsedMs := 0 } } : Beam.LSP.RunAt.Result) @@ -974,6 +923,61 @@ private def checkCrossSurfaceResultParity : IO Unit := do require "array payload is retained without progress" (wrappedPlainArray == #[toJson (8 : Nat)]) requireFieldAbsent "array result without progress" "document_progress" cliPlainArray +private def checkProfileLabelOmission : IO Unit := do + -- Repeated display text is noise, but distinct indices, tags and costs remain evidence. + -- Equal clipped previews in particular do not establish equivalent underlying operations. + let clippedLabel := ("".pushn 'λ' 159) ++ "…" + let labelCases : Array (String × Option String × Option String × Option String) := #[ + ("equal", some "grind", some "grind", none), + ("clipped-equal", some clippedLabel, some clippedLabel, none), + ("different", some "simp", some "grind", some "grind"), + ("missing-outer", none, some "grind", some "grind"), + ("missing-inner", some "grind", none, none), + ("both-missing", none, none, none)] + for (name, outerLabel?, innerLabel?, expectedInnerLabel?) in labelCases do + try + let response := Beam.Broker.Response.success <| toJson ({ + profile? := some { elapsedMs := 130, spans := #[ + { thread := 0, category := "Elab.step", tag := "Lean.Parser.Tactic.tacticSeq", + startMs := 0, durationMs := 100, label? := outerLabel? }, + { thread := 0, parent? := some 0, category := "Elab.step", tag := "Lean.Parser.Tactic.grind", + startMs := 10, durationMs := 60, label? := innerLabel? }, + { thread := 0, category := "Kernel", tag := "", startMs := 100, durationMs := 30, + label? := some "grind" }] } + } : Beam.LSP.RunAt.Result) + let mcp ← expectToolOk "MCP profile label omission" <| + Beam.Mcp.normalizeBrokerResponse (.leanOperation .runAt) response + let cliEnvelope ← expectToolOk "CLI profile label omission" <| + (Beam.Cli.prepareOperationResponse (.broker .runAt) response).map (·.json) + let cli ← requireObjVal "CLI label omission envelope" "result" cliEnvelope + require "CLI/MCP profile label omission parity" (cli == mcp) + let p ← requireObjVal "label omission result" "profile" cli + let s ← requireObjVal "label omission profile" "summary" p + let tops ← IO.ofExcept <| s.getObjValAs? (Array Json) "top_spans" + let phaseEntries ← IO.ofExcept <| s.getObjValAs? (Array Json) "phase_spans" + let child ← requireObjVal "distinct inner measurement retained" "inner_span" tops[0]! + match outerLabel? with + | some label => requireJsonString "outer label retained" "label" label tops[0]! + | none => requireFieldAbsent "missing outer label not invented" "label" tops[0]! + match expectedInnerLabel? with + | some label => requireJsonString "distinct or only available inner label retained" "label" label child + | none => requireFieldAbsent "repeated or unavailable inner label omitted" "label" child + requireJsonInt "distinct inner index retained" "span" 1 child + requireJsonString "distinct inner tag retained" "tag" "Lean.Parser.Tactic.grind" child + require "distinct inner duration retained" ((← requireObjVal "inner" "duration_ms" child) == toJson (60 : Float)) + require "outer duration retained" ((← requireObjVal "outer" "duration_ms" tops[0]!) == toJson (100 : Float)) + require "independent phase keeps its label in both views" (phaseEntries[0]! == tops[1]!) + requireJsonString "independent phase label retained" "label" "grind" phaseEntries[0]! + requireJsonInt "label omission does not alter grouping" "collapsed_spans" 1 s + requireJsonInt "label omission does not alter retained omissions" "omitted_from_top" 0 s + requireJsonBool "label omission does not truncate evidence" "truncated" false p + let raw ← IO.ofExcept <| p.getObjValAs? (Array Json) "spans" + require "raw spans retained" (raw.size == 3) + requireJsonInt "raw parent retained" "parent" 0 raw[1]! + require "raw inner duration retained" ((← requireObjVal "raw inner" "duration_ms" raw[1]!) == toJson (60 : Float)) + catch error => + throw <| IO.userError s!"profile label omission ({name}): {error}" + private def checkProjectionFailureEvidence : IO Unit := do let partialReceipt := Json.mkObj [("module", toJson "Main"), ("sourceHash", toJson "saved")] let cases : Array (Beam.Output.Operation × Beam.Mcp.ToolName × Json) := #[ @@ -1994,6 +1998,7 @@ def main : IO Unit := do checkRunAtNormalization checkSyncAndSaveNormalization checkCrossSurfaceResultParity + checkProfileLabelOmission checkCrossSurfaceErrorParity checkBrokerFailureCodeCompleteness checkSaveImportsChangedProjection