Update lean-toolchain for testing https://github.com/leanprover/lean4… #133488
leanprover-community-mathlib4-botbuild.yml
on: push
Cancel Previous Runs (CI)
2s
Post-CI job
0s
Annotations
10 errors and 5 warnings
|
Build:
test/DocPrime.lean#L36
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Clean.lean#L12
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Clean.lean#L18
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Clean.lean#L28
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Clean.lean#L35
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L18
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L25
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L40
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L52
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build
The process '/home/lean/.elan/bin/lake' failed with exit code 1
|
|
Build:
test/DocPrime.lean#L37
`thm_no_doc2'` is missing a doc-string, please add one.
|
|
Build:
test/Lint.lean#L19
The namespace 'Foo' is duplicated in the declaration 'Foo.foo'
|
|
Build:
test/Lint.lean#L27
The namespace 'add' is duplicated in the declaration 'add.add'
|
|
Build:
test/Lint.lean#L41
The namespace 'Nat' is duplicated in the declaration 'Nat.Nats'
|
|
Build:
test/Lint.lean#L53
The namespace 'add' is duplicated in the declaration 'add'
|