Update Mathlib Dependencies #4719
This file contains 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 | |
| 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" |