update_dependencies.yml

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 }})