feat: enable precompileLibrary for Iris by MackieLoeffel · Pull Request #722 · leanprover-community/iris-lean

MackieLoeffel · 2026-10-21T13:22:38Z

Description

This PR enables the precompileLibrary flag introduced by leanprover/lean4#15015 for Iris. This enables precompilation for clients of Iris, giving a significant performance boost, while not performing precompilation when compiling Iris itself to keep development fast.

cc @alvinylt

MackieLoeffel · 2026-10-21T13:22:53Z

!bench

leanprover-radar · 2026-10-21T13:23:18Z

Benchmark results for 480ba07 against 9a4ae0d are in. No significant results found. @MackieLoeffel

✅ build//instructions: -120.8M (-0.00%)

No significant changes detected.

MackieLoeffel · 2026-10-23T13:35:24Z

!bench

leanprover-radar · 2026-10-23T13:36:47Z

Benchmark results for 6d45091 against 9a4ae0d are in. There are significant results. @MackieLoeffel

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run main has different system configurations between commits.

🟥 main exited with code 1

No significant changes detected.

MackieLoeffel · 2026-10-23T13:43:46Z

@Garmelon I am trying to use precompileLibrary with the benchmark runner, but this is causing errors in the compilation on the runner: https://radar.lean-lang.org/repos/iris-lean/commits/6d450919acd28de46a2639387e0121c1056dbf01/runs/main

[00:00:19] [0.324] ✖ [92/1015] Building Batteries.Classes.Cast:c.o (148ms)
[00:00:19] [0.324] trace: .> cc -c -o /tmp/radar/repo/Iris/.lake/packages/batteries/.lake/build/ir/Batteries/Classes/Cast.c.o.export /tmp/radar/repo/Iris/.lake/packages/batteries/.lake/build/ir/Batteries/Classes/Cast.c -I /tmp/radar/repo/scripts/bench/build/fake-root/include -fstack-clash-protection -ffp-contract=off -fdata-sections -ffunction-sections -fPIC -fvisibility=hidden -Wno-unused-command-line-argument -O3 -DNDEBUG -DLEAN_EXPORTING
[00:00:19] [0.324] info: stderr:
[00:00:19] [0.324] /tmp/radar/repo/Iris/.lake/packages/batteries/.lake/build/ir/Batteries/Classes/Cast.c:4:10: fatal error: 'lean/lean.h' file not found
[00:00:19] [0.324]     4 | #include <lean/lean.h>
[00:00:19] [0.324]       |          ^~~~~~~~~~~~~
[00:00:19] [0.324] 1 error generated.
[00:00:19] [0.324] error: external command 'cc' exited with code 1

Do you have an idea what the problem could be?

Garmelon · 2026-10-23T13:47:31Z

You may need similar adaptations to leanprover-community/mathlib4@81648b8

MackieLoeffel · 2026-10-23T13:51:25Z

Thanks for the quick response! I will try that.

MackieLoeffel · 2026-10-23T13:51:30Z

!bench

leanprover-radar · 2026-10-23T13:52:31Z

Benchmark results for b25f630 against 9a4ae0d are in. There are significant results. @MackieLoeffel

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Runner for run main has different system configurations between commits.

🟥 main exited with code 1

No significant changes detected.

MackieLoeffel · 2026-10-23T14:02:35Z

This helped, but something is still broken: https://radar.lean-lang.org/repos/iris-lean/commits/b25f630d9b284dc29b4bd2ad993490359232bf6c/runs/main

[00:01:28] + /tmp/radar/repo/scripts/bench/build/lakeprof_measurements.py /tmp/radar/repo/measurements.jsonl
[00:01:28] Traceback (most recent call last):
[00:01:28]   File "/nix/store/8mqqnbvp689slfi0mcylfs3lkm4z9m3p-lakeprof/bin/.lakeprof-wrapped", line 9, in <module>
[00:01:28]     sys.exit(lakeprof())
[00:01:28]              ~~~~~~~~^^
[00:01:28]   File "/nix/store/gvs7q12a9n2qnma36q0rrlaz16za53a3-python3.13-click-8.3.1/lib/python3.13/site-packages/click/core.py", line 1485, in __call__
[00:01:28]     return self.main(*args, **kwargs)
[00:01:28]            ~~~~~~~~~^^^^^^^^^^^^^^^^^
[00:01:28]   File "/nix/store/gvs7q12a9n2qnma36q0rrlaz16za53a3-python3.13-click-8.3.1/lib/python3.13/site-packages/click/core.py", line 1406, in main
[00:01:28]     rv = self.invoke(ctx)
[00:01:28]   File "/nix/store/gvs7q12a9n2qnma36q0rrlaz16za53a3-python3.13-click-8.3.1/lib/python3.13/site-packages/click/core.py", line 1873, in invoke
[00:01:28]     return _process_result(sub_ctx.command.invoke(sub_ctx))
[00:01:28]                            ~~~~~~~~~~~~~~~~~~~~~~^^^^^^^^^
[00:01:28]   File "/nix/store/gvs7q12a9n2qnma36q0rrlaz16za53a3-python3.13-click-8.3.1/lib/python3.13/site-packages/click/core.py", line 1269, in invoke
[00:01:28]     return ctx.invoke(self.callback, **ctx.params)
[00:01:28]            ~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[00:01:28]   File "/nix/store/gvs7q12a9n2qnma36q0rrlaz16za53a3-python3.13-click-8.3.1/lib/python3.13/site-packages/click/core.py", line 824, in invoke
[00:01:28]     return callback(*args, **kwargs)
[00:01:28]   File "/nix/store/8mqqnbvp689slfi0mcylfs3lkm4z9m3p-lakeprof/lib/python3.13/site-packages/lakeprof.py", line 144, in report
[00:01:28]     g = parse(input)
[00:01:28]   File "/nix/store/8mqqnbvp689slfi0mcylfs3lkm4z9m3p-lakeprof/lib/python3.13/site-packages/lakeprof.py", line 116, in parse
[00:01:28]     add_dep(g, drv, drv[:-4])
[00:01:28]     ~~~~~~~^^^^^^^^^^^^^^^^^^
[00:01:28]   File "/nix/store/8mqqnbvp689slfi0mcylfs3lkm4z9m3p-lakeprof/lib/python3.13/site-packages/lakeprof.py", line 99, in add_dep
[00:01:28]     g.nodes[n]["start"] = max(g.nodes[n]["start"], g.nodes[m]["stop"])
[00:01:28]                                                    ~~~~~~~^^^
[00:01:28]   File "/nix/store/v7jm15j9sp5x38sg9vqfls4096bh6a9w-python3.13-networkx-3.6.1/lib/python3.13/site-packages/networkx/classes/reportviews.py", line 196, in __getitem__
[00:01:28]     return self._nodes[n]
[00:01:28]            ~~~~~~~~~~~^^^
[00:01:28] KeyError: 'Batteries.Classes.Cast'

Please let me know if you have any idea what could be going on here. I have to stop for today, but might look into this next week.

Garmelon · 2026-10-26T19:40:11Z

Maybe a bug in https://github.com/Kha/lakeprof/?

MackieLoeffel · 2026-10-27T08:06:25Z

!bench

leanprover-radar · 2026-10-27T08:07:01Z

Benchmark results for 98db22b against 3f808f5 are in. There are significant results. @MackieLoeffel

🟥 main exited with code 1

No significant changes detected.

MackieLoeffel · 2026-10-27T08:32:37Z

!bench

leanprover-radar · 2026-10-27T08:34:15Z

Benchmark results for bbcf15c against 3f808f5 are in. There are significant results. @MackieLoeffel

🟥 build//instructions: +424.3G (+16.69%)

Large changes (1🟥)

1 hidden

Small changes (241✅)

✅ build/module/Iris.Algebra.Agree//instructions: -390.3M (-3.28%)
✅ build/module/Iris.Algebra.Auth//instructions: -363.2M (-2.43%)
✅ build/module/Iris.Algebra.BigOp//instructions: -395.5M (-2.23%)
✅ build/module/Iris.Algebra.CMRA//instructions: -627.4M (-0.93%)
✅ build/module/Iris.Algebra.CMRABigOp//instructions: -310.6M (-15.88%)
✅ build/module/Iris.Algebra.COFESolver//instructions: -342.6M (-2.62%)
✅ build/module/Iris.Algebra.Chain//instructions: -316.0M (-9.11%)
✅ build/module/Iris.Algebra.Csum//instructions: -381.6M (-1.16%)
✅ build/module/Iris.Algebra.DFrac//instructions: -351.1M (-1.93%)
✅ build/module/Iris.Algebra.DynReservationMap//instructions: -367.7M (-2.55%)
✅ build/module/Iris.Algebra.Excl//instructions: -334.7M (-6.18%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.Frac//instructions: -333.6M (-4.46%)
✅ build/module/Iris.Algebra.Functions//instructions: -316.0M (-7.80%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.GenMap//instructions: -337.6M (-2.56%)
✅ build/module/Iris.Algebra.Heap//instructions: -407.9M (-1.19%)
✅ build/module/Iris.Algebra.HeapView//instructions: -365.8M (-1.58%)
✅ build/module/Iris.Algebra.IProp//instructions: -312.2M (-9.22%)
✅ build/module/Iris.Algebra.IsOp//instructions: -317.0M (-17.99%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizMultiSet//instructions: -323.5M (-9.96%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizSet//instructions: -370.3M (-4.13%)
and 221 more

MackieLoeffel · 2026-10-27T08:40:40Z

!bench

leanprover-radar · 2026-10-27T08:41:41Z

Benchmark results for 0a57994 against 3f808f5 are in. There are significant results. @MackieLoeffel

🟥 build//instructions: +10.9G (+0.43%)

Small changes (242✅)

✅ build/module/Iris.Algebra.Agree//instructions: -390.1M (-3.28%)
✅ build/module/Iris.Algebra.Auth//instructions: -361.2M (-2.41%)
✅ build/module/Iris.Algebra.BigOp//instructions: -394.2M (-2.22%)
✅ build/module/Iris.Algebra.CMRA//instructions: -622.6M (-0.92%)
✅ build/module/Iris.Algebra.CMRABigOp//instructions: -310.5M (-15.87%)
✅ build/module/Iris.Algebra.COFESolver//instructions: -344.0M (-2.63%)
✅ build/module/Iris.Algebra.Chain//instructions: -315.9M (-9.11%)
✅ build/module/Iris.Algebra.Csum//instructions: -383.2M (-1.16%)
✅ build/module/Iris.Algebra.DFrac//instructions: -351.4M (-1.94%)
✅ build/module/Iris.Algebra.DynReservationMap//instructions: -371.1M (-2.57%)
✅ build/module/Iris.Algebra.Excl//instructions: -335.4M (-6.19%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.Frac//instructions: -334.5M (-4.47%)
✅ build/module/Iris.Algebra.Functions//instructions: -315.9M (-7.80%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.GenMap//instructions: -341.2M (-2.59%)
✅ build/module/Iris.Algebra.Heap//instructions: -410.8M (-1.20%)
✅ build/module/Iris.Algebra.HeapView//instructions: -368.5M (-1.60%)
✅ build/module/Iris.Algebra.IProp//instructions: -312.4M (-9.23%)
✅ build/module/Iris.Algebra.IsOp//instructions: -316.9M (-17.98%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizMultiSet//instructions: -323.0M (-9.95%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizSet//instructions: -370.3M (-4.13%)
and 222 more

MackieLoeffel · 2026-10-27T08:49:24Z

Using precompileLibrary = true gives a 50% speedup in the tactics testfile 🎉 : https://radar.lean-lang.org/repos/iris-lean/commits/bbcf15ccec8cecd0a835e725f87f4bbfe5a5edc0?reference=0a5799410947026ee68762bc657172b58a98f741&s=IrisTest.Tactics
(Though not sure why this does not show up on the notable results on that page.)

MackieLoeffel · 2026-10-27T09:51:01Z

!bench

leanprover-radar · 2026-10-27T09:52:00Z

Benchmark results for c7015b2 against 3f808f5 are in. There are significant results. @MackieLoeffel

🟥 build//instructions: +424.4G (+16.69%)

Large changes (1🟥)

1 hidden

Small changes (242✅)

✅ build/module/Iris.Algebra.Agree//instructions: -391.1M (-3.28%)
✅ build/module/Iris.Algebra.Auth//instructions: -360.7M (-2.41%)
✅ build/module/Iris.Algebra.BigOp//instructions: -393.1M (-2.21%)
✅ build/module/Iris.Algebra.CMRA//instructions: -633.0M (-0.93%)
✅ build/module/Iris.Algebra.CMRABigOp//instructions: -310.4M (-15.87%)
✅ build/module/Iris.Algebra.COFESolver//instructions: -344.1M (-2.63%)
✅ build/module/Iris.Algebra.Chain//instructions: -316.2M (-9.11%)
✅ build/module/Iris.Algebra.Csum//instructions: -377.2M (-1.15%)
✅ build/module/Iris.Algebra.DFrac//instructions: -352.8M (-1.94%)
✅ build/module/Iris.Algebra.DynReservationMap//instructions: -371.9M (-2.58%)
✅ build/module/Iris.Algebra.Excl//instructions: -334.2M (-6.17%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.Frac//instructions: -332.0M (-4.44%)
✅ build/module/Iris.Algebra.Functions//instructions: -316.5M (-7.81%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.GenMap//instructions: -337.7M (-2.56%)
✅ build/module/Iris.Algebra.Heap//instructions: -410.4M (-1.20%)
✅ build/module/Iris.Algebra.HeapView//instructions: -359.3M (-1.56%)
✅ build/module/Iris.Algebra.IProp//instructions: -313.5M (-9.26%)
✅ build/module/Iris.Algebra.IsOp//instructions: -317.0M (-17.99%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizMultiSet//instructions: -323.6M (-9.97%) (reduced significance based on absolute threshold)
✅ build/module/Iris.Algebra.LeibnizSet//instructions: -370.4M (-4.13%)
and 222 more

See leanprover/lean4#15015

Garmelon mentioned this pull request Oct 26, 2026

chore: update bench suite #728

Merged

MackieLoeffel force-pushed the precompileLibrary branch from b25f630 to 98db22b Compare October 27, 2026 08:05

MackieLoeffel force-pushed the precompileLibrary branch from 47c5a44 to c7015b2 Compare October 27, 2026 09:49

MackieLoeffel added 2 commits October 27, 2026 10:57

feat: enable precompileLibrary for Iris

0e9dff3

See leanprover/lean4#15015

feat: include IrisTest in the benchmark

d8bccda

MackieLoeffel force-pushed the precompileLibrary branch from c7015b2 to 81a25bc Compare October 27, 2026 09:57

try building shared versions

7d482a8

MackieLoeffel force-pushed the precompileLibrary branch from 81a25bc to 7d482a8 Compare October 27, 2026 09:58

MackieLoeffel merged commit e0a0990 into master Oct 27, 2026
5 checks passed

MackieLoeffel deleted the precompileLibrary branch October 27, 2026 12:15

Conversation

MackieLoeffel commented Oct 21, 2026

Description

Uh oh!

MackieLoeffel commented Oct 21, 2026

Uh oh!

leanprover-radar commented Oct 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 23, 2026

Uh oh!

leanprover-radar commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 23, 2026

Uh oh!

Garmelon commented Oct 23, 2026

Uh oh!

MackieLoeffel commented Oct 23, 2026

Uh oh!

MackieLoeffel commented Oct 23, 2026

Uh oh!

leanprover-radar commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 23, 2026

Uh oh!

Garmelon commented Oct 26, 2026

Uh oh!

MackieLoeffel commented Oct 27, 2026

Uh oh!

leanprover-radar commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 27, 2026

Uh oh!

leanprover-radar commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 27, 2026

Uh oh!

leanprover-radar commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MackieLoeffel commented Oct 27, 2026

Uh oh!

MackieLoeffel commented Oct 27, 2026

Uh oh!

leanprover-radar commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-radar commented Oct 21, 2026 •

edited

Loading

leanprover-radar commented Oct 23, 2026 •

edited

Loading

leanprover-radar commented Oct 23, 2026 •

edited

Loading

leanprover-radar commented Oct 27, 2026 •

edited

Loading

leanprover-radar commented Oct 27, 2026 •

edited

Loading

leanprover-radar commented Oct 27, 2026 •

edited

Loading

leanprover-radar commented Oct 27, 2026 •

edited

Loading