Skip to content

feat(RingTheory/Valuation/Integers): dvdNotUnit_iff_lt #146278

feat(RingTheory/Valuation/Integers): dvdNotUnit_iff_lt

feat(RingTheory/Valuation/Integers): dvdNotUnit_iff_lt #146278

Workflow file for this run

# DO NOT EDIT THIS FILE!!!
# This file is automatically generated by mk_build_yml.sh
# Edit .github/build.in.yml instead and run
# .github/workflows/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 GitHub-hosted workers and will only be run from external forks
on:
push:
branches-ignore:
# ignore tmp branches used by bors
- 'staging.tmp*'
- 'trying.tmp*'
- 'staging*.tmp'
- 'nolints'
name: continuous integration (mathlib forks)
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 (fork)
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: "Check for Lean files with the executable bit set"
shell: bash
run: |
executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
if [[ -n "$executable_files" ]]
then
echo "ERROR: The following Lean files have the executable bit set."
echo "$executable_files"
exit 1
fi
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v5
with:
python-version: 3.8
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
- name: "run style linters"
run: |
lake exe lint-style
- 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
build:
if: github.repository != 'leanprover-community/mathlib4'
name: Build (fork)
runs-on: ubuntu-latest
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.1.1/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: 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
id: get
run: |
rm -rf .lake/build/lib/Mathlib/
# Fail quickly if the cache is completely cold, by checking for Mathlib.Init
lake exe cache get #Mathlib.Init
#lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
id: mk_all
run: |
if ! lake exe mk_all --check
then
echo "Not all lean files are in the import all files"
echo "mk_all=false" >> "${GITHUB_OUTPUT}"
else
echo "mk_all=true" >> "${GITHUB_OUTPUT}"
fi
- 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"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
if: ${{ always() && steps.get.outcome == 'success' }}
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: 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"
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"
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 {Mathlib, Tactic, Counterexamples, Archive}.lean
run: |
if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
then
echo "Please run 'lake exe mk_all' to regenerate the import all files"
exit 1
fi
- name: check for noisy stdout lines
id: noisy
run: |
buildMsgs="$(
## we exploit `lake`s replay feature: since the cache is present, running
## `lake build` will reproduce all the outputs without having to recompute
lake build Mathlib Archive Counterexamples |
## we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
## are either numbers or ?, and the "Build completed successfully." message.
## We keep the rest, which are actual outputs of the files
awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')"
if [ -n "${buildMsgs}" ]
then
printf $'%s\n' "${buildMsgs}"
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 check-yaml
- name: verify `lake exe graph` works
run: |
lake exe graph
rm import_graph.dot
- name: build everything
# make sure everything is available for test/import_all.lean
run: |
lake build Batteries Qq Aesop ProofWidgets
- name: test mathlib
id: test
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run:
lake 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
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
# Instead we run it in a cron job on master: see `lean4checker.yml`.
# Output is posted to the zulip topic
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
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 }}
run: |
scripts/lean-pr-testing-comments.sh lean
scripts/lean-pr-testing-comments.sh batteries
final:
name: Post-CI job (fork)
if: github.repository != 'leanprover-community/mathlib4'
needs: [style_lint, build]
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/comment@v2
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