lean-mathlib bench seems to be broken

[zooko]

I noticed lean-mathlib was only taking a few seconds:

~/playground/mimalloc-bench-upstream/out/bench$ time ../../bench.sh sys je sn mi2 rp lean-mathlib 2>&1 | tee ../../../log.34.txt
benchmarking on 88 cores.
use '-h' or '--help' for help on configuration options.

allocators:  sys je sn mi2 rp
tests     :  lean-mathlib
~/playground/mimalloc-bench-upstream/extern/mathlib ~/playground/mimalloc-bench-upstream/out/bench

---- 1: mathlib

run 1: mathlib sys: SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sys   0:00.47 75328 0.39 0.08 0 32798

run 1: mathlib je: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/je/lib/libjemalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     je    0:00.39 67584 0.31 0.08 0 30444

run 1: mathlib sn: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/sn/release/libsnmallocshim.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sn    0:00.38 71104 0.31 0.07 0 30138

run 1: mathlib mi2: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/mi2/out/release/libmimalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     mi2   0:00.37 69696 0.31 0.06 0 28967

run 1: mathlib rp: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/rp/bin/linux/release/x86-64/librpmallocwrap.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     rp    0:00.39 73216 0.31 0.08 0 32205
~/playground/mimalloc-bench-upstream/out/bench

results written to: /home/usern/playground/mimalloc-bench-upstream/out/bench/benchres.csv

#------------------------------------------------------------------
# test    alloc   time  rss    user  sys  page-faults page-reclaims
mathlib     sys   00.47 75328 0.39 0.08 0 32798
mathlib     je    00.39 67584 0.31 0.08 0 30444
mathlib     sn    00.38 71104 0.31 0.07 0 30138
mathlib     mi2   00.37 69696 0.31 0.06 0 28967
mathlib     rp    00.39 73216 0.31 0.08 0 32205

Executing the command shown in the directory shown results in:

usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/out/bench$ pushd ~/playground/mimalloc-bench-upstream/extern/mathlib
~/playground/mimalloc-bench-upstream/extern/mathlib ~/playground/mimalloc-bench-upstream/out/bench ~/playground/mimalloc-bench-upstream/out/bench ~/playground/mimalloc-bench-upstream ~/playground/mimalloc-bench-upstream/out/bench
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/extern/mathlib$ time SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
configuring leanpkg 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    0m0.470s
user    0m0.382s
sys     0m0.089s

[zooko]

I did a little experimenting, by deleting all the .olean files, in which case the leanpkg command took more like 20 seconds:

usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/extern$ find . -iname '*olean' -print0  | xargs -0 rm
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/out/bench$ pushd ~/playground/mimalloc-bench-upstream/extern/mathlib
~/playground/mimalloc-bench-upstream/extern/mathlib ~/playground/mimalloc-bench-upstream/out/bench
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/extern/mathlib$ time SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
configuring leanpkg 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    0m19.412s
user    0m46.642s
sys     0m1.919s
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/extern/mathlib$ time SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
configuring leanpkg 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    0m18.981s
user    0m45.110s
sys     0m1.785s
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/extern/mathlib$ time SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
configuring leanpkg 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    0m19.448s
user    0m46.441s
sys     0m1.904s

So then I tried the bench.sh script, and it too took 15-20 seconds (depending on the allocator):

usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/out/bench$ ../../bench.sh sys je sn mi2 rp lean-mathlib 2>&1 | tee ../../../log.35.txt
benchmarking on 88 cores.
use '-h' or '--help' for help on configuration options.

allocators:  sys je sn mi2 rp
tests     :  lean-mathlib
~/playground/mimalloc-bench-upstream/extern/mathlib ~/playground/mimalloc-bench-upstream/out/bench

---- 1: mathlib

run 1: mathlib sys: SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sys   0:19.34 575716 45.85 1.95 0 431472

run 1: mathlib je: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/je/lib/libjemalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     je    0:16.07 499064 38.84 1.64 0 329752

run 1: mathlib sn: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/sn/release/libsnmallocshim.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sn    0:15.89 662268 38.65 1.63 0 358642

run 1: mathlib mi2: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/mi2/out/release/libmimalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     mi2   0:16.25 607284 39.27 1.69 0 366072

run 1: mathlib rp: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/rp/bin/linux/release/x86-64/librpmallocwrap.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     rp    0:16.38 689136 39.03 1.74 0 364966
~/playground/mimalloc-bench-upstream/out/bench

results written to: /home/usern/playground/mimalloc-bench-upstream/out/bench/benchres.csv

#------------------------------------------------------------------
# test    alloc   time  rss    user  sys  page-faults page-reclaims
mathlib     sys   19.34 575716 45.85 1.95 0 431472
mathlib     je    16.07 499064 38.84 1.64 0 329752
mathlib     sn    15.89 662268 38.65 1.63 0 358642
mathlib     mi2   16.25 607284 39.27 1.69 0 366072
mathlib     rp    16.38 689136 39.03 1.74 0 364966

So then I git cloned a fresh copy of mimalloc-bench, built it, and ran the lean-mathlib bench,
but it is back to taking < 1 second.

usern@us1-blade41-d:~/playground$ git clone https://github.com/daanx/mimalloc-bench mimalloc-bench-upstream
Cloning into 'mimalloc-bench-upstream'...
...
usern@us1-blade41-d:~/playground$ cd !$
cd mimalloc-bench-upstream
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream$ ./build-bench-env.sh sys je sn mi2 rp bench lean
...
--------------------------------------------
done in /home/usern/playground/mimalloc-bench-upstream
--------------------------------------------

run the cfrac benchmarks as:
> cd out/bench
> ../../bench.sh alla cfrac

to see all options use:
> ../../bench.sh help
usern@us1-blade41-d:~/playground/mimalloc-bench-upstream/out/bench$ ../../bench.sh sys je sn mi2 rp lean-mathlib
benchmarking on 88 cores.
use '-h' or '--help' for help on configuration options.

allocators:  sys je sn mi2 rp
tests     :  lean-mathlib
~/playground/mimalloc-bench-upstream/extern/mathlib ~/playground/mimalloc-bench-upstream/out/bench

---- 1: mathlib

run 1: mathlib sys: SYSMALLOC=1 /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sys   0:00.46 75328 0.38 0.08 0 32781

run 1: mathlib je: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/je/lib/libjemalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     je    0:00.39 67584 0.32 0.07 0 30434

run 1: mathlib sn: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/sn/release/libsnmallocshim.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     sn    0:00.38 71104 0.32 0.06 0 30117

run 1: mathlib mi2: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/mi2/out/release/libmimalloc.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     mi2   0:00.37 69696 0.31 0.06 0 28956

run 1: mathlib rp: LD_PRELOAD=/home/usern/playground/mimalloc-bench-upstream/extern/rp/bin/linux/release/x86-64/librpmallocwrap.so /home/usern/playground/mimalloc-bench-upstream/extern/lean/bin/leanpkg build
preprocess...
mathlib     rp    0:00.39 73216 0.31 0.07 0 32223
~/playground/mimalloc-bench-upstream/out/bench

results written to: /home/usern/playground/mimalloc-bench-upstream/out/bench/benchres.csv

#------------------------------------------------------------------
# test    alloc   time  rss    user  sys  page-faults page-reclaims
mathlib     sys   00.46 75328 0.38 0.08 0 32781
mathlib     je    00.39 67584 0.32 0.07 0 30434
mathlib     sn    00.38 71104 0.32 0.06 0 30117
mathlib     mi2   00.37 69696 0.31 0.06 0 28956
mathlib     rp    00.39 73216 0.31 0.07 0 32223

[zooko]

Hm, I was just messing with something else in mimalloc-bench, and I happened to notice this bit:

mimalloc-bench/bench.sh

Line 534 in 2951c39

make clean-olean

. I wonder if that's not getting executed when it should...

[mjp41]

I guess I am not sure I know what the desired behaviour is here.

Looking at #195

This fix seems to make it not fail, but I think perhaps something is meant to be checked out here?

[zooko]

I think the desired behavior is that the lean-mathlib bench should build all the .olean files from the source files. That's the benchmark, and I'm guessing based on my experiment recounted above that this benchmark should take 15-20 seconds. I think the current behavior is that the lean-mathlib bench determines that all the .olean files are already up to date, in less than 1 second. I'll bet that "clean olean" step to delete all the .olean files isn't getting executed, or else it is getting executed but failing to delete the .olean files. Maybe they live in a different location now than where that step is looking for them.

[mjp41]

I think this might be the correct fix

#254

The size of this benchmark is huge though

[zooko]

Great! I want a big benchmark. (related discussion: https://bsky.app/profile/zooko2.bsky.social/post/3mddzfpchc22h )

[jvoisin]

This brings the question of how to ensure that the benchmark is still working without running it in the Github CI.

[zooko]

Hold on, it’s been running for several hours now, using all 88 cores of my server, and has not emitted one line of output other than “preprocessing…”. Is this what you meant by huge!?

[zooko]

Hold on, it’s been running for several hours now, using all 88 cores of my server, and has not emitted one line of output other than “preprocessing…”. Is this what you meant by huge!?

Update: okay what actually happened was that my RAM failed. From IPMI:

 4d4 | 01/12/2026 | 05:20:55 PM UTC | Session Audit #0xff |  | Asserted
 4d5 | 01/12/2026 | 05:20:56 PM UTC | Session Audit #0xff |  | Asserted
 4d6 | 01/12/2026 | 05:20:57 PM UTC | Session Audit #0xff |  | Asserted
 4d7 | 01/12/2026 | 05:20:57 PM UTC | Session Audit #0xff |  | Asserted
 53c | 01/27/2026 | 11:08:33 PM UTC | Memory | Uncorrectable ECC (@DIMMB1(CPU2)) | Asserted
 53d | 01/27/2026 | 11:09:21 PM UTC | Unknown #0xfe |  | Asserted
 53e | 01/27/2026 | 11:09:47 PM UTC | Unknown #0xfe |  | Asserted

[zooko]

Update: running it on a new server with working RAM, it took one hour and generated some very large numbers for high-water-mark-rss and for soft page faults. Great! This is exactly the kind of heavyweight test I've been looking for!

Hm. Interesting that it generated 0 hard page faults in this run! 🤔

usern@srv142630:~/playground/mimalloc-bench/out/bench$ time ../../bench.sh sys lean-mathlib 2>&1 | tee ../../tmp/bench.2.log.txt
benchmarking on 256 cores.
use '-h' or '--help' for help on configuration options.

allocators:  sys
tests     :  lean-mathlib
~/playground/mimalloc-bench/extern/mathlib ~/playground/mimalloc-bench/out/bench

---- 1: mathlib

run 1: mathlib sys: SYSMALLOC=1 /home/usern/playground/mimalloc-bench/extern/lean/bin/leanpkg build
preprocess...

mathlib     sys   1:05:48 95474668 187738.52 265.74 0 29228932
~/playground/mimalloc-bench/out/bench

results written to: /home/usern/playground/mimalloc-bench/out/bench/benchres.csv

#------------------------------------------------------------------
# test    alloc   time  rss    user  sys  page-faults page-reclaims
mathlib     sys   1:05:48 95474668 187738.52 265.74 0 29228932


real    65m48.187s
user    3128m58.549s
sys     4m25.817s

[zooko]

FYI here's the output (which I manually edited to trim out and rename fields so I could fit it into a pair of space-limited posts on bluesky) of a six-hour run of this from https://github.com/zooko/mimalloc-bench

alloc  time     max rss     faults
-----  -------  ----------  -----------
  sys  1:05:48  95,474,668   29,228,932
   je  1:03:52  30,433,204  232,731,733
   sn  1:04:40  81,733,632   21,683,587
  mi2  1:03:46  33,444,528  235,687,074
   rp  1:03:03  44,411,860  145,587,326
    s  1:06:55  55,431,168   27,284,750