chore: keep trying with update_dependencies workflow (#14143)

.github/workflows/update_dependencies.yml

@@ -8,82 +8,40 @@ jobs:
   update-dependencies:
     runs-on: ubuntu-latest
     steps:
-      - name: install elan
+      - name: Install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          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.NIGHTLY_TESTING }}
+          token: "${{ secrets.NIGHTLY_TESTING }}"
 
       - name: Configure Git User
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "[email protected]"
 
-      - name: Check for existing PRs
-        id: check_pr
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          prs=$(gh pr list --search "author:leanprover-community-mathlib4-bot state:open" --json title,headRefName)
-          for pr in $(echo "$prs" | jq -c '.[]'); do
-            pr_title=$(echo "$pr" | jq -r '.title')
-            pr_branch=$(echo "$pr" | jq -r '.headRefName')
-            if [[ "$pr_title" == *"update Mathlib dependencies"* ]] || [[ "$pr_branch" == update-dependencies-* ]]; then
-              echo "Existing PR found with title or branch name indicating a dependency update. Stopping."
-              echo "existing_pr=true" >> "$GITHUB_ENV"
-              exit 0
-            fi
-          done
-          echo "existing_pr=false" >> "$GITHUB_ENV"
-
-      - name: Stop if PR exists
-        if: env.existing_pr == 'true'
-        run: echo "Stopping workflow due to existing PR."
-
       - name: Update dependencies
-        if: env.existing_pr == 'false'
         run: lake update
 
-      - name: Check for changes
-        id: check_changes
-        if: env.existing_pr == 'false'
-        run: |
-          if git diff-index --quiet HEAD --; then
-            echo "no_changes=true" >> "$GITHUB_ENV"
-          else
-            echo "no_changes=false" >> "$GITHUB_ENV"
-          fi
-
-      - name: Stop if no changes
-        if: env.no_changes == 'true'
-        run: echo "No changes detected. Stopping."
-
-      - name: Create new branch
-        if: env.no_changes == 'false'
-        id: create_new_branch
+      - name: Generate branch name
+        id: generate_branch_name
         run: |
           timestamp=$(date -u +"%Y-%m-%d-%H-%M")
-          branch_name="update-dependencies-$timestamp"
-          echo "branch_name=$branch_name" >> "$GITHUB_ENV"
-          git checkout -b "$branch_name"
-          git add .
-          git commit -m "chore: update Mathlib dependencies $(date -u +\"%Y-%m-%d\")"
-          git push origin "$branch_name"
+          echo "branch_name=update-dependencies-$timestamp" >> "$GITHUB_ENV"
 
       - name: Create Pull Request
-        if: env.no_changes == 'false'
-        uses: peter-evans/create-pull-request@v5
+        uses: peter-evans/create-pull-request@v6
         with:
-          token: ${{ secrets.NIGHTLY_TESTING }}
+          token: "${{ secrets.NIGHTLY_TESTING }}"
           commit-message: "chore: update Mathlib dependencies $(date -u +\"%Y-%m-%d\")"
-          branch: ${{ env.branch_name }}
-          base: master  # Ensure the base branch is explicitly set to master
+          branch: "${{ env.branch_name }}"
+          base: master
           title: "chore: update Mathlib dependencies $(date -u +\"%Y-%m-%d\")"
+          body: "This PR updates the Mathlib dependencies."
           labels: "auto-merge-after-CI"