Skip to content
continuous integration

Update to nightly test #196603

Sign in to view logs

Update to nightly test

Update to nightly test #196603

Triggered via push June 5, 2025 10:03
@nomeatanomeata
pushed 2b96e5b
lean-pr-testing-8419
Status Failure
Total duration 4m 19s
Artifacts –

build.yml

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

Annotations

11 errors
Build
The process '/usr/bin/env' failed with exit code 1
Build: Mathlib/Data/Option/Basic.lean#L148
unsolved goals
Build
simp made no progress
Build
simp made no progress
Build
unsolved goals
Build
unsolved goals
Build
unsolved goals
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