Skip to content

feat: guard_msgs to treat trace messages separate#8267

Merged
nomeata merged 8 commits intomasterfrom
joachim/guard-msgs-trace
May 9, 2025
Merged

feat: guard_msgs to treat trace messages separate#8267
nomeata merged 8 commits intomasterfrom
joachim/guard-msgs-trace

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented May 8, 2025 •
edited
Loading

This PR makes #guard_msgs to treat trace messages separate from info, warning and error. It also introduce the ability to say #guard_msgs (pass info, like (drop info) so far, and also adds (check info) as the explicit form of (info), for completeness.

Fixes #8266

@nomeata
feat: guard_msgs to treat trace messages separate
f1fd9d5 
This PR makes `#guard_msgs` to treat trace messages separte from `info`,
`warning` and `error`, and pass them through by default.

Fixes #8266
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented May 8, 2025

A bunch more of tests to update, though.

@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 May 8, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 8, 2025
Update lean-toolchain for testing leanprover/lean4#8267
5fc240f
@nomeata nomeata marked this pull request as ready for review May 8, 2025 15:59
@nomeata nomeata requested a review from digama0 as a code owner May 8, 2025 15:59
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2025
Update lean-toolchain for testing leanprover/lean4#8267
2dd059c
@nomeata nomeata added the changelog-language Language features and metaprograms label May 8, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 8, 2025
Trigger CI for leanprover/lean4#8267
832da7a
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2025
Trigger CI for leanprover/lean4#8267
796f910
@ghost
Copy link
Copy Markdown

ghost commented May 8, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 8, 2025
@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented May 8, 2025

Looking at the test results, we might want to exclude the trace_state tactic from this change? It seems like trace_state is mostly used for these kind of tests so it doesn't make too much sense to remove them from the #guard_msgs log.

@Rob23oba
Copy link
Copy Markdown
Contributor

Rob23oba commented May 8, 2025

Also, maybe add a note to the #guard_msgs error message that traces are now omitted by default and that one should use #guard_msgs (all) if they want traces to be captured.

@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented May 8, 2025

I've been wondering if trace_state should actually be an info, like #check. But maybe let's not let this get this out of hand here, and avoid confusing special cases.

@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented May 8, 2025

Ok, I’ll make this less invasive and leave the default at all, merely extracting the trace category.

ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 8, 2025
Trigger CI for leanprover/lean4#8267
71386da
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 8, 2025
Trigger CI for leanprover/lean4#8267
1cea329
@nomeata nomeata enabled auto-merge May 9, 2025 05:44
@nomeata nomeata added this pull request to the merge queue May 9, 2025
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 9, 2025
Merged via the queue into master with commit 0e49576 May 9, 2025
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms 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.

RFC: guard_msgs to pass trace messages by default

2 participants

@nomeata @Rob23oba