Skip to content
continuous integration

Trigger CI for https://github.com/leanprover/lean4/pull/3186 #66517

Sign in to view logs

Trigger CI for https://github.com/leanprover/lean4/pull/3186

Trigger CI for https://github.com/leanprover/lean4/pull/3186 #66517

Triggered via push January 16, 2024 17:54
@leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
pushed 8e480de
lean-pr-testing-3186
Status Failure
Total duration 56m 41s
Artifacts –

build.yml

on: push
Lint style
43s
Lint style
Check all files imported
8s
Check all files imported
Build
55m 34s
Build
Cancel Previous Runs (CI)
2s
Cancel Previous Runs (CI)
check workflows
8s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

1 error and 10 warnings
Build
Process completed with exit code 1.
Build
unused variable `ord` [linter.unusedVariables]
Build
unused variable `ord` [linter.unusedVariables]
Build
unused variable `simple` [linter.unusedVariables]
Build
unused variable `h` [linter.unusedVariables]
Build
unused variable `h` [linter.unusedVariables]
Build: Mathlib/Mathport/Notation.lean#L533
unused variable `stx` [linter.unusedVariables]
Build: Mathlib/Data/PNat/Basic.lean#L399
unused variable `h` [linter.unusedVariables]
Build: Mathlib/Data/List/BigOperators/Basic.lean#L203
unused variable `h` [linter.unusedVariables]
Build: Mathlib/NumberTheory/Divisors.lean#L411
unused variable `h` [linter.unusedVariables]
Build: Mathlib/Combinatorics/SimpleGraph/Connectivity.lean#L1762
unused variable `a` [linter.unusedVariables]