Updates available but manual intervention required

[github-actions]

Try lake update and then investigate why this update causes the lean build to fail.

Files changed in update:

• lean-toolchain
• lake-manifest.json

Build Output

⚠ [1/46] Replayed Iris.Algebra.OFE
warning: ./src//Iris/Algebra/OFE.lean:129:0: Definition `Iris.OFE.ofDiscrete` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
warning: ./src//Iris/Algebra/OFE.lean:562:0: Definition `Iris.COFE.ofDiscrete` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
warning: ./src//Iris/Algebra/OFE.lean:602:11: instance `Iris.COFE.OFunctor.cofe` must be marked with `@[reducible]` or `@[implicit_reducible]`
⚠ [2/46] Replayed Iris.Algebra.CMRA
warning: ./src//Iris/Algebra/CMRA.lean:894:11: instance `Iris.RFunctor.cmra` must be marked with `@[reducible]` or `@[implicit_reducible]`
warning: ./src//Iris/Algebra/CMRA.lean:930:11: instance `Iris.URFunctor.cmra` must be marked with `@[reducible]` or `@[implicit_reducible]`
✖ [26/61] Building Iris.BI.Extensions (875ms)
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/runner/work/iris-lean/iris-lean/./src//Iris/BI/Extensions.lean -o /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/BI/Extensions.olean -i /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/BI/Extensions.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/BI/Extensions.c --setup /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/BI/Extensions.setup.json --json
error: ./src//Iris/BI/Extensions.lean:31:18: Failed to infer universe levels in type of field `pure_forall_2`
  ∀ {α : Sort ?u.505} (φ : α → Prop), («forall».{u_1, ?u.505} fun a => iprop(⌜φ a⌝)) ⊢ ⌜∀ (a : α), φ a⌝
error: ./src//Iris/BI/Extensions.lean:31:21: Failed to infer universe levels in type of binder `α`
  Sort ?u.505
error: Lean exited with code 1
✖ [70/156] Building Iris.Algebra.Frac (1.0s)
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/runner/work/iris-lean/iris-lean/./src//Iris/Algebra/Frac.lean -o /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/Frac.olean -i /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/Frac.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Algebra/Frac.c --setup /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Algebra/Frac.setup.json --json
error: ./src//Iris/Algebra/Frac.lean:116:4: Type mismatch: After simplification, term
  H
 has type
  Add.add a x = Add.add a y
but is expected to have type
  a.car + x.car = a.car + y.car
error: Lean exited with code 1
✖ [78/156] Building Iris.Std.Namespaces (518ms)
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/runner/work/iris-lean/iris-lean/./src//Iris/Std/Namespaces.lean -o /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Std/Namespaces.olean -i /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Std/Namespaces.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Std/Namespaces.c --setup /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Std/Namespaces.setup.json --json
error: ./src//Iris/Std/Namespaces.lean:69:2: `grind` failed
case grind
X1 X2 X3 Y : CoPset
h : (X1 \ X2) \ X3 ## Y
h_1 : ¬X1 \ (X2 ∪ X3) ## Y
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] (X1 \ X2) \ X3 ## Y
    [prop] ¬X1 \ (X2 ∪ X3) ## Y
  [eqc] True propositions
    [prop] (X1 \ X2) \ X3 ## Y
  [eqc] False propositions
    [prop] X1 \ (X2 ∪ X3) ## Y
  [ematch] E-matching patterns
    [thm] in_diff: [@Membership.mem `[Pos] `[CoPset] `[instMembershipPosCoPset] (@SDiff.sdiff `[CoPset] `[instSDiff] #1 #0) #2]
    [thm] not_in_union: [@Membership.mem `[Pos] `[CoPset] `[instMembershipPosCoPset] (@Union.union `[CoPset] `[instUnion] #1 #0) #2]
error: Lean exited with code 1
✖ [79/156] Building Iris.Algebra.GenMap (2.8s)
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/runner/work/iris-lean/iris-lean/./src//Iris/Algebra/GenMap.lean -o /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/GenMap.olean -i /home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean/Iris/Algebra/GenMap.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Algebra/GenMap.c --setup /home/runner/work/iris-lean/iris-lean/.lake/build/ir/Iris/Algebra/GenMap.setup.json --json
error: ./src//Iris/Algebra/GenMap.lean:279:17: unsolved goals
case some.none.some
F : OFunctorPre
inst✝⁴ : RFunctor F
α₁✝ α₂✝ : Type ?u.46616
β₁✝ β₂✝ : Type ?u.46615
inst✝³ : OFE α₁✝
inst✝² : OFE α₂✝
inst✝¹ : OFE β₁✝
inst✝ : OFE β₂✝
f : α₂✝ -n> α₁✝
g : β₁✝ -n> β₂✝
x : GenMapOF Nat F α₁✝ β₁✝
γ : Nat
v : F α₁✝ β₁✝
h : x.car γ = some v
val✝ : F α₂✝ β₂✝
Hcore :
  match none, pcore ((RFunctor.map f g).f v) with
  | none, none => True
  | some a, some b => a ≡ b
  | x, x_1 => False
h' : pcore v = none
h'' : pcore ((OFunctor.map f g).f v) = some val✝
⊢ False

case some.some.none
F : OFunctorPre
inst✝⁴ : RFunctor F
α₁✝ α₂✝ : Type ?u.46616
β₁✝ β₂✝ : Type ?u.46615
inst✝³ : OFE α₁✝
inst✝² : OFE α₂✝
inst✝¹ : OFE β₁✝
inst✝ : OFE β₂✝
f : α₂✝ -n> α₁✝
g : β₁✝ -n> β₂✝
x : GenMapOF Nat F α₁✝ β₁✝
γ : Nat
v : F α₁✝ β₁✝
h : x.car γ = some v
val✝ : F α₁✝ β₁✝
Hcore :
  match some ((RFunctor.map f g).f val✝), pcore ((RFunctor.map f g).f v) with
  | none, none => True
  | some a, some b => a ≡ b
  | x, x_1 => False
h' : pcore v = some val✝
h'' : pcore ((OFunctor.map f g).f v) = none
⊢ False

case some.some.some
F : OFunctorPre
inst✝⁴ : RFunctor F
α₁✝ α₂✝ : Type ?u.46616
β₁✝ β₂✝ : Type ?u.46615
inst✝³ : OFE α₁✝
inst✝² : OFE α₂✝
inst✝¹ : OFE β₁✝
inst✝ : OFE β₂✝
f : α₂✝ -n> α₁✝
g : β₁✝ -n> β₂✝
x : GenMapOF Nat F α₁✝ β₁✝
γ : Nat
v : F α₁✝ β₁✝
h : x.car γ = some v
val✝¹ : F α₁✝ β₁✝
val✝ : F α₂✝ β₂✝
Hcore :
  match some ((RFunctor.map f g).f val✝¹), pcore ((RFunctor.map f g).f v) with
  | none, none => True
  | some a, some b => a ≡ b
  | x, x_1 => False
h' : pcore v = some val✝¹
h'' : pcore ((OFunctor.map f g).f v) = some val✝
⊢ (OFunctor.map f g).f val✝¹ ≡ val✝
warning: ./src//Iris/Algebra/GenMap.lean:287:18: This simp argument is unused:
  RFunctor.toOFunctor

Hint: Omit it from the simp argument list.
  simp_all ̵[̵R̵F̵u̵n̵c̵t̵o̵r̵.̵t̵o̵O̵F̵u̵n̵c̵t̵o̵r̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ./src//Iris/Algebra/GenMap.lean:290:29: This simp argument is unused:
  RFunctor.toOFunctor

Hint: Omit it from the simp argument list.
  simp only [Option.map, R̵F̵u̵n̵c̵t̵o̵r̵.̵t̵o̵O̵F̵u̵n̵c̵t̵o̵r̵,̵ ̵op, optionOp, URFunctor.map] at Hop ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Lean exited with code 1
✖ [81/156] Building Batteries.Data.List.Basic (3.6s)
trace: .> LEAN_PATH=/home/runner/work/iris-lean/iris-lean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/iris-lean/iris-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/Batteries/Data/List/Basic.lean -o /home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/List/Basic.olean -i /home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/List/Basic.ilean -c /home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Basic.c --setup /home/runner/work/iris-lean/iris-lean/.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Basic.setup.json --json
error: Batteries/Data/List/Basic.lean:202:4: `List.scanlM` has already been declared
error: Batteries/Data/List/Basic.lean:210:4: `List.scanrM` has already been declared
error: Batteries/Data/List/Basic.lean:220:4: `List.scanl` has already been declared
error: Batteries/Data/List/Basic.lean:230:4: `List.scanr` has already been declared
error: Lean exited with code 1
Some required targets logged failures:
- Iris.BI.Extensions
- Iris.Algebra.Frac
- Iris.Std.Namespaces
- Iris.Algebra.GenMap
- Batteries.Data.List.Basic
error: build failed