PS C:\Users\Notoc\Coding\Lean\leangz> cargo build --release Compiling proc-macro2 v1.0.94 Compiling unicode-ident v1.0.18 Compiling shlex v1.3.0 Compiling jobserver v0.1.32 Compiling crossbeam-utils v0.8.21 Compiling pkg-config v0.3.32 Compiling rayon-core v1.12.1 Compiling serde v1.0.219 Compiling zstd-safe v7.2.4 Compiling serde_json v1.0.140 Compiling zerocopy v0.8.24 Compiling equivalent v1.0.2 Compiling itoa v1.0.15 Compiling ryu v1.0.20 Compiling either v1.15.0 Compiling allocator-api2 v0.2.21 Compiling foldhash v0.1.5 Compiling memchr v2.7.4 Compiling byteorder v1.5.0 Compiling memmap2 v0.9.5 Compiling cc v1.2.17 Compiling hashbrown v0.15.2 Compiling crossbeam-epoch v0.9.18 Compiling quote v1.0.40 Compiling crossbeam-deque v0.8.6 Compiling syn v2.0.100 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 (C:\Users\Notoc\Coding\Lean\leangz) Finished `release` profile [optimized] target(s) in 8.08s PS C:\Users\Notoc\Coding\Lean\leangz> cargo install --path . Installing leangz v0.1.16 (C:\Users\Notoc\Coding\Lean\leangz) Updating crates.io index Locking 39 packages to latest compatible versions Adding hashbrown v0.15.5 (available: v0.16.1) Downloaded quote v1.0.42 Downloaded jobserver v0.1.34 Downloaded cfg-if v1.0.4 Downloaded unicode-ident v1.0.22 Downloaded serde_derive v1.0.228 Downloaded memchr v2.7.6 Downloaded find-msvc-tools v0.1.5 Downloaded memmap2 v0.9.9 Downloaded serde_core v1.0.228 Downloaded zerocopy-derive v0.8.31 Downloaded serde v1.0.228 Downloaded hashbrown v0.15.5 Downloaded proc-macro2 v1.0.103 Downloaded rayon-core v1.13.0 Downloaded getrandom v0.3.4 Downloaded serde_json v1.0.145 Downloaded cc v1.2.49 Downloaded rayon v1.11.0 Downloaded zerocopy v0.8.31 Downloaded syn v2.0.111 Downloaded zstd-sys v2.0.16+zstd.1.5.7 Downloaded 21 crates (2.7 MB) in 1.12s Compiling getrandom v0.3.4 Compiling cfg-if v1.0.4 Compiling proc-macro2 v1.0.103 Compiling find-msvc-tools v0.1.5 Compiling unicode-ident v1.0.22 Compiling quote v1.0.42 Compiling serde_core v1.0.228 Compiling rayon-core v1.13.0 Compiling serde_json v1.0.145 Compiling zerocopy v0.8.31 Compiling serde v1.0.228 Compiling memchr v2.7.6 Compiling memmap2 v0.9.9 Compiling hashbrown v0.15.5 Compiling jobserver v0.1.34 Compiling cc v1.2.49 Compiling rayon v1.11.0 Compiling syn v2.0.111 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 (C:\Users\Notoc\Coding\Lean\leangz) Finished `release` profile [optimized] target(s) in 8.53s Installing C:\Users\Notoc\.cargo\bin\leangz.exe Installing C:\Users\Notoc\.cargo\bin\leantar-benchmark.exe Installing C:\Users\Notoc\.cargo\bin\leantar.exe Installed package `leangz v0.1.16 (C:\Users\Notoc\Coding\Lean\leangz)` (executables `leangz.exe`, `leantar-benchmark.exe`, `leantar.exe`) PS C:\Users\Notoc\Coding\Lean\leangz> leantar-benchmark --create-release v4.26.0 Unknown option: --create-release PS C:\Users\Notoc\Coding\Lean\leangz> leantar-benchmark --create-manifest v4.26.0 Creating manifest for mathlib v4.26.0 Clone dir: C:\Users\Notoc\AppData\Local\Temp\mathlib-manifest-v4.26.0 Cache dir: C:\Users\Notoc\AppData\Local\Temp\mathlib-cache-v4.26.0 Cloning mathlib4 at v4.26.0... Cloning into 'C:\Users\Notoc\AppData\Local\Temp\mathlib-manifest-v4.26.0'... fatal: Remote branch v4.26.0 not found in upstream origin Failed to clone mathlib4 at tag v4.26.0 PS C:\Users\Notoc\Coding\Lean\leangz> leantar-benchmark --create-manifest v4.26.0-rc2 Creating manifest for mathlib v4.26.0-rc2 Clone dir: C:\Users\Notoc\AppData\Local\Temp\mathlib-manifest-v4.26.0-rc2 Cache dir: C:\Users\Notoc\AppData\Local\Temp\mathlib-cache-v4.26.0-rc2 Cloning mathlib4 at v4.26.0-rc2... Cloning into 'C:\Users\Notoc\AppData\Local\Temp\mathlib-manifest-v4.26.0-rc2'... remote: Enumerating objects: 8910, done. remote: Counting objects: 100% (8910/8910), done. remote: Compressing objects: 100% (8585/8585), done. remote: Total 8910 (delta 238), reused 1334 (delta 172), pack-reused 0 (from 0) Receiving objects: 100% (8910/8910), 22.51 MiB | 9.87 MiB/s, done. Resolving deltas: 100% (238/238), 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 Updating files: 100% (7817/7817), done. 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' PANIC at String.toNat! Init.Data.String.Extra:39:4: Nat expected 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 100 745k 100 745k 0 0 2212k 0 --:--:-- --:--:-- --:--:-- 2212k 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: 7572 file(s) [attempted 7572/7572 = 100%, 232 KB/s] Decompressing 7572 file(s) Unpacked in 13262 ms Completed successfully! Collecting .ltar files... Found 7572 .ltar files Manifest written to: C:\Users\Notoc\Coding\Lean\leangz\benchmarks\mathlib-v4.26.0-rc2.manifest Files in manifest: 7572 Cleaning up temporary directories... Done! PS C:\Users\Notoc\Coding\Lean\leangz> leantar-benchmark --sweep Thread Count Sweep Testing: [1, 2, 4, 6, 8, 12, 16, 24, 32] 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 16 threads... FAILED Testing 24 threads... FAILED Testing 32 threads... FAILED No successful benchmark runs! PS C:\Users\Notoc\Coding\Lean\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)