Skip to content

update

update #2525

Workflow file for this run

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