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@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        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@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.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 }})