Bump mathlib to LKG #49
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
| # Keeps cslib's mathlib dependency up to date and tracks compatibility. | |
| # | |
| # leanprover-community/downstream-reports publishes a daily snapshot | |
| # of each downstream's build status against recent mathlib commits, identifying the | |
| # last-known-good (LKG) and first-known-bad (FKB) mathlib revisions for each project. | |
| # | |
| # The provided actions which are used here consume this snapshot, with: | |
| # | |
| # bump: | |
| # updates lakefile.lean/lake-manifest to the LKG mathlib commit | |
| # and opens (or force-pushes) a PR via the mathlib-nightly-testing bot. | |
| # track-incompatibility: | |
| # opens | |
| # (1) a persistent issue when an FKB commit is detected (i.e. cslib | |
| # can't yet advance to the mathlib tip) | |
| # (2) a pull request with the dependency pinned to this commit, so issues can be worked on | |
| # closes these automatically once the incompatibility is resolved. | |
| name: Bump mathlib to LKG | |
| on: | |
| schedule: | |
| - cron: "0 20 * * *" # Daily at 20:00 UTC, after the hopscotch-reports regression run | |
| workflow_dispatch: | |
| jobs: | |
| bump: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Generate app token | |
| id: app-token | |
| uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Bump to latest | |
| id: bump | |
| uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main | |
| - name: Open or update PR | |
| if: steps.bump.outputs.updated == 'true' | |
| uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main | |
| with: | |
| title: "chore: ${{ steps.bump.outputs.pr-title }}" | |
| message: ${{ steps.bump.outputs.bump-description }} | |
| commit-message: ${{ steps.bump.outputs.commit-message }} | |
| token: ${{ steps.app-token.outputs.token }} | |
| git-user-name: mathlib-nightly-testing[bot] | |
| git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com | |
| open-issue: | |
| runs-on: ubuntu-latest | |
| permissions: | |
| issues: write | |
| steps: | |
| - name: Generate app token | |
| id: app-token | |
| uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} | |
| # We need to check out so the action can open the PR | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Open or update incompatibility issue | |
| uses: leanprover-community/downstream-reports/.github/actions/track-incompatibility@main | |
| with: | |
| open-pr: true | |
| token: ${{ steps.app-token.outputs.token }} | |
| git-user-name: mathlib-nightly-testing[bot] | |
| git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com |