Skip to content
continuous integration

remove unused argument. The linter did not find it :( #35839

Sign in to view logs

remove unused argument. The linter did not find it :(

remove unused argument. The linter did not find it :( #35839

Workflow file for this run

.github/workflows/build.yml at 5bd526b
# 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'
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@v3
- name: Install bibtool
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: lint
run: |
./scripts/lint-style.sh
- 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@v3
- 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 MathlibExtras.lean
run: |
git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.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
build:
if: github.repository == 'leanprover-community/mathlib4'
name: Build
runs-on: pr
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- 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@v3
# 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: get cache
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
- name: build library_search cache
run: lake build -KCI MathlibExtras
- name: upload cache
if: always()
run: |
lake exe cache commit || true
lake exe cache put || true
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
- name: build archive
run: lake build Archive
- name: build counterexamples
run: lake build Counterexamples
- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
build/bin/checkYaml
- name: test mathlib
run: make -j 8 test
- name: lint mathlib
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 make lint
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@v3
- 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 }}'