Update Mathlib Dependencies #15669
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@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.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: 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: Check if lake-manifest.json was modified or if no mergeable PR exists | |
| # only run if check_toolchain ran and returned "false" | |
| if: ${{ steps.check_toolchain.outputs.toolchain_modified == 'false' }} | |
| id: check_manifest | |
| run: | | |
| # Default to false | |
| create_pr=false | |
| # Log individual reasons for running the create-pull-request action | |
| if [ -z "${{ steps.get-branch-sha.outputs.sha }}" ]; then | |
| create_pr=true | |
| echo "$BRANCH_NAME does not exist, need to run create-pull-request to create it" | |
| fi | |
| if [ "${{ steps.PR.outputs.pr_found }}" != "true" ]; then | |
| create_pr=true | |
| echo "PR does not exist, need to run create-pull-request to check whether one should be created" | |
| fi | |
| if [ "${{ steps.PR.outputs.pr_found }}" == "true" ] && \ | |
| git diff --quiet "origin/master" -- lake-manifest.json; then | |
| create_pr=true | |
| echo "No differences found with lake-manifest.json on master, need to run create-pull-request to close the PR" | |
| fi | |
| if [ "${{ contains(steps.PR.outputs.pr_labels, 'merge-conflict') }}" == "true" ]; then | |
| create_pr=true | |
| echo "merge-conflict on PR, need to run create-pull-request to update $BRANCH_NAME" | |
| fi | |
| if [ -n "${{ steps.get-branch-sha.outputs.sha }}" ] && \ | |
| ! git diff --quiet "origin/$BRANCH_NAME" -- lake-manifest.json; then | |
| create_pr=true | |
| echo "Differences found with lake-manifest.json on $BRANCH_NAME, need to run create-pull-request to update $BRANCH_NAME" | |
| fi | |
| # Otherwise, there's no reason to run create-pull-request | |
| echo "create_pr=$create_pr" >> "${GITHUB_OUTPUT}" | |
| - name: Generate PR title | |
| id: pr-title | |
| if: ${{ steps.check_manifest.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@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0 | |
| 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' | |
| type: 'stream' | |
| topic: 'Mathlib `lake update` failure' | |
| content: | | |
| ["Update dependencies" workflow run failed!](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) |