feat: trace postprocessors - #14352
Merged
Merged
Conversation
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 10, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 10, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 10, 2026
Contributor
Author
|
!radar |
|
Benchmark results for d2a15cd against da19ea0 are in. There are significant results. @datokrat Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (3✅)
Small changes (1✅)
|
This PR adds trace postprocessors: functions that transform the trace messages of a command before they are reported, e.g. by filtering out irrelevant subtrees, focusing on a single trace class, or pre-expanding the paths to failures. The new `trace_view post in cmd` command applies a postprocessor to the traces of `cmd`, and `store_trace_as t in cmd` stores the traces of a slow command so they can be inspected with `#trace_roots t` and re-rendered with `#trace_view t post` without re-running `cmd`. Postprocessors have type `Lean.TraceView.TracePostprocessor` (`Array TraceTree → CoreM (Array TraceTree)`, applied to the trace roots of each trace message); they can be composed with `>=>` and defined by users as ordinary functions. The `Lean.TraceView` namespace provides basic combinators: `focusOn`, `hideSucceeded`, `maxDepth`, `minTimeMs`, `grep`, `expandAll`, `collapseAll`, `expandFailures`, `onRoots`, `onClass`, and `onRootIdx`. `TraceTree` is a structured view of trace `MessageData` that handles the context wrappers around trace nodes. Stored traces live in a non-persistent environment extension and are not exported to `.olean` files. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ew` at its own range This PR makes `store_trace_as t in cmd` add an actual declaration `t : CoreM Lean.TraceView.StoredTrace` to the environment, so the stored trace can be inspected by arbitrary metaprograms, e.g. `#eval do return (← t).roots.size` or `(← t).postprocess (focusOn `cls)`. Stored trace names now live in the current namespace and resolve like any other constant. The output of `#trace_view t post` is now anchored at the `#trace_view` command itself rather than at the source range of the traced command; the original positions remain inspectable via `#trace_roots t`. The declaration body merely references the trace data via `Lean.TraceView.findStoredTrace`, which reads it from the in-memory environment extension at evaluation time. Declaring a stored trace is therefore O(1) regardless of trace size: no serialization, no embedding of the trace in the declaration value, and no kernel checking of large terms. The data itself consists of the already materialized in-memory trace messages, shared rather than copied. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This PR adds the `expandMatches pat` trace postprocessor: it expands all transitive parents of the trace nodes whose trace class or head message contains `pat` as a substring, so that the trace opens in the editor already showing all matches. Unlike `grep`, no nodes are removed, and all other nodes — including the matches themselves — keep their expansion state. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
!radar |
|
Benchmark results for 434109f against 12c859a are in. No significant results found. @datokrat
Medium changes (1🟥)
Small changes (2✅)
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 14, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 14, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 14, 2026
mathlib-lean-pr-testing
Bot
added
breaks-mathlib
Contributor
Author
|
!radar |
|
Benchmark results for 5b7031b against 12c859a are in. There are significant results. @datokrat
Large changes (1🟥)
Small changes (1✅, 1🟥)
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 14, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 14, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 14, 2026
datokrat
marked this pull request as ready for review
July 14, 2026 12:11
pull Bot
pushed a commit
to DaviRain-Su/lean4
that referenced
this pull request
Jul 15, 2026
leanprover#14386) This PR is a follow-up to leanprover#14352 (introducing `postprocess_traces`). It provides a new command `store_traces_as myTraces in cmd` that runs the command `cmd` and stores its traces in-memory under the name `name`. The stored traces can be transformed and viewed using `#postprocess_traces tracePostprocessor myTraces`.
robsimmons
pushed a commit
that referenced
this pull request
Jul 29, 2026
#14386) This PR is a follow-up to #14352 (introducing `postprocess_traces`). It provides a new command `store_traces_as myTraces in cmd` that runs the command `cmd` and stores its traces in-memory under the name `name`. The stored traces can be transformed and viewed using `#postprocess_traces tracePostprocessor myTraces`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR provides the experimental
postprocess_traces tracePostprocessor in cmdcommand, which is useful for working with large trees of trace nodes. It runs the commandcmdand then transforms the traces using a functiontracePostprocessor. The transformation can affect which nodes are expanded or collaped by default, it can change messages of the trace nodes, and it can add or delete nodes.Example: