Skip to content

refactor: port EmitC to LCNF#12781

Merged
hargoniX merged 15 commits intomasterfrom
hbv/lcnf_emitc
Mar 11, 2026
Merged

refactor: port EmitC to LCNF#12781
hargoniX merged 15 commits intomasterfrom
hbv/lcnf_emitc

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Mar 3, 2026 •
edited
Loading

This PR ports the C emission pass from IR to LCNF, marking the last step of the IR/LCNF conversion and thus enabling end-to-end code generation through the new compilation infrastructure.

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 3, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 3, 2026 •
edited
Loading

Benchmark results for 8603954 against cda8470 are in! @hargoniX

Warning

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

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 3, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 3, 2026 •
edited
Loading

Benchmark results for 0caa3c8 against cda8470 are in! @hargoniX

Warning

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

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +71.6G (+0.57%)

Small changes (1✅, 573🟥)

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

@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 Mar 3, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 3, 2026
Update lean-toolchain for testing leanprover/lean4#12781
1a8b95d
@github-actions 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 Mar 3, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 3, 2026
Update lean-toolchain for testing leanprover/lean4#12781
9d26109
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Mar 3, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#12781
3a03f26
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 4, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-12781 has successfully built against this PR. (2026-03-04 00:19:26) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-05 09:32:14)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b500b204cacbb3149f42feda880c8bdfcab7db --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 17:13:42)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e5e7dcc00f18b4b6e10c64998df17e01d3c11645 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 11:14:01)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4450ff89958bd479af79da62fa1949931b81351b --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-11 11:27:45)

@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 4, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2026
Update lean-toolchain for leanprover/lean4#12781
97edec9
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 4, 2026
Update lean-toolchain for leanprover/lean4#12781
b2e01b1
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Mar 4, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#12781
f52b703
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Mar 4, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 4, 2026

Mathlib CI status (docs):

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 5, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-05 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-03-05 09:32:17)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e2b500b204cacbb3149f42feda880c8bdfcab7db --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 17:13:44)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e5e7dcc00f18b4b6e10c64998df17e01d3c11645 --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-10 11:14:03)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4450ff89958bd479af79da62fa1949931b81351b --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-11 11:27:47)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4450ff89958bd479af79da62fa1949931b81351b --onto ff6816a854ef5cf2966519452d03933785f2fdeb. You can force reference manual CI using the force-manual-ci label. (2026-03-11 14:41:50)

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 9, 2026 •
edited
Loading

Benchmark results for 3a9254c against e2b500b are in. Significant changes detected! @Garmelon @hargoniX

  • 🟥 build//instructions: +63.2G (+0.49%)

Large changes (1🟥)

  • 🟥 build/profile/C code generation//wall-clock: +12s (+8541.39%)

Medium changes (1🟥)

  • 🟥 size/all/.c//lines: +49.1k (+0.45%)

Small changes (4✅, 516🟥)

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

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 9, 2026 •
edited
Loading

Benchmark results for 4e63be2 against e2b500b are in. Significant changes detected! @hargoniX

  • 🟥 build//instructions: +57.5G (+0.45%)

Large changes (2🟥)

  • 🟥 build/profile/C code generation//wall-clock: +12s (+8654.37%)
  • 🟥 size/all/.c//lines: +74.6k (+0.68%)

Medium changes (1🟥)

  • 🟥 size/all/.ir//bytes: +2MiB (+0.48%)

Small changes (4✅, 395🟥)

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

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 9, 2026 •
edited
Loading

Benchmark results for 82ddc19 against e2b500b are in. Significant changes detected! @hargoniX

  • 🟥 build//instructions: +24.8G (+0.19%)

Large changes (7🟥)

  • 🟥 build/profile/C code generation//wall-clock: +11s (+7696.63%)
  • 🟥 build/stat/imported bytes//bytes: +2GiB (+5.19%)
  • 🟥 size/Init/.olean//bytes: +3MiB (+2.97%)
  • 🟥 size/all/.c//lines: +78.5k (+0.72%)
  • 🟥 size/all/.olean.private//bytes: +68MiB (+5.85%)
  • 🟥 size/all/.olean//bytes: +23MiB (+7.24%)
  • 🟥 size/install//bytes: +95MiB (+3.90%)

Medium changes (3🟥)

  • 🟥 size/Init/.olean.private//bytes: +1MiB (+0.50%)
  • 🟥 size/all/.ir//bytes: +2MiB (+0.52%)
  • 🟥 size/libleanshared.so//bytes: +624kiB (+0.43%)

Small changes (12✅, 8🟥)

  • ✅ build/module/Lake.CLI.Translate.Lean//instructions: -47.7M (-0.30%)
  • 🟥 build/module/Lean.Compiler.IR.AddExtern//instructions: +103.3M (+9.88%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.Passes//instructions: +18.8M (+0.84%)
  • 🟥 build/module/Lean.Compiler.LCNF.PhaseExt//instructions: +449.7M (+17.93%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.SimpCase//instructions: +53.4M (+2.72%)
  • ✅ build/module/Lean.Compiler.LCNF.Toposort//instructions: -57.1M (-3.42%)
  • ✅ build/module/Lean.Meta.Sym.Simp.EvalGround//instructions: -72.2M (-0.32%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.CommRing//instructions: -10.1M (-0.55%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat//instructions: -10.4M (-0.55%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Linear//instructions: -7.5M (-0.48%)
  • ✅ build/module/Lean.Meta.Tactic.Grind.PropagatorAttr//instructions: -13.5M (-0.66%)
  • ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt//instructions: -61.0M (-0.30%)
  • ✅ build/module/Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt//instructions: -58.2M (-0.39%)
  • 🟥 build/module/Lean.Shell//instructions: +183.4M (+3.19%) (reduced significance based on *//lines)
  • ✅ build/profile/compilation (LCNF impure)//wall-clock: -1s (-4.02%)
  • ✅ compiled/binarytrees.st//task-clock: -184ms (-6.30%)
  • ✅ compiled/binarytrees.st//wall-clock: -184ms (-6.29%)
  • 🟥 compiled/watchdogRss//instructions: +61.9M (+0.24%)
  • 🟥 elab/grind_bitvec2//wall-clock: +182ms (+3.64%)
  • 🟥 size/all/.ilean//bytes: +221kiB (+0.29%)

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 9, 2026 •
edited
Loading

Benchmark results for ed606b1 against e2b500b are in. Significant changes detected! @hargoniX

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

No significant changes detected.

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 9, 2026 •
edited
Loading

Benchmark results for 0e0aed8 against e2b500b are in. Significant changes detected! @hargoniX

  • 🟥 build//instructions: +40.8G (+0.32%)

Large changes (2🟥)

  • 🟥 build/profile/C code generation//wall-clock: +11s (+7740.21%)
  • 🟥 size/all/.c//lines: +78.5k (+0.72%)

Medium changes (2🟥)

  • 🟥 size/all/.ir//bytes: +2MiB (+0.52%)
  • 🟥 size/libleanshared.so//bytes: +624kiB (+0.43%)

Small changes (4✅, 63🟥)

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

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 10, 2026 •
edited
Loading

Benchmark results for f826eeb against e5e7dcc are in. Significant changes detected! @hargoniX

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

Large changes (3🟥)

  • 🟥 build/profile/C code generation//wall-clock: +3s (+38.47%)
  • 🟥 compiled/hashmap//task-clock: +32ms (+17.61%)
  • 🟥 compiled/hashmap//wall-clock: +32ms (+17.61%)

Medium changes (1✅)

  • ✅ elab/big_do//instructions: -77.9M (-0.32%)

Small changes (78✅, 11🟥)

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

@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented Mar 11, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 11, 2026 •
edited
Loading

Benchmark results for 40ebc7d against 4450ff8 are in. Significant changes detected! @hargoniX

  • 🟥 build//instructions: +11.3G (+0.09%)

Large changes (1✅)

  • ✅ lake/inundation/build no-op//instructions: -630.5M (-9.72%)

Medium changes (1✅)

  • ✅ lake/inundation/build no-op//task-clock: -138ms (-21.65%)

Small changes (18✅, 10🟥)

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

@hargoniX hargoniX added the release-ci Enable all CI checks for a PR, like is done for releases label Mar 11, 2026
@hargoniX hargoniX marked this pull request as ready for review March 11, 2026 13:41
@hargoniX hargoniX requested a review from leodemoura as a code owner March 11, 2026 13:41
@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Mar 11, 2026
@hargoniX hargoniX enabled auto-merge March 11, 2026 13:42
@hargoniX hargoniX removed the release-ci Enable all CI checks for a PR, like is done for releases label Mar 11, 2026
@hargoniX hargoniX disabled auto-merge March 11, 2026 13:59
@hargoniX hargoniX added this pull request to the merge queue Mar 11, 2026
Merged via the queue into master with commit 652ca9f Mar 11, 2026
33 of 43 checks passed
@hargoniX hargoniX deleted the hbv/lcnf_emitc branch March 11, 2026 14:48
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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-compiler Compiler, runtime, and FFI mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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