fix: indent nested traces correctly

[eric-wieser]

Presumably this worked before due to extra .group nodes appearing. I think groups should be implied by the children of a trace node.

Not tested as I do not have a working setup for the latest Lean, though there is a test case at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/trace.20nodes.20do.20not.20nest.20correctly.20in.20the.20infoview/near/487028252.

Read this section before submitting

• Ensure your PR follows the External Contribution Guidelines.
• Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
• Include the link to your RFC or bug issue in the description.
• If the issue does not already have approval from a developer, submit the PR as draft.
• The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
• For feat/fix PRs, the first paragraph starting with "This PR" must be present and will become a
  changelog entry unless the PR is labeled with no-changelog. If the PR does not have this label,
  it must instead be categorized with one of the changelog-* labels (which will be done by a
  reviewer for external PRs).
• A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
• If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
• You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
• Remove this section, up to and including the --- before submitting.

---

This PR <short changelog summary for feat/fix, see above>.

Closes <RFC or bug issue number fixed by this PR, if any>

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 520d4b698f3f1f8ed5d673fad6cc810179642279 --onto 3f791933f16d74d74ab8116c96cadec6cdf7b70e. (2024-12-09 16:15:51)

[nomeata]

I have been wondering if it’s just me that the nested traces looked less useful than they could, but maybe it was indeed just broken and needed a simple fix!

Any chance of a test case that covers that? Can #guard_msgs notice the difference?

[eric-wieser]

#eval Lean.logInfo <|
  .trace { cls := `foo } m!"Foo" #[
    .trace { cls := `bar } m!"Bar 1" #[
      .trace { cls := `baz } m!"Baz" #[
        m!"Log message"
      ]
    ],
    .trace { cls := `bar } m!"Bar 2" #[
      m!"Log message"
    ]
  ]

is enough to reproduce the issue, but guard_msgs doesn't spot it.

[eric-wieser]

Maybe the issue is actually at

lean4/src/Lean/Widget/InteractiveDiagnostic.lean

Lines 210 to 215 in ffac974

	let col := col + tt.stripTags.length - 2
	let children ←
	match children with
	| .lazy children => pure <| .lazy ⟨{indent := col+2, children := children.map .mk}⟩
	| .strict children => pure <| .strict (← children.mapM (fmtToTT · (col+2)))
	return .tag (.trace indent cls (← fmtToTT msg col) collapsed children) default

and my patch is garbage.

[eric-wieser]

Closing in favor of #6389, this patch doesn't help.