Skip to content
continuous integration

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

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… #192687

Triggered via push May 20, 2025 15:22
@ghostghost
pushed 781b9da
lean-pr-testing-8419
Status Failure
Total duration 3m 40s
Artifacts –

build.yml

on: push
Lint style
2m 31s
Lint style
Build
3m 32s
Build
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

11 errors
Build
The process '/usr/bin/env' failed with exit code 1
Build: Mathlib/Algebra/Homology/ComplexShape.lean#L213
dsimp made no progress
Build: Mathlib/Algebra/Homology/ComplexShape.lean#L216
dsimp made no progress
Build: Mathlib/Combinatorics/Quiver/Path.lean#L233
unsolved goals
Build: Mathlib/Logic/Equiv/Basic.lean#L470
unsolved goals
Build: Mathlib/Logic/Equiv/Basic.lean#L486
unsolved goals
Build: Mathlib/CategoryTheory/Functor/Category.lean#L121
unsolved goals
Build: Mathlib/CategoryTheory/Functor/Category.lean#L154
could not synthesize default value for field 'naturality' of 'CategoryTheory.NatTrans' using tactics
Build: Mathlib/CategoryTheory/Functor/Category.lean#L154
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
Build: Mathlib/CategoryTheory/Functor/Category.lean#L162
could not synthesize default value for field 'naturality' of 'CategoryTheory.NatTrans' using tactics
Build: Mathlib/CategoryTheory/Functor/Category.lean#L162
tactic 'aesop' failed, failed to prove the goal after exhaustive search.