Skip to content

feat: lake: configurable MACOSX_DEPLOYMENT_TARGET - #14723

Merged
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/macosxDeploymentTarget
Aug 10, 2026
Merged

feat: lake: configurable MACOSX_DEPLOYMENT_TARGET#14723
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/macosxDeploymentTarget

Conversation

@tydeu

@tydeu tydeu commented Aug 9, 2026

Copy link
Copy Markdown
Member

This PR makes the MACOSX_DEPLOYMENT_TARGET configurable via the Lake API -- both across a build and for custom builds of shared libraries or executables. It also includes the target in traces, ensuring a rebuilding if the value changes (e.g., if the environment variable MACOSX_DEPLOYMENT_TARGET is set).

@tydeu tydeu added the changelog-lake Lake label Aug 9, 2026
@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 Aug 9, 2026
@leanprover-bot

leanprover-bot commented Aug 9, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-09 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-08-09 19:25:58)
  • ✅ Reference manual branch lean-pr-testing-14723 has successfully built against this PR. (2026-08-09 23:51:51) View Log
  • 🟡 Reference manual branch lean-pr-testing-14723 build against this PR didn't complete normally. (2026-08-09 23:53:03) View Log

@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 Aug 9, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Aug 9, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 9, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

@tydeu tydeu added the macos-arm-ci Build for darwin_aarch64 in CI label Aug 9, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 9, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 9, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Aug 9, 2026
@tydeu
tydeu marked this pull request as ready for review August 10, 2026 03:14
@tydeu
tydeu added this pull request to the merge queue Aug 10, 2026
Merged via the queue into leanprover:master with commit 294cedf Aug 10, 2026
60 checks passed
@tydeu
tydeu deleted the lake/macosxDeploymentTarget branch August 10, 2026 04:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake macos-arm-ci Build for darwin_aarch64 in CI 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

Development

Successfully merging this pull request may close these issues.

2 participants