fix merge #64651
semorrisonbuild.yml
on: push
Cancel Previous Runs (CI)
4s
check workflows
9s
Post-CI job
0s
Annotations
11 errors
|
Lint style:
Mathlib/Tactic/SimpIntro.lean#L69
Mathlib/Tactic/SimpIntro.lean#L69: ERR_LIN: Line has more than 100 characters
|
|
Lint style
Process completed with exit code 123.
|
|
Build:
Mathlib/Data/Polynomial/Lifts.lean#L151
Tactic `simp? [coeff_monomial] at hq ` produced `simp only [coeff_map, coeff_monomial, ↓reduceIte] at hq `,
|
|
Build:
Mathlib/Probability/ProbabilityMassFunction/Monad.lean#L289
Tactic `simp? [h] at this ` produced `simp only [h, ↓reduceDite, mul_eq_zero, false_or] at this `,
|
|
Build:
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean#L673
Tactic `simp? [Nat.divisors_prime_pow hp 2] at this
|
|
Build:
Mathlib/Algebra/Lie/DirectSum.lean#L173
Tactic `simp? [h]` produced `simp only [h, ↓reduceDite, single_apply]`,
|
|
Build:
Mathlib/CategoryTheory/Monoidal/Preadditive.lean#L285
Tactic `simp? [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
|
|
Build:
Mathlib/CategoryTheory/Monoidal/Preadditive.lean#L295
Tactic `simp? [leftDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
|
|
Build:
Mathlib/CategoryTheory/Monoidal/Preadditive.lean#L328
Tactic `simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
|
|
Build:
Mathlib/CategoryTheory/Monoidal/Preadditive.lean#L340
Tactic `simp? [rightDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
|
|
Build
The process '/usr/bin/bash' failed with exit code 1
|