feat: port Analysis.NormedSpace.LpSpace (#4465) #2886
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# 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: | |
- staging | |
name: continuous integration (staging) | |
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/cancel-workflow-action@0.11.0 | |
with: | |
all_but_latest: true | |
access_token: ${{ github.token }} | |
style_lint: | |
if: github.repository == 'leanprover-community/mathlib4' | |
name: Lint style | |
runs-on: bors | |
steps: | |
- name: cleanup | |
run: | | |
find . -name . -o -prune -exec rm -rf -- {} + | |
- uses: actions/checkout@v3 | |
- name: Install bibtool | |
if: ${{ 'bors' == 'ubuntu-latest' }} | |
run: | | |
sudo apt-get update | |
sudo apt-get install -y bibtool | |
- name: install Python | |
if: ${{ 'bors' == '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: | | |
find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean | |
- name: update MathlibExtras.lean | |
run: | | |
find MathlibExtras -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean | |
- name: update Mathlib/Tactic.lean | |
run: | | |
find Mathlib/Tactic -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean | |
- name: check that all files are imported | |
run: git diff --exit-code | |
build: | |
if: github.repository == 'leanprover-community/mathlib4' | |
name: Build | |
runs-on: ubuntu-latest | |
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 get | |
- name: build mathlib | |
uses: liskin/gh-problem-matcher-wrap@v2 | |
with: | |
linters: gcc | |
run: env LEAN_ABORT_ON_PANIC=1 lake build | |
- name: build library_search cache | |
run: lake build 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: test mathlib | |
run: make -j 8 test | |
- name: lint mathlib | |
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/gh-get-current-pr@2.2.0 | |
# 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 }}' |