Skip to content

feat: lake: ModuleLinkInfo & build*Sync#14254

Merged
tydeu merged 3 commits into
leanprover:masterfrom
tydeu:lake/link-info
Jul 3, 2026
Merged

feat: lake: ModuleLinkInfo & build*Sync#14254
tydeu merged 3 commits into
leanprover:masterfrom
tydeu:lake/link-info

Conversation

@tydeu

@tydeu tydeu commented Jul 3, 2026

Copy link
Copy Markdown
Member

This PR adds two new module facets: linkInfoExport and linkInfoNoExport. They provide information on how to link a module. It also provides Sync variants for buildSharedLib, buildLeanSharedLib, and buildLeanExe that work from within a Job rather than across them.

Together, this new API allows custom build targets to link shared libraries or executables from a module without having to copy the code previously in LeanExe.recBuildExe.

@tydeu tydeu added the changelog-lake Lake label Jul 3, 2026
@tydeu tydeu force-pushed the lake/link-info branch from 0ae98a0 to 4c5b16e Compare July 3, 2026 03:31
@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 Jul 3, 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 Jul 3, 2026
@leanprover-bot

leanprover-bot commented Jul 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

@tydeu

tydeu commented Jul 3, 2026

Copy link
Copy Markdown
Member Author

!bench

@tydeu tydeu marked this pull request as ready for review July 3, 2026 04:15
@leanprover-radar

leanprover-radar commented Jul 3, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 4c5b16e against e281ba8 are in. There are significant results. @tydeu

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

Large changes (3🟥)

  • 🟥 compiled/incr_header_load//instructions: +439.1M (+61.12%)
  • 🟥 compiled/incr_header_load//maxrss: +63MiB (+11.36%)
  • 🟥 compiled/incr_header_load//wall-clock: +74ms (+102.14%)

Medium changes (1🟥)

  • 🟥 compiled/incr_header_load//task-clock: +65ms (+56.58%)

Small changes (3✅, 5🟥)

  • 🟥 build/module/Lake.Build.Common//instructions: +420.7M (+1.53%) (reduced significance based on *//lines)
  • ✅ build/module/Lake.Build.Executable//instructions: -2.4G (-69.58%) (reduced significance based on *//lines)
  • 🟥 build/module/Lake.Build.Facets//instructions: +321.5M (+5.51%) (reduced significance based on *//lines)
  • 🟥 build/module/Lake.Build.Infos//instructions: +22.6M (+0.84%)
  • 🟥 build/module/Lake.Build.Module//instructions: +3.4G (+6.81%) (reduced significance based on *//lines)
  • 🟥 compiled/binarytrees//maxrss: +2MiB (+0.77%)
  • ✅ elab/delayed_sharing//wall-clock: -26ms (-6.84%)
  • ✅ vcgen/AddSubCancel/200/kernel//wall-clock: -3ms (-11.54%)

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 3, 2026
Update lean-toolchain for leanprover/lean4#14254
68c147e
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 3, 2026
Update lean-toolchain for leanprover/lean4#14254
7fa5a6d
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 3, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14254
b0ea99d
@tydeu tydeu enabled auto-merge July 3, 2026 04:46
@tydeu tydeu added this pull request to the merge queue Jul 3, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jul 3, 2026
Update lean-toolchain for leanprover/lean4#14254
0b1ad53
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 3, 2026
Update lean-toolchain for leanprover/lean4#14254
bc6d82f
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jul 3, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#14254
951ab40
Merged via the queue into leanprover:master with commit 41b2fe8 Jul 3, 2026
18 checks passed
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jul 3, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 3, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

@tydeu tydeu deleted the lake/link-info branch July 3, 2026 08:42
This was referenced Jul 7, 2026
Merged
Merged
robsimmons added a commit to leanprover/reference-manual that referenced this pull request Jul 7, 2026
@robsimmons @tydeu
chore: documentation for new Lake options (#883)
7c80d57 
Documents new additions to Lake added in
github.com/leanprover/lean4/issues/14254

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
stepbrobd pushed a commit to stepbrobd/lean4 that referenced this pull request Jul 8, 2026
@robsimmons
chore: fix three spell-check typos (leanprover#14312)
0435373 
This PR fixes spelling errors I ran across updating the reference manual
for leanprover#14254 compatibility
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jul 8, 2026
@tydeu @wkrozowski
feat: lake: ModuleLinkInfo & build*Sync (leanprover#14254)
4a87a40 
This PR adds two new module facets: `linkInfoExport` and
`linkInfoNoExport`. They provide information on how to link a module. It
also provides `Sync` variants for `buildSharedLib`,
`buildLeanSharedLib`, and `buildLeanExe` that work from within a `Job`
rather than across them.

Together, this new API allows custom build targets to link shared
libraries or executables from a module without having to copy the code
previously in `LeanExe.recBuildExe`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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 @leanprover-radar