fix: omit repeated inner labels from profile summaries

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 [

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,

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

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.

tests/lean/BeamTest/Broker/McpProjectionTest.lean

@@ -831,6 +831,7 @@ 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
+
   let emptyProfile := Beam.Broker.Response.success <| toJson ({
     profile? := some { elapsedMs := 0 }
   } : Beam.LSP.RunAt.Result)
@@ -922,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) := #[
@@ -1942,6 +1998,7 @@ def main : IO Unit := do
   checkRunAtNormalization
   checkSyncAndSaveNormalization
   checkCrossSurfaceResultParity
+  checkProfileLabelOmission
   checkCrossSurfaceErrorParity
   checkBrokerFailureCodeCompleteness
   checkSaveImportsChangedProjection