Skip to content

Commit

Permalink
Merge branch 'fix-lint' into alexjbest/auto-suggest
Browse files Browse the repository at this point in the history 
* fix-lint: (463 commits)
  chore: lint-style.py was calling str.replace incorrectly
  chore: module doc for #find_home, #minimize_imports, import early (#7095)
  chore: reduce imports to Data.Rat.Cast.CharZero (#7091)
  chore: cleanup imports of Data/Rat/Cast/Defs (#7092)
  chore: linarith only needs ring1 (#7090)
  refactor(Data/Int/Bitwise): use `<<<` and `>>>` notation (#6789)
  chore: delete redundant commented-out positivity test (#7085)
  chore: fix docstrings, names and aligns about paracompacity of emetric spaces (#7064)
  feat(Data/Finsupp): add notation (#6367)
  refactor: re-home some meta code (#6921)
  fix: don't use `False` as a bool, use `false` (#7059)
  chore: fix reference to `compactCovering` in docstring (#7065)
  fix: fix link in docstring of IsWellFounded (#7063)
  chore: tidy various files (#7041)
  feat: roots in an algebra (#6740)
  chore: revert ProofWidgets bump in #7044 and #7056 (#7069)
  feat: super factorial (#6768)
  feat(LinearAlgebra/Matrix/Trace): add Matrix.trace_diagonal (#7061)
  chore: complete ProofWidgets bump (#7056)
  feat: More `Finset.sup'` lemmas (#7021)
  feat: self_lt_pow (#7058)
  chore: move some files to `MeasureTheory/MeasurableSpace/` (#7045)
  chore(RingTheory/Nilpotent): untwine two universes (#7057)
  feat: von Neumann Mean Ergodic Theorem (#6053)
  feat: (sSup, Iic) and (Ici, sInf) are Galois connections (#6951)
  feat: derivative along a vector (#7038)
  feat: check for some common git problems in CI (#7043)
  chore: bump ProofWidgets (#7044)
  feat(Topology/Algebra): add `DiscreteTopology Mˣ` (#7028)
  chore: simplify `by rfl` (#7039)
  chore: tidy various files (#7035)
  refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' (#6783)
  feat: add `DiscreteTopology.of_continuous_injective` (#7029)
  feat: restore the module docstring code snippet (#7030)
  feat: flesh out the API for `realPart` and `imaginaryPart` (#7023)
  chore: missing simps lemmas for `Multiplicative` defs (#7016)
  feat: characterize isLittleO on principal filters (#7008)
  doc: cleanup documentation on Basis.constr (#7007)
  feat: cleanup API around differentiable functions (#7004)
  feat: add Nat.digits_append_digits (#6999)
  feat: definition of the homology of a short complex (#6994)
  chore: implement porting notes about Polish spaces (#6991)
  feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915)
  feat: compute the integral of sqrt (1 - x ^ 2) (#6905)
  chore(*/TensorProduct): missing functorial lemmas (#6781)
  feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
  feat: expand API on locally integrable functions (#7006)
  chore: split Tactic.NormNum.Basic (#7002)
  feat: a few lemmas on continuous functions (#7005)
  feat: ZMod.castHom_self (#7013)
  ...
  • Loading branch information
@Julian
Julian committed Sep 11, 2023
2 parents 15f7041 + b2bd89a commit 4eadc5d
Show file tree
Hide file tree
Showing 1,781 changed files with 37,447 additions and 14,884 deletions.
77 changes: 73 additions & 4 deletions .github/workflows/bors.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,19 @@ jobs:
- uses: actions/checkout@v3

# Run the case checker action
- name: Check Case Sensitivity
uses: credfeto/action-case-checker@v1.3.0

- name: Look for ignored files
uses: credfeto/action-no-ignored-files@v1.1.0

- 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
Expand Down Expand Up @@ -99,6 +112,12 @@ jobs:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
# Delete any elan toolchains older than two weeks.
find $HOME/.elan/toolchains/ -maxdepth 1 -type d -ctime +14 -exec rm -rf {} || true
# The Hoskinson runners may not have jq installed, so do that now.
- name: 'Setup jq'
uses: dcarbone/install-jq-action@v1.0.1

- name: install elan
run: |
Expand All @@ -115,12 +134,20 @@ jobs:
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
echo "Uninstalling transient toolchain `cat lean-toolchain`"
elan toolchain uninstall `cat lean-toolchain`
fi
- name: get cache
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
id: build
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
Expand All @@ -143,24 +170,55 @@ jobs:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build archive
run: lake build Archive
run: |
# Note: we should not be including `Archive` and `Countexamples` 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
lake build Archive
lake exe cache put Archive.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build counterexamples
run: lake build Counterexamples
run: |
lake exe cache get Counterexamples.lean
lake build Counterexamples
lake exe cache put Counterexamples.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
build/bin/checkYaml
lake exe checkYaml
- name: test mathlib
id: test
run: make -j 8 test

- name: lint mathlib
id: lint
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 make lint
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter

- 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.event.workflow_run.id }}
LINT_OUTCOME: ${{ steps.lint.outcome }}
TEST_OUTCOME: ${{ steps.test.outcome }}
BUILD_OUTCOME: ${{ steps.build.outcome }}
run: |
scripts/lean-pr-testing-comments.sh
final:
name: Post-CI job
Expand All @@ -187,3 +245,14 @@ jobs:
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.0.1
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
77 changes: 73 additions & 4 deletions .github/workflows/build.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,19 @@ jobs:
- uses: actions/checkout@v3

# Run the case checker action
- name: Check Case Sensitivity
uses: credfeto/action-case-checker@v1.3.0

- name: Look for ignored files
uses: credfeto/action-no-ignored-files@v1.1.0

- 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
Expand Down Expand Up @@ -105,6 +118,12 @@ jobs:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
# Delete any elan toolchains older than two weeks.
find $HOME/.elan/toolchains/ -maxdepth 1 -type d -ctime +14 -exec rm -rf {} || true
# The Hoskinson runners may not have jq installed, so do that now.
- name: 'Setup jq'
uses: dcarbone/install-jq-action@v1.0.1

- name: install elan
run: |
Expand All @@ -121,12 +140,20 @@ jobs:
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
echo "Uninstalling transient toolchain `cat lean-toolchain`"
elan toolchain uninstall `cat lean-toolchain`
fi
- name: get cache
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
id: build
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
Expand All @@ -149,24 +176,55 @@ jobs:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build archive
run: lake build Archive
run: |
# Note: we should not be including `Archive` and `Countexamples` 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
lake build Archive
lake exe cache put Archive.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build counterexamples
run: lake build Counterexamples
run: |
lake exe cache get Counterexamples.lean
lake build Counterexamples
lake exe cache put Counterexamples.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
build/bin/checkYaml
lake exe checkYaml
- name: test mathlib
id: test
run: make -j 8 test

- name: lint mathlib
id: lint
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 make lint
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter

- 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.event.workflow_run.id }}
LINT_OUTCOME: ${{ steps.lint.outcome }}
TEST_OUTCOME: ${{ steps.test.outcome }}
BUILD_OUTCOME: ${{ steps.build.outcome }}
run: |
scripts/lean-pr-testing-comments.sh
final:
name: Post-CI job
Expand All @@ -193,3 +251,14 @@ jobs:
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.0.1
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
77 changes: 73 additions & 4 deletions .github/workflows/build.yml.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,19 @@ jobs:

- uses: actions/checkout@v3

# Run the case checker action
- name: Check Case Sensitivity
uses: credfeto/action-case-checker@v1.3.0

- name: Look for ignored files
uses: credfeto/action-no-ignored-files@v1.1.0

- name: Install bibtool
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool

- name: install Python
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
uses: actions/setup-python@v4
Expand Down Expand Up @@ -85,6 +98,12 @@ jobs:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
# Delete any elan toolchains older than two weeks.
find $HOME/.elan/toolchains/ -maxdepth 1 -type d -ctime +14 -exec rm -rf {} || true

# The Hoskinson runners may not have jq installed, so do that now.
- name: 'Setup jq'
uses: dcarbone/install-jq-action@v1.0.1

- name: install elan
run: |
Expand All @@ -101,12 +120,20 @@ jobs:
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
echo "Uninstalling transient toolchain `cat lean-toolchain`"
elan toolchain uninstall `cat lean-toolchain`
fi

- name: get cache
run: |
lake exe cache clean
lake exe cache get

- name: build mathlib
id: build
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
Expand All @@ -129,24 +156,55 @@ jobs:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build archive
run: lake build Archive
run: |
# Note: we should not be including `Archive` and `Countexamples` 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
lake build Archive
lake exe cache put Archive.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: build counterexamples
run: lake build Counterexamples
run: |
lake exe cache get Counterexamples.lean
lake build Counterexamples
lake exe cache put Counterexamples.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
build/bin/checkYaml
lake exe checkYaml

- name: test mathlib
id: test
run: make -j 8 test

- name: lint mathlib
id: lint
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 make lint
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter

- 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.event.workflow_run.id }}
LINT_OUTCOME: ${{ steps.lint.outcome }}
TEST_OUTCOME: ${{ steps.test.outcome }}
BUILD_OUTCOME: ${{ steps.build.outcome }}
run: |
scripts/lean-pr-testing-comments.sh

final:
name: Post-CI jobJOB_NAME
Expand All @@ -173,3 +231,14 @@ jobs:
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.0.1
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
Loading

0 comments on commit 4eadc5d

Please sign in to comment.