Skip to content

Conversation

@tobiasgrosser
Copy link
Contributor

@tobiasgrosser tobiasgrosser commented May 14, 2025

This PR enables the build of all artifacts for custom releases, e.g., releases outside the main lean4 repository.

This resolves #8333.

@tobiasgrosser tobiasgrosser requested a review from kim-em as a code owner May 14, 2025 10:15
@tobiasgrosser
Copy link
Contributor Author

I believe this does the right thing, but the merge_group part has not been tested. @Kha, I would appreciate a careful refview.

@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 May 14, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88078930a92aa55089e936a5fe8e99ec65ab2ceb --onto 29cc75531a5a0e8626fa5e96371e7ceb98877782. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-14 10:49:57)

@Kha
Copy link
Member

Kha commented May 14, 2025

Wouldn't it make more sense to use the same level for custom releases as for standard releases, i.e. building all platforms?

@tobiasgrosser
Copy link
Contributor Author

Potentially, but I am a bit unsure how this would translate into code. Alternatively, I guess I can check for github.event_name == 'push' && contains(github.ref, 'refs/tags/'), and the raise the check_level to 2. Is that what you have in mind?

@Kha
Copy link
Member

Kha commented May 14, 2025

Yes, I think you can replace the check for steps.set-release.outputs.RELEASE_TAG with that. But let's get @kim-em's input as well.

This PR enables the build of all artifacts for custom releases, e.g.,
releases outside the main lean4 repository.

This resolves leanprover#8333.
@tobiasgrosser tobiasgrosser force-pushed the fix_ci_macos_aarch64_tagged_builds branch from 7651684 to 4930fac Compare May 14, 2025 19:52
@tobiasgrosser
Copy link
Contributor Author

Yes, I think you can replace the check for steps.set-release.outputs.RELEASE_TAG with that. But let's get @kim-em's input as well.

I introduced a separate step to check for custom releases. This works well, as can be seen here: https://github.com/opencompl/lean4/actions/runs/15029737370

@Kha Kha added the will-merge-soon …unless someone speaks up label May 15, 2025
@Kha Kha added this pull request to the merge queue May 27, 2025
@tobiasgrosser
Copy link
Contributor Author

Thank you!

@tobiasgrosser tobiasgrosser changed the title chore: skip OS X aarch64 CI only in merge groups chore: build of all artifacts (including OS X aarch64) for custom releases May 27, 2025
Merged via the queue into leanprover:master with commit ed6c780 May 27, 2025
23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

The releases built on tags in a forked repo do not include OSX aarch64 builds

3 participants