Skip to content

fix(Lake): load missing dynlibs individually with precompileModules#14326

Draft
Vtec234 wants to merge 1 commit into
masterfrom
lake-more-plugins
Draft

fix(Lake): load missing dynlibs individually with precompileModules#14326
Vtec234 wants to merge 1 commit into
masterfrom
lake-more-plugins

Conversation

@Vtec234

@Vtec234 Vtec234 commented Jul 8, 2026

Copy link
Copy Markdown
Member

No description provided.

@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 Jul 8, 2026
@mathlib-lean-pr-testing

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

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80be7b312023d7c0a6376e33c50aeca1c483e4db --onto e90c70fdd7d0cb1b39ab5380a75950b416f11638. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-08 16:20:58)

@leanprover-bot

leanprover-bot commented Jul 8, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 80be7b312023d7c0a6376e33c50aeca1c483e4db --onto 41b2fe837a74f3d3449816e58dd6219eac034ff7. You can force reference manual CI using the force-manual-ci label. (2026-07-08 16:20:59)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu Awaiting requested review from tydeu tydeu will be requested when the pull request is marked ready for review tydeu is a code owner

Assignees

No one assigned

Labels

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.

2 participants

@Vtec234 @leanprover-bot