thomas@trm leangz % cargo clean Removed 2309 files, 391.7MiB total thomas@trm leangz % cargo build --release Compiling libc v0.2.171 Compiling proc-macro2 v1.0.94 Compiling unicode-ident v1.0.18 Compiling shlex v1.3.0 Compiling crossbeam-utils v0.8.21 Compiling pkg-config v0.3.32 Compiling zstd-safe v7.2.4 Compiling serde v1.0.219 Compiling rayon-core v1.12.1 Compiling serde_json v1.0.140 Compiling zerocopy v0.8.24 Compiling equivalent v1.0.2 Compiling allocator-api2 v0.2.21 Compiling foldhash v0.1.5 Compiling memchr v2.7.4 Compiling either v1.15.0 Compiling itoa v1.0.15 Compiling ryu v1.0.20 Compiling byteorder v1.5.0 Compiling hashbrown v0.15.2 Compiling quote v1.0.40 Compiling jobserver v0.1.32 Compiling memmap2 v0.9.5 Compiling syn v2.0.100 Compiling cc v1.2.17 Compiling crossbeam-epoch v0.9.18 Compiling crossbeam-deque v0.8.6 Compiling zstd-sys v2.0.15+zstd.1.5.7 Compiling rayon v1.10.0 Compiling serde_derive v1.0.219 Compiling zerocopy-derive v0.8.24 Compiling zstd v0.13.3 Compiling leangz v0.1.16 (/Users/thomas/LeanContribution/leangz) Finished `release` profile [optimized] target(s) in 5.96s thomas@trm leangz % cargo install --path . Installing leangz v0.1.16 (/Users/thomas/LeanContribution/leangz) Updating crates.io index Locking 39 packages to latest compatible versions Adding hashbrown v0.15.5 (available: v0.16.1) Compiling libc v0.2.178 Compiling proc-macro2 v1.0.103 Compiling unicode-ident v1.0.22 Compiling quote v1.0.42 Compiling find-msvc-tools v0.1.5 Compiling serde_core v1.0.228 Compiling rayon-core v1.13.0 Compiling zerocopy v0.8.31 Compiling serde v1.0.228 Compiling serde_json v1.0.145 Compiling memchr v2.7.6 Compiling hashbrown v0.15.5 Compiling rayon v1.11.0 Compiling syn v2.0.111 Compiling jobserver v0.1.34 Compiling memmap2 v0.9.9 Compiling cc v1.2.49 Compiling zstd-sys v2.0.16+zstd.1.5.7 Compiling zerocopy-derive v0.8.31 Compiling serde_derive v1.0.228 Compiling zstd-safe v7.2.4 Compiling zstd v0.13.3 Compiling leangz v0.1.16 (/Users/thomas/LeanContribution/leangz) Finished `release` profile [optimized] target(s) in 5.84s Replacing /Users/thomas/.cargo/bin/leangz Replacing /Users/thomas/.cargo/bin/leantar Replacing /Users/thomas/.cargo/bin/leantar-benchmark Replaced package `leangz v0.1.16 (/Users/thomas/LeanContribution/leangz)` with `leangz v0.1.16 (/Users/thomas/LeanContribution/leangz)` (executables `leangz`, `leantar`, `leantar-benchmark`) thomas@trm leangz % leantar-benchmark --create-manifest v4.26.0-rc2 Creating manifest for mathlib v4.26.0-rc2 Clone dir: /var/folders/dj/q118rpgd5zb9pzjsxn0d154m0000gn/T/mathlib-manifest-v4.26.0-rc2 Cache dir: /var/folders/dj/q118rpgd5zb9pzjsxn0d154m0000gn/T/mathlib-cache-v4.26.0-rc2 Cloning mathlib4 at v4.26.0-rc2... Cloning into '/var/folders/dj/q118rpgd5zb9pzjsxn0d154m0000gn/T/mathlib-manifest-v4.26.0-rc2'... remote: Enumerating objects: 8910, done. remote: Counting objects: 100% (8910/8910), done. remote: Compressing objects: 100% (8583/8583), done. Receiving objects: 36% (3208/8910), 5.75 MiB | 11.49 MiReceiving objects: 37% (3297/8910), 5.75 MiB | 11.49 MiReceiving objects: 38% (3386/8910), 5.75 MiB | 11.49 MiReceiving objects: 39% (3475/8910), 5.75 MiB | 11.49 MiReceiving objects: 40% (3564/8910), 5.75 MiB | 11.49 MiReceiving objects: 41% (3654/8910), 5.75 MiB | 11.49 MiReceiving objects: 42% (3743/8910), 5.75 MiB | 11.49 MiReceiving objects: 43% (3832/8910), 5.75 MiB | 11.49 MiReceiving objects: 44% (3921/8910), 5.75 MiB | 11.49 MiReceiving objects: 45% (4010/8910), 5.75 MiB | 11.49 MiReceiving objects: 46% (4099/8910), 5.75 MiB | 11.49 MiReceiving objects: 47% (4188/8910), 5.75 MiB | 11.49 MiReceiving objects: 48% (4277/8910), 5.75 MiB | 11.49 MiReceiving objects: 49% (4366/8910), 5.75 MiB | 11.49 MiReceiving objects: 50% (4455/8910), 5.75 MiB | 11.49 MiReceiving objects: 51% (4545/8910), 5.75 MiB | 11.49 MiReceiving objects: 52% (4634/8910), 5.75 MiB | 11.49 MiReceiving objects: 53% (4723/8910), 5.75 MiB | 11.49 MiReceiving objects: 54% (4812/8910), 5.75 MiB | 11.49 MiReceiving objects: 55% (4901/8910), 5.75 MiB | 11.49 MiReceiving objects: 56% (4990/8910), 5.75 MiB | 11.49 MiReceiving objects: 57% (5079/8910), 5.75 MiB | 11.49 MiReceiving objects: 58% (5168/8910), 5.75 MiB | 11.49 MiReceiving objects: 59% (5257/8910), 5.75 MiB | 11.49 MiReceiving objects: 59% (5293/8910), 11.35 MiB | 11.34 MReceiving objects: 60% (5346/8910), 11.35 MiB | 11.34 MReceiving objects: 61% (5436/8910), 11.35 MiB | 11.34 MReceiving objects: 62% (5525/8910), 11.35 MiB | 11.34 MReceiving objects: 63% (5614/8910), 11.35 MiB | 11.34 MReceiving objects: 64% (5703/8910), 11.35 MiB | 11.34 MReceiving objects: 65% (5792/8910), 11.35 MiB | 11.34 MReceiving objects: 66% (5881/8910), 11.35 MiB | 11.34 MReceiving objects: 67% (5970/8910), 11.35 MiB | 11.34 MReceiving objects: 68% (6059/8910), 11.35 MiB | 11.34 MReceiving objects: 69% (6148/8910), 11.35 MiB | 11.34 MReceiving objects: 70% (6237/8910), 11.35 MiB | 11.34 MReceiving objects: 71% (6327/8910), 11.35 MiB | 11.34 MReceiving objects: 72% (6416/8910), 11.35 MiB | 11.34 MReceiving objects: 73% (6505/8910), 11.35 MiB | 11.34 MReceiving objects: 74% (6594/8910), 11.35 MiB | 11.34 MReceiving objects: 75% (6683/8910), 11.35 MiB | 11.34 MReceiving objects: 76% (6772/8910), 16.46 MiB | 10.96 MReceiving objects: 77% (6861/8910), 16.46 MiB | 10.96 MReceiving objects: 78% (6950/8910), 16.46 MiB | 10.96 MReceiving objects: 79% (7039/8910), 16.46 MiB | 10.96 MReceiving objects: 80% (7128/8910), 16.46 MiB | 10.96 MReceiving objects: 81% (7218/8910), 16.46 MiB | 10.96 MReceiving objects: 82% (7307/8910), 16.46 MiB | 10.96 MReceiving objects: 83% (7396/8910), 16.46 MiB | 10.96 MReceiving objects: 84% (7485/8910), 16.46 MiB | 10.96 MReceiving objects: 85% (7574/8910), 16.46 MiB | 10.96 MReceiving objects: 86% (7663/8910), 16.46 MiB | 10.96 MReceiving objects: 87% (7752/8910), 16.46 MiB | 10.96 MReceiving objects: 88% (7841/8910), 16.46 MiB | 10.96 MReceiving objects: 89% (7930/8910), 16.46 MiB | 10.96 MReceiving objects: 90% (8019/8910), 16.46 MiB | 10.96 MReceiving objects: 91% (8109/8910), 16.46 MiB | 10.96 MReceiving objects: 92% (8198/8910), 16.46 MiB | 10.96 MReceiving objects: 93% (8287/8910), 16.46 MiB | 10.96 MReceiving objects: 94% (8376/8910), 16.46 MiB | 10.96 MReceiving objects: 95% (8465/8910), 16.46 MiB | 10.96 MReceiving objects: 95% (8491/8910), 16.46 MiB | 10.96 MReceiving objects: 96% (8554/8910), 21.96 MiB | 10.97 MReceiving objects: 97% (8643/8910), 21.96 MiB | 10.97 MReceiving objects: 98% (8732/8910), 21.96 MiB | 10.97 MReceiving objects: 99% (8821/8910), 21.96 MiB | 10.97 Mremote: Total 8910 (delta 236), reused 1340 (delta 174), pack-reused 0 (from 0) Receiving objects: 100% (8910/8910), 21.96 MiB | 10.97 MReceiving objects: 100% (8910/8910), 22.51 MiB | 10.98 MiB/s, done. Resolving deltas: 100% (236/236), done. Note: switching to 'd5c9558e75342a10d6321e6a8c798a14f68ae23c'. You are in 'detached HEAD' state. You can look around, make experimental changes and commit them, and you can discard any commits you make in this state without impacting any branches by switching back to a branch. If you want to create a new branch to retain commits you create, you may do so (now or later) by using -c with the switch command. Example: git switch -c Or undo this operation with: git switch - Turn off this advice by setting config variable advice.detachedHead to false Downloading cache files... info: plausible: cloning https://github.com/leanprover-community/plausible info: plausible: checking out revision '74835c84b38e4070b8240a063c6417c767e551ae' info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf' info: importGraph: cloning https://github.com/leanprover-community/import-graph info: importGraph: checking out revision '6e3bb4bf31f731ab28891fe229eb347ec7d5dad3' info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 info: proofwidgets: checking out revision '2aaad968dd10a168b644b6a5afd4b92496af4710' info: aesop: cloning https://github.com/leanprover-community/aesop info: aesop: checking out revision '9c70abdd9215b76019340fad65138e2e8d21843e' info: Qq: cloning https://github.com/leanprover-community/quote4 info: Qq: checking out revision 'a31845b5557fd5e47d52b9e2977a1b0eff3c38c3' info: batteries: cloning https://github.com/leanprover-community/batteries info: batteries: checking out revision 'afe9302d9243cee630b0be95322b38b90342ddbf' info: Cli: cloning https://github.com/leanprover/lean4-cli info: Cli: checking out revision '7e1ced9e049a4fab2508980ec4877ca9c46dffc9' ⣽ [7/20] Running Batteries.Data.String.Basic:c.o (+ 2 mo ⣾ [9/20] Running Batteries.Data.Array.Match:c.o (+ 2 mor PANIC at String.toNat! Init.Data.String.Extra:39:4: Nat expected backtrace: 0 cache 0x00000001090a01d8 _ZN4leanL15lean_panic_implEPKcmb + 268 1 cache 0x00000001090a06ac lean_panic_fn + 40 2 cache 0x00000001021d4048 l_Cache_IO_parseVersion + 548 3 cache 0x00000001021d4ae4 l_Cache_IO_validateLeanTar + 1560 4 cache 0x00000001021c4ad0 l_main___lam__1 + 1416 5 cache 0x00000001090ae114 lean_apply_2 + 788 6 cache 0x00000001021c7f0c main + 204 7 dyld 0x000000018d5feb98 start + 6076 installing leantar 0.1.16 % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- - 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- -100 884k 100 884k 0 0 3816k 0 --:--:-- --:--:-- --:--:-- 10.9M Fetching ProofWidgets cloud release... done! Current branch: HEAD Using cache (Azure) from origin: leanprover-community/mathlib4 Attempting to download 7572 file(s) from leanprover-community/mathlib4 cache Downloaded: 161 file(s) [attempted 161/7572 = 2%, 221 KBDownloaded: 249 file(s) [attempted 249/7572 = 3%, 773 KBDownloaded: 346 file(s) [attempted 346/7572 = 4%, 739 KBDownloaded: 443 file(s) [attempted 443/7572 = 5%, 852 KBDownloaded: 531 file(s) [attempted 531/7572 = 7%, 2411 KDownloaded: 628 file(s) [attempted 628/7572 = 8%, 278 KBDownloaded: 725 file(s) [attempted 725/7572 = 9%, 85 KB/Downloaded: 822 file(s) [attempted 822/7572 = 10%, 1007 Downloaded: 910 file(s) [attempted 910/7572 = 12%, 952 KDownloaded: 1007 file(s) [attempted 1007/7572 = 13%, 174Downloaded: 1104 file(s) [attempted 1104/7572 = 14%, 455Downloaded: 1201 file(s) [attempted 1201/7572 = 15%, 158Downloaded: 1298 file(s) [attempted 1298/7572 = 17%, 210Downloaded: 1395 file(s) [attempted 1395/7572 = 18%, 934Downloaded: 1502 file(s) [attempted 1502/7572 = 19%, 925Downloaded: 1599 file(s) [attempted 1599/7572 = 21%, 115Downloaded: 1697 file(s) [attempted 1697/7572 = 22%, 677Downloaded: 1784 file(s) [attempted 1784/7572 = 23%, 527Downloaded: 1866 file(s) [attempted 1866/7572 = 24%, 224Downloaded: 1939 file(s) [attempted 1939/7572 = 25%, 663Downloaded: 2027 file(s) [attempted 2027/7572 = 26%, 521Downloaded: 2124 file(s) [attempted 2124/7572 = 28%, 700Downloaded: 2211 file(s) [attempted 2211/7572 = 29%, 519Downloaded: 2302 file(s) [attempted 2302/7572 = 30%, 225Downloaded: 2376 file(s) [attempted 2376/7572 = 31%, 367Downloaded: 2462 file(s) [attempted 2462/7572 = 32%, 176Downloaded: 2541 file(s) [attempted 2541/7572 = 33%, 149Downloaded: 2629 file(s) [attempted 2629/7572 = 34%, 103Downloaded: 2707 file(s) [attempted 2707/7572 = 35%, 289Downloaded: 2755 file(s) [attempted 2755/7572 = 36%, 448Downloaded: 2813 file(s) [attempted 2813/7572 = 37%, 830Downloaded: 2901 file(s) [attempted 2901/7572 = 38%, 594Downloaded: 2988 file(s) [attempted 2988/7572 = 39%, 224Downloaded: 3082 file(s) [attempted 3082/7572 = 40%, 114Downloaded: 3173 file(s) [attempted 3173/7572 = 41%, 503Downloaded: 3270 file(s) [attempted 3270/7572 = 43%, 114Downloaded: 3367 file(s) [attempted 3367/7572 = 44%, 148Downloaded: 3464 file(s) [attempted 3464/7572 = 45%, 424Downloaded: 3551 file(s) [attempted 3551/7572 = 46%, 242Downloaded: 3639 file(s) [attempted 3639/7572 = 48%, 617Downloaded: 3720 file(s) [attempted 3720/7572 = 49%, 171Downloaded: 3804 file(s) [attempted 3804/7572 = 50%, 529Downloaded: 3901 file(s) [attempted 3901/7572 = 51%, 896Downloaded: 3979 file(s) [attempted 3979/7572 = 52%, 386Downloaded: 4066 file(s) [attempted 4066/7572 = 53%, 373Downloaded: 4144 file(s) [attempted 4144/7572 = 54%, 146Downloaded: 4222 file(s) [attempted 4222/7572 = 55%, 479Downloaded: 4299 file(s) [attempted 4299/7572 = 56%, 361Downloaded: 4396 file(s) [attempted 4396/7572 = 58%, 146Downloaded: 4484 file(s) [attempted 4484/7572 = 59%, 205Downloaded: 4571 file(s) [attempted 4571/7572 = 60%, 915Downloaded: 4657 file(s) [attempted 4657/7572 = 61%, 320Downloaded: 4746 file(s) [attempted 4746/7572 = 62%, 502Downloaded: 4843 file(s) [attempted 4843/7572 = 63%, 780Downloaded: 4940 file(s) [attempted 4940/7572 = 65%, 299Downloaded: 5037 file(s) [attempted 5037/7572 = 66%, 309Downloaded: 5134 file(s) [attempted 5134/7572 = 67%, 414Downloaded: 5232 file(s) [attempted 5232/7572 = 69%, 275Downloaded: 5329 file(s) [attempted 5329/7572 = 70%, 151Downloaded: 5426 file(s) [attempted 5426/7572 = 71%, 156Downloaded: 5513 file(s) [attempted 5513/7572 = 72%, 292Downloaded: 5610 file(s) [attempted 5610/7572 = 74%, 302Downloaded: 5698 file(s) [attempted 5698/7572 = 75%, 308Downloaded: 5775 file(s) [attempted 5775/7572 = 76%, 153Downloaded: 5853 file(s) [attempted 5853/7572 = 77%, 684Downloaded: 5921 file(s) [attempted 5921/7572 = 78%, 598Downloaded: 5989 file(s) [attempted 5989/7572 = 79%, 472Downloaded: 6076 file(s) [attempted 6076/7572 = 80%, 184Downloaded: 6164 file(s) [attempted 6164/7572 = 81%, 500Downloaded: 6251 file(s) [attempted 6251/7572 = 82%, 472Downloaded: 6339 file(s) [attempted 6339/7572 = 83%, 131Downloaded: 6416 file(s) [attempted 6416/7572 = 84%, 273Downloaded: 6513 file(s) [attempted 6513/7572 = 86%, 486Downloaded: 6601 file(s) [attempted 6601/7572 = 87%, 138Downloaded: 6688 file(s) [attempted 6688/7572 = 88%, 815Downloaded: 6785 file(s) [attempted 6785/7572 = 89%, 441Downloaded: 6873 file(s) [attempted 6873/7572 = 90%, 108Downloaded: 6960 file(s) [attempted 6960/7572 = 91%, 153Downloaded: 7048 file(s) [attempted 7048/7572 = 93%, 232Downloaded: 7125 file(s) [attempted 7125/7572 = 94%, 935Downloaded: 7213 file(s) [attempted 7213/7572 = 95%, 129Downloaded: 7310 file(s) [attempted 7310/7572 = 96%, 113Downloaded: 7397 file(s) [attempted 7397/7572 = 97%, 327Downloaded: 7485 file(s) [attempted 7485/7572 = 98%, 630Downloaded: 7562 file(s) [attempted 7562/7572 = 99%, 116Downloaded: 7572 file(s) [attempted 7572/7572 = 100%, 1160 KB/s] Decompressing 7572 file(s) Unpacked in 8560 ms Completed successfully! Collecting .ltar files... Found 7572 .ltar files Manifest written to: /Users/thomas/LeanContribution/leangz/benchmarks/mathlib-v4.26.0-rc2.manifest Files in manifest: 7572 Cleaning up temporary directories... Done! thomas@trm leangz % leantar-benchmark --sweep Thread Count Sweep Testing: [1, 2, 4, 6, 8, 12, 14] Testing 1 threads... FAILED Testing 2 threads... FAILED Testing 4 threads... FAILED Testing 6 threads... FAILED Testing 8 threads... FAILED Testing 12 threads... FAILED Testing 14 threads... FAILED No successful benchmark runs! thomas@trm leangz % git show HEAD commit 1651fd4049737e089c08696d313e9d00a9358071 (HEAD -> fix-manifest-path, kim-em/fix-manifest-path) Author: Kim Morrison Date: Tue Dec 9 01:40:05 2025 +0000 docs: update examples to use v4.26.0-rc2 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude diff --git a/src/benchmark.rs b/src/benchmark.rs index 592140d..27ba440 100644 --- a/src/benchmark.rs +++ b/src/benchmark.rs @@ -142,7 +142,7 @@ fn main() { eprintln!("Error: No benchmark manifest found.");