diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 15459e38a..35028aead 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -11,7 +11,39 @@ permissions: jobs: bump: - uses: leanprover-community/downstream-reports/.github/workflows/bump-dependency-to-latest.yml@main + runs-on: ubuntu-latest permissions: contents: write pull-requests: 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 }} + + - 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 + id: open-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 + + - name: Enable auto-merge + if: steps.open-pr.outputs.pr-number != '' + env: + GH_TOKEN: ${{ steps.app-token.outputs.token }} + run: | + gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" diff --git a/lake-manifest.json b/lake-manifest.json index c2af358d2..262223fbd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", + "rev": "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 390db150b..2de532e95 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -18,6 +18,7 @@ weak.linter.unicodeLinter = false [[require]] name = "mathlib" scope = "leanprover-community" +rev = "1d2ba2d2aedb9065a4699cff0bfe8f0c3d3fb8d9" [[lean_lib]] name = "Cslib"