feat: add benchmarking and profiling infrastructure#6
Closed
kim-em wants to merge 6 commits into
Closed
Conversation
kim-em
force-pushed
the
fix-manifest-path
branch
from
December 3, 2025 03:11
37a4210 to
b64f06d
Compare
kim-em
changed the title
Add comprehensive benchmarking and profiling support for leantar: **New binaries:** - `leantar-benchmark`: Benchmark tool with manifest-based reproducible runs - `--create-manifest <TAG>`: Generate manifest from mathlib tag - `--sweep`: Test different thread counts to find optimal parallelism - `--json`: Machine-readable output - `-l/--limit`: Limit files for quick tests **Profiling:** - New `profile` module with atomic counters for lock-free metrics - Detailed timing breakdown: read, zstd init, decompress, file I/O - Byte counters for compressed/decompressed data - File type counters (zstd, lgz, lgz_module, hash variants) **Instrumentation:** - `ltar.rs`: Fine-grained profiling of all unpack operations - `tar.rs`: Wall-clock timing and profile report output 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
kim-em
force-pushed
the
fix-manifest-path
branch
from
December 3, 2025 03:15
b64f06d to
1762673
Compare
Apply fn_single_line, match_arm_blocks, trailing_semicolon, and where_single_line formatting options from rustfmt.toml. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Fixes clippy::lines_filter_map_ok warning - filter_map() could run forever if the iterator repeatedly produces Err on a read error. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
Replace table-like ASCII formatting with simpler text output that doesn't have alignment issues. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
digama0
reviewed
Dec 9, 2025
| eprintln!(); | ||
| eprintln!("To create a manifest for a specific mathlib version:"); | ||
| eprintln!(" leantar-benchmark --create-manifest v4.26.0-rc1"); | ||
| eprintln!(" leantar-benchmark --create-manifest v4.26.0-rc2"); |
Owner
There was a problem hiding this comment.
Should I be worried about this being something to update all the time?
Contributor
Author
There was a problem hiding this comment.
It's only in a help message that a user is meant to copy, so I'd hope that they update it as they prefer (or that it just doesn't matter).
We could also change this to e.g. stable.
I'm not actually particularly sure we want to merge this --- I'd like to get to the bottom of slow decompression on macos, and Jireh's reports of intermittent single-threaded behaviour, but hopefully we can collect the data just by people using the PR. The actual code in this PR is entirely AI generated and I don't particular want to have to read it / vouch for it.
Owner
There was a problem hiding this comment.
I was going to suggest the same. If the PR alone is good enough for you, then I think I would prefer not to merge it for now.
The --create-manifest command was downloading cache files to a temp directory and then deleting them, causing --sweep to fail because the .ltar files no longer existed. Now: - Cache files are downloaded to benchmarks/cache-<tag>/ (persistent) - The cache path is stored in the manifest header - Benchmarks read the cache path from the manifest by default - Users can override with their system cache (~/.cache/mathlib) for in-situ benchmarking 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
kim-em
marked this pull request as draft
December 11, 2025 01:55
Contributor
Author
|
Closing per @digama0's preference — thanks for the review. |
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
2 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.
See #mathlib4 > lake exe cache get very slow @ 💬, where I discovered that setting the parallelism significantly lower than the number of CPUs gives much better throughput. Needs testing now on other machines.
No particular need to merge this, we can benchmark from the branch.
Add comprehensive benchmarking and profiling support for leantar:
New
leantar-benchmarkbinary for reproducible performance testing--create-manifest <TAG>: Generate manifest from mathlib tag (writes to./benchmarks/)--sweep: Test different thread counts to find optimal parallelism--json: Machine-readable output for CI integration-l/--limit: Limit files for quick testsNew
profilemodule with atomic counters for lock-free metricsInstrumentation in
ltar.rswith fine-grained profiling of all unpack operationsProfile reporting in
tar.rswith wall-clock timing and breakdown🤖 Prepared with Claude Code