Repository navigation
doc: describe how to profile mergeWithGrind suggestions - #1169
Open
arademaker wants to merge 1 commit into
Open
arademaker wants to merge 1 commit into
arademaker wants to merge 1 commit into
Conversation
Add a section to CONTRIBUTING.md asking contributors who accept `mergeWithGrind` suggestions from the weekly linters to report the change in elaboration time per-declaration in the PR description, following Mathlib's practice (e.g. leanprover-community/mathlib4#36764). Explain how to measure it with `trace.profiler` and how to read the resulting trace. AI disclaim: Claude Opus 5.5 was used to validate the commands and draft the new section.
arademaker
requested review from
SamuelSchlesinger,
chenson2018,
crei,
fmontesi and
sorrachai
as code owners
October 28, 2026 00:27
There was a problem hiding this comment.
🟢 Approval recommended
No active review issues are recorded for the contributor profiling documentation update.
No open issues 🎉
What changed in this PR
Documents how CSLib contributors should measure and report elaboration-time changes when accepting weekly mergeWithGrind suggestions.
Changes:
- Adds profiling instructions using
Elab.async falseandtrace.profiler, with guidance on interpreting the output. - Provides an example PR-description format for per-declaration timing results, following Mathlib’s practice.
| File | Description |
|---|---|
| CONTRIBUTING.md | Adds weekly-linter profiling guidance and a table-of-contents link. |
Review effort: Balanced
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
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.
Add a section to CONTRIBUTING.md asking contributors who accept
mergeWithGrindsuggestions from the weekly linters to report the change in elaboration time per declaration in the PR description, following Mathlib's practice (e.g., leanprover-community/mathlib4#36764). Explain how to measure it withtrace.profilerand how to read the resulting trace.I'm documenting the suggestion made by @chenson2018 here.
AI disclaimer: Claude Opus 5.5 validated the commands and drafted the new section.