From 3418d3040cd2fe5d48c7df7fe9b77b1c6838d7c1 Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Mon, 20 Apr 2026 17:26:12 -0300 Subject: [PATCH 01/13] ci: use mathlib-nightly-testing identity bot for auto-update PRs --- .github/workflows/lake-update.yml | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 15459e38a..a6b6fbd93 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -11,7 +11,33 @@ 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 + with: + token: ${{ steps.app-token.outputs.token }} + + - 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: ${{ 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 From 2503c445e4c72b2447e217a315a311fcd6000a3d Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Mon, 20 Apr 2026 17:29:09 -0300 Subject: [PATCH 02/13] no need to use token for checkout --- .github/workflows/lake-update.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index a6b6fbd93..4600865d3 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -24,8 +24,6 @@ jobs: private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - with: - token: ${{ steps.app-token.outputs.token }} - name: Bump to latest id: bump From c4ad3196effdadaaba55ee75775f4062f4b65428 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:16:18 -0400 Subject: [PATCH 03/13] auto-merge input, title format --- .github/workflows/lake-update.yml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 4600865d3..f75d755f2 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -4,6 +4,12 @@ on: #schedule: # - cron: "0 20 * * *" # Daily at 20:00 UTC, after the hopscotch-reports regression run workflow_dispatch: + inputs: + auto-merge: + description: 'Set auto-merge for the opened PR' + required: true + type: boolean + default: false permissions: contents: write @@ -30,12 +36,19 @@ jobs: 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: ${{ steps.bump.outputs.pr-title }} + 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 != '' && ${{ inputs.auto-merge }} + env: + GH_TOKEN: ${{ steps.app-token.outputs.token }} + run: gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" From d28e219080ea13412df0b73e0dd867e85712ea3a Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:18:27 -0400 Subject: [PATCH 04/13] missing braces --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index f75d755f2..a1ba4b0ee 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -48,7 +48,7 @@ jobs: git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com - name: Enable auto-merge - if: steps.open-pr.outputs.pr-number != '' && ${{ inputs.auto-merge }} + if: ${{ steps.open-pr.outputs.pr-number }} != '' && ${{ inputs.auto-merge }} env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" From 3f51745edf184d4ecc93bcd3f873d4359c2979f6 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:21:37 -0400 Subject: [PATCH 05/13] once more... --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index a1ba4b0ee..e0fe58321 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -48,7 +48,7 @@ jobs: git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com - name: Enable auto-merge - if: ${{ steps.open-pr.outputs.pr-number }} != '' && ${{ inputs.auto-merge }} + if: steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" From ae5c9dcce2a268f496bc1f49f60fa3209bf7c504 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:33:57 -0400 Subject: [PATCH 06/13] minimize boolean test... --- .github/workflows/lake-update.yml | 36 ++++++++++++++++--------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index e0fe58321..834bbe469 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -29,26 +29,28 @@ jobs: app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} - - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 + #- 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: 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: 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 != '' && inputs.auto-merge == 'true' + #if: steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' + if: inputs.auto-merge == 'true' env: GH_TOKEN: ${{ steps.app-token.outputs.token }} - run: gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" + run: | + echo "test" From 7836be17fcf8c5328aae577b02a6f36ca7ad3456 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:36:14 -0400 Subject: [PATCH 07/13] braces? --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 834bbe469..2c40c9f32 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -49,7 +49,7 @@ jobs: - name: Enable auto-merge #if: steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' - if: inputs.auto-merge == 'true' + if: ${{ inputs.auto-merge }} == 'true' env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | From 94fea7aa62f411724fd9f0efafd4a4b58e2b6274 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:37:58 -0400 Subject: [PATCH 08/13] braces? --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 2c40c9f32..2ac886e12 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -49,7 +49,7 @@ jobs: - name: Enable auto-merge #if: steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' - if: ${{ inputs.auto-merge }} == 'true' + if: ${{ ${{ inputs.auto-merge }} == 'true' }} env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | From 3bedc13f84bf314e5cec92ebbb40a213369011ba Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:38:32 -0400 Subject: [PATCH 09/13] braces? --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 2ac886e12..d124fe57b 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -49,7 +49,7 @@ jobs: - name: Enable auto-merge #if: steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' - if: ${{ ${{ inputs.auto-merge }} == 'true' }} + if: ${{ inputs.auto-merge == 'true' }} env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | From 3aee23cb7404ab1bed6e616c5ec34b1b7357719c Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:40:27 -0400 Subject: [PATCH 10/13] full thing... --- .github/workflows/lake-update.yml | 35 +++++++++++++++---------------- 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index d124fe57b..6875ed46f 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -29,28 +29,27 @@ jobs: app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }} - #- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 + - 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: 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: 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 != '' && inputs.auto-merge == 'true' - if: ${{ inputs.auto-merge == 'true' }} + if: ${{ steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' }} env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | - echo "test" + gh pr merge --auto --merge "${{ steps.open-pr.outputs.pr-number }}" From 1cf61de3b18e76b96703aac0ca6d67075c75fd69 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 17:55:02 -0400 Subject: [PATCH 11/13] try removing the empty string check? --- .github/workflows/lake-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index 6875ed46f..cd46bd70b 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -48,7 +48,7 @@ jobs: git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com - name: Enable auto-merge - if: ${{ steps.open-pr.outputs.pr-number != '' && inputs.auto-merge == 'true' }} + if: ${{ inputs.auto-merge == 'true' }} env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | From b9338db6a5e9354c4c9049219dcca90b1b10b314 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Mon, 20 Apr 2026 18:03:00 -0400 Subject: [PATCH 12/13] get rid of input --- .github/workflows/lake-update.yml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml index cd46bd70b..35028aead 100644 --- a/.github/workflows/lake-update.yml +++ b/.github/workflows/lake-update.yml @@ -4,12 +4,6 @@ on: #schedule: # - cron: "0 20 * * *" # Daily at 20:00 UTC, after the hopscotch-reports regression run workflow_dispatch: - inputs: - auto-merge: - description: 'Set auto-merge for the opened PR' - required: true - type: boolean - default: false permissions: contents: write @@ -48,7 +42,7 @@ jobs: git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com - name: Enable auto-merge - if: ${{ inputs.auto-merge == 'true' }} + if: steps.open-pr.outputs.pr-number != '' env: GH_TOKEN: ${{ steps.app-token.outputs.token }} run: | From cbccccba65a0262fdbb77074e5e46bf0306f57a8 Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Mon, 20 Apr 2026 22:08:01 +0000 Subject: [PATCH 13/13] chore: bump mathlib to 1d2ba2d: chore: remove implicit-reducible diamond in boolean rings (#38246) (2026-04-19) --- lake-manifest.json | 4 ++-- lakefile.toml | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) 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"