chore: remove IR elim dead branches

[hargoniX]

This PR removes the old ElimDeadBranches pass and shifts the new one past lambda lifting.

The reason for dropping the old one is its general unsoundness and the fact that we want to do refactorings on the IR part. The reason for shifting the current pass past lambda lifting, is that its analysis is imprecise in the presence of local function symbols. I experimented with the exact placement for a while and it seems like it is optimal here. Overall we observe a slight regression in the amount of C code generated, likely because we don't propagate information into lambdas before lifting them anymore. But generally measure a slight performance improvement in general.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 9859f04 against 9895e25 are in! @hargoniX

Major changes (9)

• ✅ hashmap.lean//instructions: -73.9M (-1.9%)
• ✅ riscv-ast.lean//instructions: -2.7G (-1.9%)
• 🟥 size/all/.c//lines: +266.6k (+2.3%)
• 🟥 size/all/.ir//bytes: +5MiB (+1.6%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.8%)
• 🟥 size/libleanshared.so//bytes: +3MiB (+1.7%)
• 🟥 tests/compiler//sum binary sizes: +27.6M (+1.5%)
• 🟥 treemap.lean//instructions: +713.0M (+3.1%)
• 🟥 unionfind//instructions: +296.1M (+1.2%)

Minor changes (2)

• ✅ build//instructions: -39.3G (-0.3%)
• ✅ size/init/.olean.private//bytes: -785kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 4283d2b against 9895e25 are in! @hargoniX

Major changes (6)

• ✅ riscv-ast.lean//instructions: -2.8G (-2.0%)
• 🟥 size/all/.c//lines: +181.2k (+1.6%)
• 🟥 size/all/.ir//bytes: +4MiB (+1.2%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.9%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+1.3%)
• 🟥 tests/compiler//sum binary sizes: +19.9M (+1.1%)

Minor changes (1)

• ✅ size/init/.olean.private//bytes: -783kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for c04971e against 9895e25 are in! @hargoniX

Runs (2)

• 🟥 build exited with code 2
• 🟥 other exited with code 2

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d90a1bb against 9895e25 are in! @hargoniX

Major changes (5)

• ✅ riscv-ast.lean//instructions: -2.8G (-2.0%)
• 🟥 size/all/.c//lines: +100.3k (+0.9%)
• 🟥 size/all/.ir//bytes: +2MiB (+0.7%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.8%)
• 🟥 size/libleanshared.so//bytes: +1MiB (+0.7%)

Minor changes (3)

• ✅ build//instructions: -17.7G (-0.1%)
• ✅ size/init/.olean.private//bytes: -787kiB (-0.4%)
• 🟥 tests/compiler//sum binary sizes: +10.8M (+0.6%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 7bb7386 against 7219616 are in! @hargoniX

Major changes (5)

• ✅ riscv-ast.lean//instructions: -2.8G (-2.0%)
• 🟥 size/all/.c//lines: +100.3k (+0.9%)
• 🟥 size/all/.ir//bytes: +2MiB (+0.7%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.8%)
• 🟥 size/libleanshared.so//bytes: +1MiB (+0.7%)

Minor changes (3)

• ✅ build//instructions: -14.9G (-0.1%)
• ✅ size/init/.olean.private//bytes: -786kiB (-0.4%)
• 🟥 tests/compiler//sum binary sizes: +10.9M (+0.6%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 8075324 against 7219616 are in! @hargoniX

Major changes (6)

• ✅ riscv-ast.lean//instructions: -1.7G (-1.3%)
• 🟥 size/all/.c//lines: +123.2k (+1.1%)
• 🟥 size/all/.ir//bytes: +3MiB (+0.9%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.9%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+0.9%)
• 🟥 tests/compiler//sum binary sizes: +14.0M (+0.8%)

Minor changes (1)

• ✅ size/init/.olean.private//bytes: -786kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 70a901a against 7219616 are in! @hargoniX

Major changes (5)

• ✅ riscv-ast.lean//instructions: -2.8G (-2.0%)
• 🟥 size/all/.c//lines: +100.3k (+0.9%)
• 🟥 size/all/.ir//bytes: +2MiB (+0.7%)
• ✅ size/all/.olean.private//bytes: -9MiB (-0.8%)
• 🟥 size/libleanshared.so//bytes: +1MiB (+0.7%)

Minor changes (3)

• ✅ build//instructions: -16.4G (-0.1%)
• ✅ size/init/.olean.private//bytes: -786kiB (-0.4%)
• 🟥 tests/compiler//sum binary sizes: +10.9M (+0.6%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 17:15:55)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 72196169b679949b3a19d6c69b80189562cd5b7f --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-10 17:15:57)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 02bcd71 against 7219616 are in! @hargoniX

Major changes (10)

• ✅ hashmap.lean//instructions: -73.8M (-1.9%)
• 🟥 lake build no-op//instructions: +130.8M (+2.1%)
• ✅ riscv-ast.lean//instructions: -2.6G (-1.9%)
• 🟥 size/all/.c//lines: +231.7k (+2.0%)
• 🟥 size/all/.ir//bytes: +5MiB (+1.4%)
• ✅ size/all/.olean.private//bytes: -8MiB (-0.8%)
• 🟥 size/libleanshared.so//bytes: +3MiB (+1.5%)
• 🟥 tests/compiler//sum binary sizes: +24.5M (+1.3%)
• 🟥 treemap.lean//instructions: +713.2M (+3.1%)
• 🟥 unionfind//instructions: +296.5M (+1.2%)

Minor changes (2)

• ✅ build//instructions: -38.8G (-0.3%)
• ✅ size/init/.olean.private//bytes: -788kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 0aaebea against 7219616 are in! @hargoniX

Major changes (9)

• ✅ build//instructions: -44.7G (-0.3%)
• ✅ hashmap.lean//instructions: -73.6M (-1.9%)
• 🟥 phashmap.lean//instructions: +153.9M (+1.5%)
• ✅ riscv-ast.lean//instructions: -2.7G (-1.9%)
• 🟥 size/all/.c//lines: +169.1k (+1.5%)
• 🟥 size/all/.ir//bytes: +3MiB (+1.0%)
• ✅ size/all/.olean.private//bytes: -10MiB (-0.9%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+1.0%)
• 🟥 tests/compiler//sum binary sizes: +17.4M (+0.9%)

Minor changes (2)

• 🟥 lake config tree//instructions: +9.1M (+0.6%)
• ✅ size/init/.olean.private//bytes: -791kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for f21f0eb against 7219616 are in! @hargoniX

Major changes (8)

• ✅ build//instructions: -43.0G (-0.3%)
• ✅ hashmap.lean//instructions: -73.6M (-1.9%)
• ✅ riscv-ast.lean//instructions: -2.7G (-2.0%)
• 🟥 size/all/.c//lines: +237.6k (+2.1%)
• 🟥 size/all/.ir//bytes: +5MiB (+1.4%)
• ✅ size/all/.olean.private//bytes: -10MiB (-0.9%)
• 🟥 size/libleanshared.so//bytes: +3MiB (+1.5%)
• 🟥 tests/compiler//sum binary sizes: +24.4M (+1.3%)

Minor changes (2)

• 🟥 phashmap.lean//instructions: +82.1M (+0.8%)
• ✅ size/init/.olean.private//bytes: -787kiB (-0.4%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 4bf51c6 against 7219616 are in! @hargoniX

Major changes (9)

• ✅ build//instructions: -44.8G (-0.3%)
• ✅ hashmap.lean//instructions: -73.6M (-1.9%)
• 🟥 phashmap.lean//instructions: +154.6M (+1.5%)
• ✅ riscv-ast.lean//instructions: -2.7G (-1.9%)
• 🟥 size/all/.c//lines: +169.1k (+1.5%)
• 🟥 size/all/.ir//bytes: +3MiB (+1.0%)
• ✅ size/all/.olean.private//bytes: -10MiB (-0.9%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+1.0%)
• 🟥 tests/compiler//sum binary sizes: +17.4M (+0.9%)

Minor changes (1)

• ✅ size/init/.olean.private//bytes: -791kiB (-0.4%)