Skip to content
continuous integration

more fix #5634

Sign in to view logs

more fix

more fix #5634

Triggered via push December 12, 2025 10:17
@KhaKha
pushed 73dcb81
lean-pr-testing-11587
Status Failure
Total duration 23m 44s
Artifacts 1

build.yml

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

Annotations

10 errors
Build
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
No goals to be solved
Build
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
No goals to be solved
Build
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
No goals to be solved
Build
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
No goals to be solved
Build
❌️ Docstring on `#guard_msgs` does not match generated message:
Build
No goals to be solved

Artifacts

Produced during runtime
Name Size Digest
mathlib4_artifact
1.87 GB
sha256:3522b21b9c357d5c1eafd099f3982ee1fa5b96a673ebd094439c1c7e600749b1