Skip to content

feat: lake: separate leanir job - #14906

Open
tydeu wants to merge 7 commits into
leanprover:masterfrom
tydeu:lake/ir-arts
Open

feat: lake: separate leanir job #14906
tydeu wants to merge 7 commits into
leanprover:masterfrom
tydeu:lake/ir-arts

Conversation

@tydeu

@tydeu tydeu commented Aug 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This PR splits leanir code generation into a separate Lake job and target . The leanArts facet on modules and libraries id deprecated and replaced with two distinct facets: elabArts and irArts. For backwards compatibility, uses of leanArts delegate to irArts.

When the Lean option compiler.postponeCompiler is enabled, only *.olean files are produced by the initial Lean elaboration (elabArts). Code generation then occurs in the subsequent irArts job that calls leanir to emit .c , .ir, and .ir.sig files for the module. This job traces solely the .ir.sig files of the import graph (along with module's own elaboration results) and only needs to rehuild when they change.

Because #eval in the server needs IR, and Lake does not currently distinguish between server and CLI builds, module elaboration still waits for the IR of its imports to be built. However, this is now more clearly demarcated in the code by fetchExportInfo and could evolve in the future if a separate serverExportInfo is developed.

A test of postponed compilation is added as moduleCodegen.

Split from #13169.

@tydeu tydeu added the changelog-lake Lake label Aug 24, 2026
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Aug 28, 2026
@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Aug 28, 2026
@leanprover-bot

leanprover-bot commented Aug 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

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

mathlib-lean-pr-testing Bot commented Aug 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
3d9c85d
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
2cbdcdb
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
be48789
@tydeu
tydeu force-pushed the lake/ir-arts branch 2 times, most recently from 45e7ece to 14bc481 Compare August 29, 2026 01:51
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
838aaaf
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 29, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
cfadcd4
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 29, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
95e3d5b
@tydeu
tydeu marked this pull request as ready for review August 29, 2026 03:14
@tydeu
tydeu requested a review from Kha August 29, 2026 03:15
tydeu
tydeu commented Aug 29, 2026
View reviewed changes
Comment thread src/LeanIR.lean Outdated
Comment on lines +94 to +96
-- As the environment imports the module to compile, it does not inherit its package.
-- Take it from the setup.
let env := env.setModulePackage setup.package?

@tydeu tydeu Aug 29, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Kha This changes non-Lake code and is thus probably the bit that most needs your review.

@Kha Kha Aug 31, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment confused me at first, it made it sound like an importModules edge case when processHeaderCore is the one otherwise setting this field. No comment needed I think, just like for setMainModule

tydeu
tydeu commented Aug 29, 2026
View reviewed changes
Comment thread src/lake/Lake/Build/Module.lean
Kha
Kha approved these changes Aug 31, 2026
View reviewed changes
Comment thread src/LeanIR.lean Outdated
Comment on lines +94 to +96
-- As the environment imports the module to compile, it does not inherit its package.
-- Take it from the setup.
let env := env.setModulePackage setup.package?

@Kha Kha Aug 31, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The comment confused me at first, it made it sound like an importModules edge case when processHeaderCore is the one otherwise setting this field. No comment needed I think, just like for setMainModule

Comment thread src/lake/Lake/Build/Module.lean
Comment thread src/lake/Lake/Build/Module.lean Outdated
Comment thread tests/lake/tests/moduleCodegen/test.sh
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 31, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
41861ed
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 31, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
593833a
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 31, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
75cd42e
@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 Aug 31, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 31, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
1082758
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 31, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
28cbc32
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Aug 31, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
b174844
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 1, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
d331401
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 1, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
1f1228b
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 1, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
0f26b54
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 5, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
1f27847
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 5, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
f2a4f25
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 5, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
33fba05
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 5, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Sep 5, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
c7a6a30
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 5, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#14906
4fc5fe2
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 5, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14906
080c724
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha approved these changes

Assignees

No one assigned

Labels

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake 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

@tydeu @leanprover-bot @Kha