update.yml

on:
  schedule:
    - cron: '30 7 * * *'  # 8:30 AM CET/11:30 PM PT
  workflow_dispatch:

name: update

jobs:
  update:
    name: Auto-update mathlib4
    runs-on: mathport
    steps:
      - name: clean up
        run: |
          rm -rf *
          rm -rf $HOME/.elan
          rm -rf $HOME/.cache/mathlib

      - name: install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - uses: actions/checkout@v4

      - name: lake update
        id: update
        run: |
          MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
          if git describe --exact-match --tags HEAD 2> /dev/null \
             && git diff --exit-code lake-manifest.json > /dev/null
          then
            echo "nothing_to_do=true" >> $GITHUB_OUTPUT
          fi

      - name: get cache
        if: success() && ${{ steps.update.outputs.nothing_to_do != 'true' }}
        run: lake exe cache get

      - name: build mathport
        if: success() && ${{ steps.update.outputs.nothing_to_do != 'true' }}
        run: lake build

      - name: push update commit
        if: success() && ${{ steps.update.outputs.nothing_to_do != 'true' }}
        run: |
          git diff --exit-code && exit
          git config --global user.email "leanprover.community@gmail.com"
          git config --global user.name "leanprover-community-bot"
          git commit -am 'chore: bump mathlib'
          git push

      - name: clean up
        if: always()
        run: |
          rm -rf *
          rm -rf $HOME/.elan
          rm -rf $HOME/.cache/mathlib