Skip to content

fix: add missing dependencies for copy-leancpp target #11809

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
NicolasRouquette wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix: add missing dependencies for copy-leancpp target #11809

NicolasRouquette wants to merge 1 commit into from
+3 −0

Conversation

@NicolasRouquette
Copy link

@NicolasRouquette NicolasRouquette commented Dec 27, 2025 •
edited
Loading

This PR adds missing dependencies in src/CMakeLists.txt to ensure that leanrt_initial-exec, leanrt, and leancpp_1 targets wait for copy-leancpp to complete before building. Fixes potential build race conditions in stage 2+ builds on systems with large nproc.

Closes #11808

@NicolasRouquette
Adds missing dependencies for copy-leancpp target
bebbcff 
Ensures leanrt_initial-exec, leanrt, and leancpp_1 targets
wait for copy-leancpp to complete before building.
Fixes potential build race conditions in stage 2+ builds.
@NicolasRouquette NicolasRouquette changed the title Adds missing dependencies for copy-leancpp target fix: Adds missing dependencies for copy-leancpp target Dec 27, 2025
@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 Dec 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 27, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f483c6c10f6122657fe6ca5ca79708567b0d6686 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-27 02:22:04)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 27, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f483c6c10f6122657fe6ca5ca79708567b0d6686 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force reference manual CI using the force-manual-ci label. (2025-12-27 02:22:06)

@NicolasRouquette NicolasRouquette changed the title fix: Adds missing dependencies for copy-leancpp target fix: add missing dependencies for copy-leancpp target Dec 27, 2025
@NicolasRouquette NicolasRouquette marked this pull request as draft December 27, 2025 02:32
@NicolasRouquette NicolasRouquette marked this pull request as ready for review December 27, 2025 02:33
@NicolasRouquette
Copy link
Author

NicolasRouquette commented Dec 27, 2025

@maintainers Could you please add the changelog-fix label to this PR? Thanks!

@kim-em kim-em added the changelog-no Do not include this PR in the release changelog label Jan 6, 2026
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

changelog-no Do not include this PR in the release changelog 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.

Race condition in lean4 stage2+ builds

4 participants

@NicolasRouquette @leanprover-community-bot @leanprover-bot @kim-em