Merge main to nightly-testing #577
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 `main` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`. | |
| # It is a slight variant of the `nightly_merge_master.yml` job from Mathlib. | |
| name: Merge main to nightly-testing | |
| on: | |
| schedule: | |
| - cron: '30 */3 * * *' # At minute 30 past every 3rd hour. | |
| workflow_dispatch: | |
| jobs: | |
| merge-to-nightly-testing: | |
| if: github.repository == 'leanprover/cslib' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout nightly-testing | |
| uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| with: | |
| repository: leanprover/cslib | |
| ref: nightly-testing | |
| path: nightly-testing | |
| token: ${{ secrets.NIGHTLY_TESTING }} # This secret needs repo access to leanprover/cslib | |
| fetch-depth: 0 | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24 | |
| 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 | |
| # For now we reuse a bot managed by Mathlib, | |
| # but it is fine to update this if Cslib wants to create its own bot accounts. | |
| git config user.name "leanprover-community-mathlib4-bot" | |
| git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" | |
| - name: Merge main to nightly-testing favoring nightly-testing changes | |
| run: | | |
| cd nightly-testing | |
| # We use a separate remote here, | |
| # in case Cslib later wants to move its nightly-testing infrastructure to a fork. | |
| git remote add upstream https://github.com/leanprover/cslib.git | |
| git fetch upstream main | |
| # Merge main into nightly-testing, resolving conflicts in favor of nightly-testing | |
| # 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/main --strategy-option ours --no-commit --allow-unrelated-histories || true | |
| # We aggressively run `lake update`, to avoid having to do this by hand. | |
| # At present Cslib pins its dependency on Mathlib, so this should be a noop. | |
| # If Mathlib were to be unpinned, and changes in Mathlib break Cslib, | |
| # this will likely show up on nightly-testing first. | |
| lake update | |
| git add . | |
| # If there's nothing to do (because there are no new commits from main), | |
| # that's okay, hence the '|| true'. | |
| git commit -m "Merge main into nightly-testing" || true | |
| # Push | |
| git push origin nightly-testing |