update.yml

name: Update Dependencies

on:
  schedule:
    - cron: "0 */6 * * *"   # Check for updates every six hours
  workflow_dispatch:

jobs:
  # LML gets Mathlib through Statlib: bumping Statlib to its latest `main` commit also moves Mathlib
  # (and Mathlib's dependencies) to the commits that Statlib pins. Statlib keeps itself close to
  # Mathlib master with its own updater, and the incompatibilities with Mathlib are tracked there.
  bump-statlib:
    runs-on: ubuntu-latest
    permissions:
      contents: write
      pull-requests: write
    steps:
      - uses: actions/checkout@v7

      - name: Install Lean
        uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
        with:
          auto-config: false
          use-mathlib-cache: false

      - name: Bump Statlib
        id: bump
        run: |
          rev() { jq -r --arg name "$1" '.packages[] | select(.name == $name) | .rev' lake-manifest.json; }
          old=$(rev Statlib)
          lake update Statlib
          new=$(rev Statlib)
          if [ "$old" = "$new" ]; then
            echo "Statlib is already at its latest commit ${new:0:7}."
            echo "updated=false" >> "$GITHUB_OUTPUT"
            exit 0
          fi
          mathlib=$(rev mathlib)
          {
            echo "updated=true"
            echo "title=chore: bump Statlib to ${new:0:7} (Mathlib ${mathlib:0:7})"
          } >> "$GITHUB_OUTPUT"

      # Pull requests opened by this workflow do not trigger the Build workflow, so the bump is
      # checked here, and opened only if LML and its tutorial build without warnings.
      - name: Build
        if: steps.bump.outputs.updated == 'true'
        run: |
          lake exe cache get
          lake build --wfail LeanMachineLearning LMLTutorial

      - name: Open or update PR
        if: steps.bump.outputs.updated == 'true'
        uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main
        with:
          branch:         statlib-bump
          title:          ${{ steps.bump.outputs.title }}
          commit-message: ${{ steps.bump.outputs.title }}
          body: >
            Bumps Statlib to its latest `main` commit. LML gets Mathlib through Statlib, so Mathlib
            moves to the commit that Statlib pins. `lake build --wfail LeanMachineLearning
            LMLTutorial` passed in the workflow run that opened this pull request.