Skip to content
continuous integration

Trigger CI for https://github.com/leanprover/lean4/pull/5474 #126743

Sign in to view logs

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

Trigger CI for https://github.com/leanprover/lean4/pull/5474 #126743

Triggered via push September 25, 2024 22:57
@leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
pushed 6e93e83
lean-pr-testing-5474
Status Failure
Total duration 51m 56s
Artifacts –

build.yml

on: push
Lint style
1m 14s
Lint style
Build
51m 49s
Build
Cancel Previous Runs (CI)
2s
Cancel Previous Runs (CI)
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

4 errors
Build: test/aesop_cat.lean#L20
could not synthesize default value for field 'w' of 'Foo' using tactics
Build: test/aesop_cat.lean#L20
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
Build: test/aesop_cat.lean#L19
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
The process '/home/lean/.elan/bin/lake' failed with exit code 1