Skip to content
continuous integration

Update lean-toolchain for testing https://github.com/leanprover/lean4… #192280

Sign in to view logs

Update lean-toolchain for testing https://github.com/leanprover/lean4…

Update lean-toolchain for testing https://github.com/leanprover/lean4… #192280

Triggered via push May 19, 2025 03:00
@ghostghost
pushed c3fbade
lean-pr-testing-8397
Status Failure
Total duration 41m 11s
Artifacts –

build.yml

on: push
Lint style
2m 59s
Lint style
Build
41m 4s
Build
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

1 error and 9 warnings
Build
The process '/usr/bin/bash' failed with exit code 1
Build: Mathlib/Data/Quot.lean#L547
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Logic/Equiv/Set.lean#L514
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Order/Filter/Basic.lean#L354
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Order/Filter/Bases/Basic.lean#L226
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Topology/Basic.lean#L204
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Topology/Basic.lean#L212
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/GroupTheory/Sylow.lean#L172
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/MeasureTheory/Measure/MeasureSpace.lean#L636
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead
Build: Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean#L136
`nonempty_of_exists` has been deprecated: use `Exists.nonempty` instead