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
    steps:
      - name: Install elan
        run: |
          set -o pipefail
          curl -sSfL "https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz" | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"

      - name: Checkout repository
        uses: actions/checkout@v4
        with:
          fetch-depth: 0
          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"

      - name: Get sha of branch
        id: sha
        run: |
          SHA="$(git rev-parse --verify origin/update-dependencies-bot-use-only)"
          echo "sha=$SHA" >> "$GITHUB_OUTPUT"

      - name: Get PR and labels
        if: ${{ steps.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@3.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.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: Configure Git User
        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
        run: |
          git config user.name "leanprover-community-mathlib4-bot"
          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"

      - name: Update dependencies
        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
        run: lake update

      - name: Generate PR title
        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
        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: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
        uses: peter-evans/create-pull-request@v7
        with:
          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
          commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
          # this branch is referenced in update_dependencies_zulip.yml
          branch: "update-dependencies-bot-use-only"
          base: master
          title: "${{ env.pr_title }}"
          body: "This PR updates the Mathlib dependencies."
          labels: "auto-merge-after-CI"