Skip to content

chore: adaptations for nightly-2024-05-09 #90333

chore: adaptations for nightly-2024-05-09

chore: adaptations for nightly-2024-05-09 #90333

Workflow file for this run

# DO NOT EDIT THIS FILE!!!
# This file is automatically generated by mk_build_yml.sh
# Edit build.yml.in instead and run mk_build_yml.sh to update.
# Forks of mathlib and other projects should be able to use build_fork.yml directly
# The jobs in this file run on self-hosted workers and will not be run from external forks
on:
push:
branches-ignore:
# ignore tmp branches used by bors
- 'staging.tmp*'
- 'trying.tmp*'
- 'staging*.tmp'
- 'nolints'
# ignore staging branch used by bors, this is handled by bors.yml
- 'staging'
merge_group:
name: continuous integration
jobs:
# Cancels previous runs of jobs in this file
cancel:
if: github.repository == 'leanprover-community/mathlib4'
name: 'Cancel Previous Runs (CI)'
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/[email protected]
with:
all_but_latest: true
access_token: ${{ github.token }}
style_lint:
if: github.repository == 'leanprover-community/mathlib4'
name: Lint style
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
# Run the case checker action
- name: Check Case Sensitivity
uses: credfeto/[email protected]
- name: Look for ignored files
uses: credfeto/[email protected]
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v5
with:
python-version: 3.8
- name: lint
run: |
./scripts/lint-style.sh
- name: Install bibtool
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool
- name: lint references.bib
run: |
./scripts/lint-bib.sh
check_imported:
if: github.repository == 'leanprover-community/mathlib4'
name: Check all files imported
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
- name: update Mathlib.lean
run: |
git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
- name: update Mathlib/Tactic.lean
run: |
git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
- name: update Counterexamples.lean
run: |
git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
- name: update Archive.lean
run: |
git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
- name: check that all files are imported
run: git diff --exit-code
check_workflows:
if: github.repository == 'leanprover-community/mathlib4'
name: check workflows
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
- name: update workflows
run: |
cd .github/workflows/
./mk_build_yml.sh
- name: check that workflows were consistent
run: git diff --exit-code
build:
if: github.repository == 'leanprover-community/mathlib4'
name: Build
runs-on: pr
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
# Delete all but the 5 most recent toolchains.
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
: # Do nothing on success
else
: # Do nothing on failure, but suppress errors
fi
# The Hoskinson runners may not have jq installed, so do that now.
- name: 'Setup jq'
uses: dcarbone/[email protected]
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/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
# We update `Mathlib.lean` as a convenience here,
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
- name: If using a lean-pr-release toolchain, uninstall
run: |
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
elan toolchain uninstall "$(cat lean-toolchain)"
fi
- name: print lean and lake versions
run: |
lean --version
lake --version
- name: build cache
run: |
lake build cache
- name: prune ProofWidgets .lake
run: |
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
# but also `.oleans`, which may have been built with the wrong toolchain.
# This removes them.
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
rm -rf .lake/packages/proofwidgets/.lake/build/lib
rm -rf .lake/packages/proofwidgets/.lake/build/ir
- name: get cache
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
id: build
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI | tee stdout.log"
- name: upload cache
# We only upload the cache if the build ran (either succeeding or failing),
# but not if it was skipped.
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
run: |
# TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
# lake exe cache commit || true
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
# lake exe cache put!
# do not try to upload files just downloaded
lake exe cache put-unpacked
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: check the cache
run: |
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
lake exe cache clean!
rm -rf .lake/build/lib/Mathlib
lake exe cache get || (sleep 1; lake exe cache get)
lake build --no-build
fi
- name: find `#`-commands
id: hash_commands
run: |
chmod u+x scripts/lint_hash_commands.sh
./scripts/lint_hash_commands.sh
- name: build archive
id: archive
run: |
# Note: we should not be including `Archive` and `Counterexamples` in the cache.
# We do this for now for the sake of not rebuilding them in every CI run
# even when they are not touched.
# Since `Archive` and `Counterexamples` files have very simple dependencies,
# it should be possible to determine whether they need to be built without actually
# storing and transferring oleans over the network.
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
lake exe cache get Archive.lean
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive | tee --append stdout.log"
lake exe cache put Archive.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: build counterexamples
id: counterexamples
run: |
lake exe cache get Counterexamples.lean
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples | tee --append stdout.log"
lake exe cache put Counterexamples.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: check for noisy stdout lines
id: noisy
run: |
grep --after-context=1 "stdout" stdout.log && ret=0
grep --after-context=1 "stderr" stdout.log && new=0
if [ "${ret}" == "0" ] || [ "${new}" == "0" ]; then exit 1; fi
- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
lake exe checkYaml
- name: verify `lake exe graph` works
run: |
lake exe graph
rm import_graph.dot
- name: test mathlib
id: test
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: |
bash -o pipefail -c "
make -k -j 8 test"
- name: check for unused imports
id: shake
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
- name: check environments using lean4checker
id: lean4checker
run: |
git clone https://github.com/leanprover/lean4checker
cd lean4checker
git checkout v4.8.0-rc1
# Now that the git hash is embedded in each olean,
# we need to compile lean4checker on the same toolchain
cp ../lean-toolchain .
lake build
./test.sh
cd ..
lake env lean4checker/.lake/build/bin/lean4checker
- name: Post comments for lean-pr-testing branch
if: always()
env:
TOKEN: ${{ secrets.LEAN_PR_TESTING }}
GITHUB_CONTEXT: ${{ toJson(github) }}
WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
BUILD_OUTCOME: ${{ steps.build.outcome }}
NOISY_OUTCOME: ${{ steps.noisy.outcome }}
ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
LINT_OUTCOME: ${{ steps.lint.outcome }}
TEST_OUTCOME: ${{ steps.test.outcome }}
CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
run: |
scripts/lean-pr-testing-comments.sh
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- id: PR
uses: 8BitJonny/[email protected]
# 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 }}
# Only return if PR is still open
filterOutClosed: true
- id: remove_labels
name: Remove "awaiting-CI"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
run: |
curl --request DELETE \
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
uses: GrantBirki/[email protected]
with:
token: ${{ secrets.AUTO_MERGE_TOKEN }}
issue-number: ${{ steps.PR.outputs.number }}
body: |
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
bors merge