chore: re-enable LLVM CI by hargoniX · Pull Request #13700 · leanprover/lean4

hargoniX · 2026-05-11T08:15:47Z

No description provided.

mathlib-lean-pr-testing · 2026-05-11T09:59:28Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2229b077d6ebd2ff42d665fe1c32501df8915dff --onto a71f158f7bd96ff9ea846f7ff4cc658de3c8b0f9. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-11 09:59:28)
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-11 20:52:47) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-11 23:12:40) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-12 23:57:12) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-13 14:48:52) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-13 23:16:10) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-14 00:14:35) View Log
✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-14 01:15:18) View Log

leanprover-bot · 2026-05-11T09:59:30Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2229b077d6ebd2ff42d665fe1c32501df8915dff --onto a71f158f7bd96ff9ea846f7ff4cc658de3c8b0f9. You can force reference manual CI using the force-manual-ci label. (2026-05-11 09:59:29)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-11 19:57:40)
✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-12 23:09:44) View Log
🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-12 23:11:36) View Log
✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-13 13:58:12) View Log
🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-13 13:59:20) View Log
✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-13 22:29:20) View Log
🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-13 22:30:51) View Log
✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-13 23:27:53) View Log
🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-13 23:29:33) View Log
✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-14 00:23:08) View Log
🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-14 00:23:31) View Log

fix fix

hargoniX · 2026-05-12T22:08:03Z

!bench

leanprover-radar · 2026-05-12T22:08:10Z

Benchmark results for 5d63f74 against 2229b07 are in. There are significant results. @hargoniX

🟥 build exited with code 1
🟥 other exited with code 1

No significant changes detected.

hargoniX · 2026-05-12T22:12:55Z

!bench

leanprover-radar · 2026-05-13T11:43:05Z

Benchmark results for c5f8dc8 against 2229b07 are in. There are significant results. @hargoniX

🟥 build exited with code 1

Large changes (7✅, 10🟥)

🟥 compiled/ilean_roundtrip//instructions: +138.7M (+0.59%)
✅ compiled/nat_repr//instructions: -548.5M (-1.39%)
🟥 compiled/phashmap//instructions: +71.7M (+0.81%)
🟥 lake/inundation/build clean//instructions: +213.2G (+13.71%)
🟥 lake/inundation/build clean//wall-clock: +2s (+7.80%)
🟥 lake/inundation/config elab//instructions: +69.8M (+2.89%)
🟥 lake/inundation/config import//instructions: +70.6M (+5.82%)
🟥 lake/inundation/config tree//instructions: +70.2M (+5.63%)
🟥 lake/inundation/env//instructions: +72.1M (+5.84%)
🟥 lake/inundation/startup//instructions: +66.7M (+34.75%)
🟥 misc/import Lean//instructions: +72.0M (+4.82%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -21s (-24.29%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//wall-clock: -4s (-17.41%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//instructions: -318.1G (-65.14%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//task-clock: -40s (-64.10%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//wall-clock: -15s (-69.21%)
✅ size/compile/.out//bytes: -23MiB (-1.16%)

Medium changes (3✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (4✅, 20🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX · 2026-05-13T12:02:04Z

!bench

leanprover-radar · 2026-05-13T12:02:12Z

Benchmark results for d129997 against 2229b07 are in. There are significant results. @hargoniX

🟥 build exited with code 1

Large changes (7✅, 11🟥)

🟥 compiled/ilean_roundtrip//instructions: +137.9M (+0.59%)
✅ compiled/nat_repr//instructions: -548.5M (-1.39%)
🟥 compiled/phashmap//instructions: +71.0M (+0.80%)
🟥 lake/inundation/build clean//instructions: +214.9G (+13.82%)
🟥 lake/inundation/build clean//task-clock: +44s (+8.69%)
🟥 lake/inundation/build clean//wall-clock: +2s (+8.04%)
🟥 lake/inundation/config elab//instructions: +69.0M (+2.86%)
🟥 lake/inundation/config import//instructions: +70.8M (+5.84%)
🟥 lake/inundation/config tree//instructions: +70.7M (+5.68%)
🟥 lake/inundation/env//instructions: +71.3M (+5.77%)
🟥 lake/inundation/startup//instructions: +66.9M (+34.89%)
🟥 misc/import Lean//instructions: +72.2M (+4.84%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -21s (-23.96%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//wall-clock: -4s (-16.39%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//instructions: -317.0G (-64.93%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//task-clock: -40s (-63.40%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//wall-clock: -15s (-68.75%)
✅ size/compile/.out//bytes: -23MiB (-1.16%)

Medium changes (3✅, 17🟥)

🟥 compiled/server_startup//instructions: +39.6M (+10.93%)
✅ compiled/watchdogRss//instructions: -182.9M (-0.72%)
🟥 elab/big_beq_rec//instructions: +143.6M (+0.88%)
🟥 elab/big_deceq//instructions: +74.2M (+1.66%)
🟥 elab/big_deceq_rec//instructions: +76.1M (+1.28%)
✅ elab/big_do//instructions: -80.7M (-0.37%)
🟥 elab/big_match//instructions: +66.2M (+0.61%)
🟥 elab/big_match_nat//instructions: +73.9M (+1.47%)
🟥 elab/big_struct//instructions: +63.7M (+2.46%)
🟥 elab/big_struct_dep1//instructions: +66.7M (+1.24%)
🟥 elab/cbv_dedup//instructions: +67.3M (+2.01%)
🟥 elab/delayed_assign//instructions: +75.8M (+2.10%)
🟥 elab/delayed_sharing//instructions: +77.0M (+2.62%)
🟥 elab/grind_ring_5//instructions: +60.8M (+0.71%)
🟥 elab/iterators//instructions: +63.6M (+2.40%)
🟥 elab/omega_stress//instructions: +66.8M (+1.68%)
🟥 elab/simp_arith1//instructions: +65.7M (+2.85%)
🟥 elab/string_simp_ne//instructions: +75.9M (+1.29%)
🟥 interpreted/iterators//instructions: +64.5M (+0.18%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//instructions: -150.0G (-20.66%)

Small changes (4✅, 21🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX · 2026-05-13T12:50:26Z

!bench

leanprover-radar · 2026-05-13T12:50:44Z

Benchmark results for 6578b52 against 2229b07 are in. There are significant results. @hargoniX

🟥 build//instructions: +7.0T (+61.08%)

Large changes (8✅, 15🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (3✅, 19🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (4✅, 24🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX · 2026-05-13T21:23:59Z

!bench

leanprover-radar · 2026-05-13T21:24:09Z

Benchmark results for 7f7d684 against 2229b07 are in. There are significant results. @hargoniX

🟥 build//instructions: +6.8T (+58.99%)

Large changes (8✅, 14🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (3✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (5✅, 19🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX · 2026-05-13T21:40:47Z

Comparison to previous commit, already a step in the right direction: https://radar.lean-lang.org/repos/lean4/commits/7f7d684e1b891b8cb89ad324f425e8b21ead82d1?reference=6578b52540126fc4bde3f38aeb530b108ae084c0

hargoniX · 2026-05-13T22:32:06Z

!bench

leanprover-radar · 2026-05-13T22:32:14Z

Benchmark results for 75f6e01 against 2229b07 are in. There are significant results. @hargoniX

🟥 build//instructions: +6.5T (+56.90%)

Large changes (9✅, 6🟥)

🟥 build//instructions: +6.5T (+56.90%)
🟥 build//task-clock: +21m 3s (+61.93%)
🟥 build//wall-clock: +48s (+31.31%)
🟥 compiled/ilean_roundtrip//instructions: +138.6M (+0.59%)
✅ compiled/nat_repr//instructions: -548.3M (-1.39%)
🟥 compiled/phashmap//instructions: +71.1M (+0.80%)
🟥 lake/inundation/build clean//instructions: +138.8G (+8.93%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -22s (-25.00%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//wall-clock: -5s (-18.18%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//instructions: -318.1G (-65.14%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//task-clock: -40s (-64.10%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//wall-clock: -15s (-69.48%)
✅ size/compile/.out//bytes: -107MiB (-5.41%)
✅ size/install//bytes: -39MiB (-1.32%)
✅ size/libleanshared.so//bytes: -14MiB (-9.67%)

and 1 hidden

Medium changes (3✅, 8🟥)

🟥 compiled/parser//task-clock: +239ms (+11.32%)
🟥 compiled/parser//wall-clock: +239ms (+11.31%)
✅ compiled/watchdogRss//instructions: -206.4M (-0.81%)
✅ elab/big_do//instructions: -126.6M (-0.57%)
🟥 lake/inundation/build clean//wall-clock: +1s (+5.35%)
🟥 lake/inundation/config import//instructions: +22.1M (+1.83%)
🟥 lake/inundation/config tree//instructions: +21.8M (+1.75%)
🟥 lake/inundation/startup//instructions: +17.7M (+9.25%)
🟥 misc/import Lean//instructions: +26.3M (+1.76%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//instructions: -155.1G (-21.37%)
🟥 size/all/.cpp//lines: +136.0 (+0.47%)

Small changes (6✅, 27🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX · 2026-05-13T22:49:53Z

Again an improvement https://radar.lean-lang.org/repos/lean4/commits/75f6e0115d03f9a881d5772d995faaf3246c819f?reference=7f7d684e1b891b8cb89ad324f425e8b21ead82d1

hargoniX · 2026-05-13T23:30:17Z

!bench

leanprover-radar · 2026-05-13T23:30:35Z

Benchmark results for 393056a against 2229b07 are in. There are significant results. @hargoniX

🟥 build//instructions: +6.5T (+56.98%)

Large changes (9✅, 6🟥)

🟥 build//instructions: +6.5T (+56.98%)
🟥 build//task-clock: +21m 6s (+62.05%)
🟥 build//wall-clock: +48s (+31.46%)
🟥 compiled/ilean_roundtrip//instructions: +139.0M (+0.59%)
✅ compiled/nat_repr//instructions: -548.4M (-1.39%)
🟥 compiled/phashmap//instructions: +71.1M (+0.80%)
🟥 lake/inundation/build clean//instructions: +139.4G (+8.97%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -22s (-24.82%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//wall-clock: -4s (-17.76%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//instructions: -317.1G (-64.94%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//task-clock: -40s (-64.06%)
✅ misc/re-elab watchdog Init.Data.List.Sublist//wall-clock: -15s (-69.24%)
✅ size/compile/.out//bytes: -107MiB (-5.41%)
✅ size/install//bytes: -39MiB (-1.32%)
✅ size/libleanshared.so//bytes: -14MiB (-9.67%)

and 1 hidden

Medium changes (3✅, 7🟥)

✅ compiled/watchdogRss//instructions: -204.8M (-0.80%)
✅ elab/big_do//instructions: -124.7M (-0.56%)
🟥 lake/inundation/build clean//wall-clock: +1s (+5.54%)
🟥 lake/inundation/config import//instructions: +21.7M (+1.79%)
🟥 lake/inundation/config tree//instructions: +21.1M (+1.70%)
🟥 lake/inundation/env//instructions: +22.5M (+1.82%)
🟥 lake/inundation/startup//instructions: +18.1M (+9.44%)
🟥 misc/import Lean//instructions: +25.4M (+1.70%)
✅ misc/re-elab Init.Data.BitVec.Lemmas//instructions: -152.8G (-21.04%)
🟥 size/all/.cpp//lines: +147.0 (+0.51%)

Small changes (5✅, 23🟥)

Too many entries to display here. View the full report on radar instead.

hargoniX added 3 commits May 11, 2026 08:15

chore: re-enable LLVM CI

ad0301e

bump

4f7c21f

bump

93d4aeb

hargoniX force-pushed the hbv/revive_llvm branch from 551cd05 to 93d4aeb Compare May 11, 2026 08:34

plz work

f728c8f

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 11, 2026

hargoniX added 3 commits May 11, 2026 11:07

more

7cd40aa

more

dfa4044

fix llvm

e3440b7

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label May 11, 2026

mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 11, 2026

hargoniX added 2 commits May 11, 2026 21:02

basic LLVM port

c1b8452

shoo

c48fdf5

github-actions Bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label May 11, 2026

fix LLVm

2d4c160

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 11, 2026

Update lean-toolchain for leanprover/lean4#13700

73a3f00

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 11, 2026

Update lean-toolchain for leanprover/lean4#13700

b337d38

hargoniX added 5 commits May 12, 2026 09:19

feat: static closed terms

8977b2d

fix more

bdae32f

self calls

3fd2992

fix fix

fix llvm strings

f76a1cf

chore: update-stage0

22a55ae

hargoniX force-pushed the hbv/revive_llvm branch from 9e7bae7 to 22a55ae Compare May 12, 2026 21:56

bench llvm

5d63f74

pass llvm config?

9df0343

no lakeprof for now

d129997

shoo

6578b52

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

e31c333

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

a3e3be0

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

5075caa

perf: use internal linkage for initializers

7f7d684

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

5240d80

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

e4d0553

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

eb44cfb

perf: nounwind

75f6e01

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

6f9cfe8

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

9f2dccc

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 13, 2026

Update lean-toolchain for leanprover/lean4#13700

7fcddd4

perf: noundef everywhere

393056a

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 14, 2026

Update lean-toolchain for leanprover/lean4#13700

62824bb

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 14, 2026

Update lean-toolchain for leanprover/lean4#13700

ad9d468

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 14, 2026

Update lean-toolchain for leanprover/lean4#13700

0792619

Conversation

hargoniX commented May 11, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented May 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented May 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hargoniX commented May 12, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 12, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

hargoniX commented May 13, 2026

Uh oh!

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

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mathlib-lean-pr-testing Bot commented May 11, 2026 •

edited

Loading

leanprover-bot commented May 11, 2026 •

edited

Loading

leanprover-radar commented May 12, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading

leanprover-radar commented May 13, 2026 •

edited

Loading