Skip to content
continuous integration

Some adaption #189210

Sign in to view logs

Some adaption

Some adaption #189210

Triggered via push May 8, 2025 21:50
@nomeatanomeata
pushed 25f1592
lean-pr-testing-8267
Status Failure
Total duration 5m 53s
Artifacts 1

build.yml

on: push
Lint style
1m 30s
Lint style
Build
5m 45s
Build
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

10 errors
Build: MathlibTest/fun_prop_dev.lean#L397
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/fun_prop_dev.lean#L550
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/fun_prop_dev.lean#L621
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L99
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L133
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L141
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L149
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L167
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L221
❌️ Docstring on `#guard_msgs` does not match generated message:
Build: MathlibTest/StringDiagram.lean#L275
❌️ Docstring on `#guard_msgs` does not match generated message:

Artifacts

Produced during runtime
Name Size Digest
import-graph Expired
221 KB
sha256:e5df151ba4c0f03e94e791e4b619044bd1d11febe1d042f3fc10a17cdbb8143f