Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
continuous integration (staging)

feat(data/finset/lattice): sup'/inf' lemmas (#18989) #6613

Sign in to view logs

feat(data/finset/lattice): sup'/inf' lemmas (#18989)

feat(data/finset/lattice): sup'/inf' lemmas (#18989) #6613

Triggered via push August 28, 2023 08:49
@borsbors[bot]
pushed 5184cd7
staging
Status Failure
Total duration 3h 9m 19s
Artifacts 1

bors.yml

on: push
Build mathlib
2h 10m
Build mathlib
Lint style
15s
Lint style
Cancel Previous Runs (CI)
4s
Cancel Previous Runs (CI)
Lint mathlib
58m 50s
Lint mathlib
Run tests
17m 35s
Run tests
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

3 errors and 1 warning
Warning from simp_nf linter: src/data/finset/basic.lean#L1793
finset.filter_true - simp can prove this: by simp only [finset.filter_true_of_mem, implies_true_iff, finset.filter_congr_decidable] One of the lemmas above could be a duplicate. If that's not the case try reordering lemmas or adding @[priority].
Warning from simp_nf linter: src/data/finset/basic.lean#L1797
finset.filter_false - simp can prove this: by simp only [if_false, finset.filter_congr_decidable, finset.filter_const] One of the lemmas above could be a duplicate. If that's not the case try reordering lemmas or adding @[priority].
Lint mathlib
Process completed with exit code 1.
Build mathlib
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Artifacts

Produced during runtime
Name Size
precompiled-mathlib-3.51.1-5184cd720 Expired
817 MB