Skip to content
continuous integration

Trigger CI for https://github.com/leanprover/lean4/pull/4242 #94903

Sign in to view logs

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

Trigger CI for https://github.com/leanprover/lean4/pull/4242 #94903

Triggered via push May 28, 2024 18:20
@leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
pushed 37f5a92
lean-pr-testing-4242
Status Failure
Total duration 1h 8m 7s
Artifacts –

build.yml

on: push
Lint style
57s
Lint style
Check all files imported
10s
Check all files imported
Build
58m 32s
Build
Cancel Previous Runs (CI)
2s
Cancel Previous Runs (CI)
check workflows
9s
check workflows
summarize_declarations
20s
summarize_declarations
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

2 errors
Build: test/LibrarySearch/basic.lean#L23
❌ Docstring on `#guard_msgs` does not match generated message:
Build
The process '/home/lean/.elan/bin/lake' failed with exit code 1