Skip to content

fix: indent nested traces correctly#6345

Closed
eric-wieser wants to merge 1 commit intoleanprover:masterfrom
eric-wieser:patch-30
Closed

fix: indent nested traces correctly#6345
eric-wieser wants to merge 1 commit intoleanprover:masterfrom
eric-wieser:patch-30

Conversation

@eric-wieser
Copy link
Copy Markdown
Contributor

@eric-wieser eric-wieser commented Dec 9, 2024

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>

@eric-wieser
fix: indent nested traces correctly
926a76e 
Presumably this worked before due to extra `.group` nodes appearing. I think `group`s 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.
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 9, 2024
@ghost
Copy link
Copy Markdown

ghost commented Dec 9, 2024

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
Copy link
Copy Markdown
Collaborator

nomeata commented Dec 9, 2024

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
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 9, 2024 

#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
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 9, 2024 •
edited
Loading

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 eric-wieser mentioned this pull request Dec 10, 2024
Closed
@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 15, 2024

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

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 11, 2025
@eric-wieser
feat: use scoped trace nodes in linarith (#19855)
3a798ee 
Inspired by hacking done with @robertylewis and @hrmacbeth which resulted in #19771.

The effect is that the traces messages are now hierarchical; though it's easy not to notice in VSCode without a better version of leanprover/lean4#6345.

See https://profiler.firefox.com/public/smkc5ffh9318w177gps2x9e5b6wy117s6f18e6g/flame-graph/?globalTrackOrder=0&thread=0&transforms=ff-2659&v=10 for an example output produced with
```bash
lake lean MathlibTest/linarith.lean -- \
  -Dtrace.profiler=true \
  -Dtrace.profiler.threshold=1 \
  -Dtrace.profiler.output.pp=true \
  -Dtrace.profiler.output=linarith-profile.json
```

Some inconclusive discussion about best practices for `withTraceNode` is [on Zulip here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20withTraceNode/near/489198580).



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@eric-wieser @nomeata