Skip to content

Update Mathlib Dependencies #3869

Update Mathlib Dependencies

Update Mathlib Dependencies #3869

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"