Skip to content

refactor: port IR.SimpCase to LCNF#12384

Merged
hargoniX merged 3 commits intomasterfrom
hbv/lcnf_simp_cases
Feb 10, 2026
Merged

refactor: port IR.SimpCase to LCNF#12384
hargoniX merged 3 commits intomasterfrom
hbv/lcnf_simp_cases

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Feb 9, 2026

This PR ports the IR SimpCase pass to LCNF.

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for 8f8da43 against d2c738c are in! @hargoniX

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

No significant changes detected.

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@hargoniX hargoniX force-pushed the hbv/lcnf_simp_cases branch from 8f8da43 to 5995b5d Compare February 9, 2026 09:32
@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for 5995b5d against d2c738c are in! @hargoniX

  • 🟥 build//instructions: +2.8G (+0.02%)

Medium changes (2🟥)

  • 🟥 big_match//instructions: +116.6M (+0.99%)
  • 🟥 big_omega.lean//instructions: +78.5M (+0.33%)

Small changes (9✅, 11🟥)

  • 🟥 Init.Data.BitVec.Lemmas//instructions: +147.0M (+0.12%)
  • 🟥 big_beq_rec//instructions: +55.3M (+0.29%)
  • 🟥 big_do//instructions: +13.8M (+0.05%)
  • 🟥 big_match_partial//instructions: +48.4M (+0.30%)
  • 🟥 big_omega.lean MT//instructions: +80.1M (+0.34%)
  • ✅ build/module/Lake.Build.Module//instructions: -135.2M (-0.21%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -757.0M (-53.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -41.7M (-3.68%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: +182.1M (+0.70%)
  • 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Convert//instructions: +27.0M (+0.44%)
  • 🟥 cbv tactic (Eratosthenes' sieve)//instructions: +62.6M (+0.10%)
  • 🟥 grind_list2.lean//instructions: +62.3M (+0.11%)
  • 🟥 grind_ring_5.lean//instructions: +12.0M (+0.13%)
  • ✅ parser//instructions: -26.2M (-0.06%)
  • 🟥 riscv-ast.lean//instructions: +243.4M (+0.23%)
  • ✅ simp_local//instructions: -59.3M (-0.13%)

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 9, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Feb 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026 •
edited
Loading

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

5 similar comments
@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 9, 2026

Benchmark results for d71bfce against d2c738c are in! @hargoniX

  • ✅ build//instructions: -7.7G (-0.06%)

Small changes (8✅, 3🟥)

  • ✅ build/module/Lake.Build.Module//instructions: -197.5M (-0.30%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .ilean: -8kiB (-82.28%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean: -3kiB (-11.86%)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.private: -195kiB (-90.47%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//bytes .olean.server: -2kiB (-58.61%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR.SimpCase//instructions: -755.6M (-53.52%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Compiler.IR//instructions: -43.7M (-3.86%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .ilean: +5kiB (+23.72%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//bytes .olean.private: +140kiB (+25.99%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.AlphaEqv//instructions: +711.8M (+22.45%) (reduced significance based on *//lines)
  • ✅ lake startup//instructions: -2.9M (-1.22%)

@hargoniX hargoniX marked this pull request as ready for review February 9, 2026 18:01
@hargoniX hargoniX requested a review from leodemoura as a code owner February 9, 2026 18:01
@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Feb 9, 2026
@hargoniX hargoniX enabled auto-merge February 9, 2026 18:30
@hargoniX hargoniX added this pull request to the merge queue Feb 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Feb 9, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d2c738c4bd798b484f474d4d7ac5d3fb5ee8ee95 --onto 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-09 19:26:43)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 9, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d2c738c4bd798b484f474d4d7ac5d3fb5ee8ee95 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-09 19:26:45)

@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to no response for status checks Feb 9, 2026
@hargoniX hargoniX added this pull request to the merge queue Feb 10, 2026
Merged via the queue into master with commit 7488201 Feb 10, 2026
23 checks passed
@hargoniX hargoniX deleted the hbv/lcnf_simp_cases branch February 10, 2026 09:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hargoniX @leanprover-radar @leanprover-bot