⚠ [717/753] Replayed PolyFun.Control.Comonad.Instances
warning: PolyFun/Control/Comonad/Instances.lean:283:44: This simp argument is unused:
zip
Hint: Omit it from the simp argument list.
simp [CoseqLeft.coseqLeft, Functor.map, z̵i̵p̵,̵ ̵NonEmptyList.map]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PolyFun/Control/Comonad/Instances.lean:286:46: This simp argument is unused:
zip
Hint: Omit it from the simp argument list.
simp [CoseqRight.coseqRight, Functor.map, z̵i̵p̵,̵ ̵NonEmptyList.map]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✖ [5564/5758] Building PolyFun.Control.Monad.Algebra (2.2s)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.31.0-rc1/bin/lean /home/runner/work/PolyFun/PolyFun/PolyFun/Control/Monad/Algebra.lean -o /home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean/PolyFun/Control/Monad/Algebra.olean -i /home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean/PolyFun/Control/Monad/Algebra.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/build/ir/PolyFun/Control/Monad/Algebra.c --setup /home/runner/work/PolyFun/PolyFun/.lake/build/ir/PolyFun/Control/Monad/Algebra.setup.json --json
error: PolyFun/Control/Monad/Algebra.lean:216:4: Type mismatch: After simplification, term
μ_bind_mono
(fun y ↦
collapse <$>
match y with
| Except.ok a => (f a).run
| Except.error e => pure (Except.error e))
(fun y ↦
collapse <$>
match y with
| Except.ok a => (g a).run
| Except.error e => pure (Except.error e))
(fun y ↦
Except.casesOn (motive := fun t ↦
y = t →
μ
(collapse <$>
match y with
| Except.ok a => (f a).run
| Except.error e => pure (Except.error e)) ≤
μ
(collapse <$>
match y with
| Except.ok a => (g a).run
| Except.error e => pure (Except.error e)))
y
(fun e h ↦
Eq.symm h ▸
of_eq_true
(Eq.trans
(congr
(congrArg LE.le
(Eq.trans
(congrArg μ
(map_pure
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥)
(Except.error e)))
(μ_pure ⊥)))
(Eq.trans
(congrArg μ
(map_pure
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥)
(Except.error e)))
(μ_pure ⊥)))
(Std.le_refl._simp_1 ⊥)))
(fun a h ↦ Eq.symm h ▸ id (hfg a)) (Eq.refl y))
x.run
has type
@LE.le l inst✝¹.toCompleteSemilatticeInf.toLE
(μ do
let y ← x.run
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥) <$>
match y with
| Except.ok a => (f a).run
| Except.error e => pure (Except.error e))
(μ do
let y ← x.run
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥) <$>
match y with
| Except.ok a => (g a).run
| Except.error e => pure (Except.error e))
but is expected to have type
@LE.le l inst✝¹.toCompleteSemilatticeInf.toLE
(μ do
let a ← x.run
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥) <$>
match a with
| Except.ok x => (f x).run
| Except.error e => pure (Except.error e))
(μ do
let a ← x.run
(fun y ↦
match y with
| Except.ok z => z
| Except.error a => ⊥) <$>
match a with
| Except.ok x => (g x).run
| Except.error e => pure (Except.error e))
error: PolyFun/Control/Monad/Algebra.lean:203:40: (kernel) declaration has metavariables 'MAlgOrdered.instExceptT'
error: Lean exited with code 1
✖ [6792/7088] Building PolyFun.PFunctor.Basic (3.1s)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.31.0-rc1/bin/lean /home/runner/work/PolyFun/PolyFun/PolyFun/PFunctor/Basic.lean -o /home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean/PolyFun/PFunctor/Basic.olean -i /home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean/PolyFun/PFunctor/Basic.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/build/ir/PolyFun/PFunctor/Basic.c --setup /home/runner/work/PolyFun/PolyFun/.lake/build/ir/PolyFun/PFunctor/Basic.setup.json --json
error: PolyFun/PFunctor/Basic.lean:395:2: Type mismatch: After simplification, term
equivB_symm_apply_of_eq e hEqA b
has type
@Eq (P.B a) ((e.equivB a).symm ((_root_.Equiv.cast ⋯).symm ((e.equivB (e.equivA.symm (e.equivA a))) b)))
(_root_.cast ⋯ b)
but is expected to have type
@Eq (P.B a) ((e.equivB a).symm (((_root_.Equiv.cast ⋯).trans (e.equivB (e.equivA.symm (e.equivA a))).symm).symm b))
(_root_.cast ⋯ b)
error: Lean exited with code 1
Some required targets logged failures:
- PolyFun.Control.Monad.Algebra
- PolyFun.PFunctor.Basic
error: build failed
Try
lake updateand then investigate why this update causes the lean build to fail.Files changed in update:
Build Output