Update Mathlib Dependencies #1631
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
| name: Update Mathlib Dependencies | |
| on: | |
| schedule: | |
| - cron: '0 * * * *' # This will run every hour | |
| workflow_dispatch: | |
| jobs: | |
| update-dependencies: | |
| runs-on: ubuntu-latest | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| permissions: | |
| pull-requests: read | |
| id-token: write | |
| env: | |
| BRANCH_NAME: "update-dependencies-bot-use-only" | |
| 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_UPDATE_DEPENDENCIES_APP_ID }} | |
| key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }} | |
| key-name: mathlib-update-dependencies-app-pk | |
| azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_PR_WRITERS }} | |
| azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }} | |
| # This token is masked by the token minting action and will not be logged accidentally. | |
| - name: Checkout repository | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| fetch-depth: 0 | |
| token: ${{ steps.app-token.outputs.token }} | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| - name: Get branch SHA if it exists | |
| id: get-branch-sha | |
| run: | | |
| # Check if the branch exists remotely | |
| SHA=$(git ls-remote --heads origin "$BRANCH_NAME" | awk '{print $1}') | |
| if [ -n "$SHA" ]; then | |
| echo "Branch '$BRANCH_NAME' exists with SHA: $SHA" | |
| echo "sha=$SHA" >> "${GITHUB_OUTPUT}" | |
| else | |
| echo "Branch '$BRANCH_NAME' does not exist" | |
| echo "sha=" >> "${GITHUB_OUTPUT}" | |
| fi | |
| - name: Get PR and labels | |
| if: ${{ steps.get-branch-sha.outputs.sha != '' }} | |
| id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here | |
| uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0 | |
| # TODO: this may not work properly if the same commit is pushed to multiple branches: | |
| # https://github.com/8BitJonny/gh-get-current-pr/issues/8 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| sha: ${{ steps.get-branch-sha.outputs.sha }} | |
| # Only return if PR is still open | |
| filterOutClosed: true | |
| - name: Print PR, if found | |
| run: echo "Found PR ${prNumber} at ${prUrl}" | |
| if: steps.PR.outputs.pr_found == 'true' | |
| env: | |
| prNumber: ${{ steps.PR.outputs.number }} | |
| prUrl: ${{ steps.PR.outputs.pr_url }} | |
| - name: Get latest mathlib-ci SHA | |
| if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }} | |
| id: mathlib-ci-sha | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| SHA=$(gh api repos/leanprover-community/mathlib-ci/commits/HEAD --jq '.sha') | |
| echo "sha=$SHA" >> "$GITHUB_OUTPUT" | |
| - name: Update mathlib-ci ref in get-mathlib-ci action | |
| if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }} | |
| id: update-mathlib-ci-ref | |
| run: | | |
| sed -i "s|^\( *default: \)[0-9a-f]\{40\}|\1${{ steps.mathlib-ci-sha.outputs.sha }}|" \ | |
| .github/actions/get-mathlib-ci/action.yml | |
| if git diff --quiet .github/actions/get-mathlib-ci/action.yml; then | |
| echo "modified=false" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "modified=true" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Update dependencies | |
| if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }} | |
| run: lake update -v | |
| - name: Check if lean-toolchain was modified | |
| if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }} | |
| id: check_toolchain | |
| run: | | |
| if git diff --name-only | grep -q "lean-toolchain"; then | |
| echo "toolchain_modified=true" >> "$GITHUB_OUTPUT" | |
| echo "Lean toolchain file was modified. Skipping PR creation." | |
| else | |
| echo "toolchain_modified=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| - name: Determine PR state | |
| # only run if check_toolchain ran and returned "false" | |
| if: ${{ steps.check_toolchain.outputs.toolchain_modified == 'false' }} | |
| id: determine_state | |
| run: | | |
| # Tracked files: lake-manifest.json and .github/actions/get-mathlib-ci/action.yml | |
| # | |
| # Two-layer model | |
| # ──────────────────────────────────────────────────────────────────── | |
| # create-pull-request (CPR) compares against master: it always | |
| # force-pushes when called with any pending changes, even if the branch | |
| # already has identical content. This gate is therefore the ONLY | |
| # mechanism preventing unnecessary force-pushes. | |
| # | |
| # needs_update : working tree differs from master → PR should exist | |
| # branch_stale : working tree differs from branch tip → CPR would push | |
| # | |
| # States (checked in priority order): | |
| # SUPERSEDED : open PR + !needs_update → call CPR to close PR | |
| # CONFLICT : merge-conflict label → call CPR to rebase | |
| # STALE : open PR + branch_stale → call CPR to update branch | |
| # ABSENT : no branch or no open PR → call CPR to create/clean up | |
| # PENDING : open PR + needs_update + !branch_stale → skip CPR | |
| # ── inputs ────────────────────────────────────────────────────────── | |
| needs_update=false | |
| if ! git diff --quiet "origin/master" -- lake-manifest.json || \ | |
| [ "${{ steps.update-mathlib-ci-ref.outputs.modified }}" == "true" ]; then | |
| needs_update=true | |
| fi | |
| branch_stale=false | |
| if [ -n "${{ steps.get-branch-sha.outputs.sha }}" ]; then | |
| if ! git diff --quiet "origin/$BRANCH_NAME" -- lake-manifest.json || \ | |
| ! git diff --quiet "origin/$BRANCH_NAME" -- .github/actions/get-mathlib-ci/action.yml; then | |
| branch_stale=true | |
| fi | |
| fi | |
| pr_open="${{ steps.PR.outputs.pr_found }}" | |
| merge_conflict="${{ contains(steps.PR.outputs.pr_labels, 'merge-conflict') }}" | |
| echo "needs_update=$needs_update" | |
| echo "branch_stale=$branch_stale" | |
| echo "pr_open=$pr_open" | |
| echo "merge_conflict=$merge_conflict" | |
| # ── state ─────────────────────────────────────────────────────────── | |
| if [ "$pr_open" == "true" ] && [ "$needs_update" == "false" ]; then | |
| state="SUPERSEDED" | |
| elif [ "$merge_conflict" == "true" ]; then | |
| state="CONFLICT" | |
| elif [ "$pr_open" == "true" ] && [ "$branch_stale" == "true" ]; then | |
| state="STALE" | |
| elif [ -z "${{ steps.get-branch-sha.outputs.sha }}" ] || [ "$pr_open" != "true" ]; then | |
| state="ABSENT" | |
| else | |
| state="PENDING" | |
| fi | |
| echo "State: $state" | |
| echo "state=$state" >> "$GITHUB_OUTPUT" | |
| if [ "$state" == "PENDING" ]; then | |
| create_pr=false | |
| else | |
| create_pr=true | |
| fi | |
| echo "create_pr=$create_pr" >> "$GITHUB_OUTPUT" | |
| - name: Generate PR title | |
| id: pr-title | |
| if: ${{ steps.determine_state.outputs.create_pr == 'true' }} | |
| run: | | |
| echo "timestamp=$(date -u +"%Y-%m-%d-%H-%M")" >> "$GITHUB_ENV" | |
| echo "pr_title=chore: update Mathlib dependencies $(date -u +"%Y-%m-%d")" >> "$GITHUB_ENV" | |
| - name: Create Pull Request | |
| if: ${{ steps.pr-title.outcome == 'success' }} | |
| uses: peter-evans/create-pull-request@5f6978faf089d4d20b00c7766989d076bb2fc7f1 # v8.1.1 | |
| with: | |
| # this needs to be set, otherwise the last person who edited the `cron` line may get tagged | |
| author: "mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com>" | |
| token: ${{ steps.app-token.outputs.token }} | |
| commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}" | |
| # this branch is referenced in update_dependencies_zulip.yml | |
| branch: ${{ env.BRANCH_NAME }} | |
| base: master | |
| title: "${{ env.pr_title }}" | |
| body: | | |
| This PR updates the Mathlib dependencies. | |
| --- | |
| [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) | |
| labels: "auto-merge-after-CI" | |
| - name: Send Zulip message (failure) | |
| if: ${{ failure() }} | |
| uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2 | |
| with: | |
| api-key: ${{ secrets.ZULIP_API_KEY }} | |
| email: 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| organization-url: 'https://leanprover.zulipchat.com' | |
| to: 'nightly-testing-mathlib' | |
| type: 'stream' | |
| topic: 'Mathlib `lake update` failure' | |
| content: | | |
| ["Update dependencies" workflow run failed!](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) |