Merge master to nightly #20
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `master`. | |
| name: Merge master to nightly | |
| on: | |
| schedule: | |
| - cron: '30 0 * * *' # At 00:30 UTC every day. | |
| workflow_dispatch: | |
| jobs: | |
| merge-to-nightly: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| permissions: | |
| id-token: write | |
| steps: | |
| - name: Generate app token | |
| id: app-token | |
| uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }} | |
| key-name: mathlib-nightly-testing-app-pk | |
| azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_NIGHTLY_TESTING }} | |
| azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }} | |
| repositories: mathlib4,mathlib4-nightly-testing | |
| # This token is masked by the token minting action and will not be logged accidentally. | |
| - name: Checkout nightly-testing from fork | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| with: | |
| repository: leanprover-community/mathlib4-nightly-testing | |
| ref: nightly-testing | |
| path: nightly-testing | |
| token: ${{ steps.app-token.outputs.token }} | |
| fetch-depth: 0 | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| lake-package-directory: "nightly-testing" # We will run `lake update` here later. | |
| - name: Configure Git User | |
| run: | | |
| cd nightly-testing | |
| git config user.name "mathlib-nightly-testing[bot]" | |
| git config user.email "mathlib-nightly-testing[bot]@users.noreply.github.com" | |
| - name: Merge master to nightly favoring master changes | |
| run: | | |
| cd nightly-testing | |
| git remote add upstream https://github.com/leanprover-community/mathlib4.git | |
| git fetch upstream master | |
| # Merge master into nightly-testing, resolving conflicts in favor of master. | |
| # In the past, we've silently dropped changes made on master because | |
| # conflicts were resolved in favor of nightly-testing, which is bad. | |
| # If the merge goes badly, we proceed anyway via '|| true'. | |
| # CI will report failures on the 'nightly-testing' branch direct to Zulip. | |
| git merge upstream/master --strategy-option theirs --no-commit --allow-unrelated-histories || true | |
| # We aggressively run `lake update`, to avoid having to do this by hand. | |
| # When Batteries changes break Mathlib, this will likely show up on nightly-testing first. | |
| lake update -v | |
| git add . | |
| # If there's nothing to do (because there are no new commits from master), | |
| # that's okay, hence the '|| true'. | |
| git commit -m "Merge master into nightly-testing" || true | |
| # Push to the mathlib4-nightly-testing fork | |
| git push origin nightly-testing |