Skip to content
continuous integration

Merge branch 'nightly-testing' of github.com:leanprover-community/mat… #196642

Sign in to view logs

Merge branch 'nightly-testing' of github.com:leanprover-community/mat…

Merge branch 'nightly-testing' of github.com:leanprover-community/mat… #196642

Triggered via push June 5, 2025 11:38
@nomeatanomeata
pushed c2665dc
lean-pr-testing-8419
Status Failure
Total duration 6m 5s
Artifacts –

build.yml

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

Annotations

6 errors
Build
The process '/usr/bin/env' failed with exit code 1
Build
The process '/usr/bin/bash' failed with exit code 1
Build: Mathlib/Algebra/Group/Defs.lean#L528
@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration
Build: Mathlib/Algebra/Group/Defs.lean#L490
@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration
Build: Mathlib/Algebra/Group/Defs.lean#L469
@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration
Build: Mathlib/Algebra/Group/Defs.lean#L459
@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration