Update lean-toolchain for testing https://github.com/leanprover/lean4… #77579
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
1s
check workflows
9s
Post-CI job
0s
Annotations
15 errors and 6 warnings
|
Lint style:
Mathlib/Data/List/Basic.lean#L1157
Mathlib/Data/List/Basic.lean#L1157: ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
|
Lint style:
Mathlib/Data/Nat/Digits.lean#L274
Mathlib/Data/Nat/Digits.lean#L274: ERR_LIN: Line has more than 100 characters
|
|
Lint style:
Mathlib/Data/Nat/Multiplicity.lean#L131
Mathlib/Data/Nat/Multiplicity.lean#L131: ERR_LIN: Line has more than 100 characters
|
|
Lint style:
Mathlib/Data/Num/Lemmas.lean#L988
Mathlib/Data/Num/Lemmas.lean#L988: ERR_NSP: Non-terminal simp. Replace with `simp?` and use the suggested output
|
|
Lint style
Process completed with exit code 123.
|
|
Build:
Mathlib/Computability/TMToPartrec.lean#L573
simp made no progress
|
|
Build:
Mathlib/Computability/TMToPartrec.lean#L573
unsolved goals
|
|
Build:
Mathlib/Computability/TMToPartrec.lean#L714
simp made no progress
|
|
Build:
Mathlib/SetTheory/Ordinal/Basic.lean#L1060
type mismatch
|
|
Build:
Mathlib/Data/Nat/Multiplicity.lean#L135
type mismatch
|
|
Build:
Mathlib/Topology/Support.lean#L266
application type mismatch
|
|
Build:
Mathlib/Topology/Support.lean#L273
Declaration HasCompactSupport.comp₂_left not found.
|
|
Build:
Mathlib/Topology/Support.lean#L325
@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration
|
|
Build:
Mathlib/Topology/Support.lean#L329
Declaration HasCompactSupport.add not found.
|
|
Build:
Mathlib/Data/Polynomial/Derivative.lean#L316
simp made no progress
|
|
Check all files imported
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
check workflows
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Lint style
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, actions/setup-python@v4. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Build
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/checkout@v3, liskin/gh-problem-matcher-wrap@v2. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Build:
Mathlib/Data/Nat/Cast/Defs.lean#L169
declaration uses 'sorry'
|
|
Build:
Mathlib/AlgebraicTopology/SimplicialSet.lean#L294
this tactic is never executed [linter.unreachableTactic]
|