Skip to content
continuous integration

fixes to @[to_additive] for leanprover#lean4#12263 #6405

Sign in to view logs

fixes to @[to_additive] for leanprover#lean4#12263

fixes to @[to_additive] for leanprover#lean4#12263 #6405

Triggered via push February 2, 2026 00:49
@kim-emkim-em
pushed 2d1f297
lean-pr-testing-12263
Status Failure
Total duration 15m 19s
Artifacts –

build.yml

on: push
Build
15m 7s
Build
Lint style
1m 55s
Lint style
Post-Build Step
0s
Post-Build Step
Post-CI job
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

20 errors and 20 warnings
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
Build
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
Build
Tactic `rfl` failed: The left-hand side
Build
Type mismatch
Build
Tactic `rfl` failed: The left-hand side
Build
Type mismatch
Build
failed to synthesize instance of type class
Build
failed to synthesize instance of type class
Build
Tactic `rfl` failed: The left-hand side
Build
Type mismatch
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
`dsimp` made no progress
Build
failed to synthesize instance of type class
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Equiv.Perm.coeEmbedding` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableEq` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableLE` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableLT` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Mathlib.Meta.monadLiftOptionMetaM` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `WellFoundedGT.toWellFoundedRelation` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `WellFoundedGT.toWellFoundedRelation` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `arrowAction` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `Equiv.Perm.coeEmbedding` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `CategoryTheory.uliftCategory` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableEq` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableLE` must be marked with `@[reducible]` or `@[instance_reducible]`
Build
instance `LinearOrder.toDecidableLT` must be marked with `@[reducible]` or `@[instance_reducible]`