Skip to content

Merge remote-tracking branch 'origin' into localization-monoidal #151597

Merge remote-tracking branch 'origin' into localization-monoidal

Merge remote-tracking branch 'origin' into localization-monoidal #151597

Triggered via push December 23, 2024 08:42
Status Failure
Total duration 7m 59s
Artifacts

build.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

11 errors and 2 warnings
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L23
@CategoryTheory.MonoidalCategory.Pentagon definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L34
@CategoryTheory.MorphismProperty.Monoidal inductive missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L53
@CategoryTheory.LocalizedMonoidal definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L67
@CategoryTheory.Localization.Monoidal.toMonoidalCategory definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L86
@CategoryTheory.Localization.Monoidal.tensorBifunctor definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L95
CategoryTheory.Localization.Monoidal.whiskeringRight₂' definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L101
@CategoryTheory.Localization.Monoidal.tensorBifunctorIso definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L115
@CategoryTheory.Localization.Monoidal.leftUnitor definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L121
@CategoryTheory.Localization.Monoidal.rightUnitor definition missing documentation string
Build: Mathlib/CategoryTheory/Localization/Monoidal.lean#L127
@CategoryTheory.Localization.Monoidal.associator definition missing documentation string
Build
The process '/usr/bin/bash' failed with exit code 1
Cancel Previous Runs (CI)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
Lint style
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636