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

✖ [3091/3095] Building Flean.Subnorm (6.6s)
trace: .> LEAN_PATH=/home/runner/work/Flean/Flean/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /home/runner/work/Flean/Flean/Flean/Subnorm.lean -o /home/runner/work/Flean/Flean/.lake/build/lib/lean/Flean/Subnorm.olean -i /home/runner/work/Flean/Flean/.lake/build/lib/lean/Flean/Subnorm.ilean -c /home/runner/work/Flean/Flean/.lake/build/ir/Flean/Subnorm.c --setup /home/runner/work/Flean/Flean/.lake/build/ir/Flean/Subnorm.setup.json --json
error: Flean/Subnorm.lean:239:6: Tactic `apply` failed: could not unify the conclusion of `@Int.le_ceil`
  ?a ≤ ↑⌈?a⌉
with the goal
  -(q * ↑C.prec) ≤ 2 ^ C.emin * ↑⌈-(q * ↑C.prec / 2 ^ C.emin)⌉

Note: The full type of `@Int.le_ceil` is
  ∀ {α : Type ?u.6358} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), a ≤ ↑⌈a⌉

case pos
C : FloatCfg
q : ℚ
t1 : 0 < ↑C.prec
t2 : 0 < 2 ^ C.emin
t3 : 0 < ↑C.prec / 2 ^ C.emin
h : q < 0
⊢ -(q * ↑C.prec) ≤ 2 ^ C.emin * ↑⌈-(q * ↑C.prec / 2 ^ C.emin)⌉
error: Flean/Subnorm.lean:254:4: Tactic `apply` failed: could not unify the conclusion of `@Int.floor_le`
  ↑⌊?a⌋ ≤ ?a
with the goal
  2 ^ C.emin * ↑⌊q * ↑C.prec / 2 ^ C.emin⌋ ≤ q * ↑C.prec

Note: The full type of `@Int.floor_le` is
  ∀ {α : Type ?u.9586} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), ↑⌊a⌋ ≤ a

case neg
C : FloatCfg
q : ℚ
t1 : 0 < ↑C.prec
t2 : 0 < 2 ^ C.emin
t3 : 0 < ↑C.prec / 2 ^ C.emin
h : 0 ≤ q
⊢ 2 ^ C.emin * ↑⌊q * ↑C.prec / 2 ^ C.emin⌋ ≤ q * ↑C.prec
error: Flean/Subnorm.lean:272:6: Tactic `apply` failed: could not unify the conclusion of `@Int.floor_le`
  ↑⌊?a⌋ ≤ ?a
with the goal
  2 ^ C.emin * ↑⌊-(q * ↑C.prec / 2 ^ C.emin)⌋ ≤ -(q * ↑C.prec)

Note: The full type of `@Int.floor_le` is
  ∀ {α : Type ?u.6450} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), ↑⌊a⌋ ≤ a

case pos
C : FloatCfg
q : ℚ
t1 : 0 < ↑C.prec
h : q < 0
⊢ 2 ^ C.emin * ↑⌊-(q * ↑C.prec / 2 ^ C.emin)⌋ ≤ -(q * ↑C.prec)
error: Flean/Subnorm.lean:291:4: Tactic `apply` failed: could not unify the conclusion of `@Int.le_ceil`
  ?a ≤ ↑⌈?a⌉
with the goal
  q * ↑C.prec ≤ 2 ^ C.emin * ↑⌈q * ↑C.prec / 2 ^ C.emin⌉

Note: The full type of `@Int.le_ceil` is
  ∀ {α : Type ?u.11341} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), a ≤ ↑⌈a⌉

case neg
C : FloatCfg
q : ℚ
t1 : 0 < ↑C.prec
h : 0 ≤ q
⊢ q * ↑C.prec ≤ 2 ^ C.emin * ↑⌈q * ↑C.prec / 2 ^ C.emin⌉
error: Flean/Subnorm.lean:326:16: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?a * (?b + ?c)
in the target expression
  ↑⌈|q| * ↑C.prec / 2 ^ C.emin⌉ / ↑C.prec ≤ (1 + ↑⌊|q| * ↑C.prec / 2 ^ C.emin⌋) / ↑C.prec

C : FloatCfg
q : ℚ
h✝ : q ≥ 0
h' : ¬q < 0
h : StrictMono fun x ↦ x / ↑C.prec * 2 ^ C.emin
this : ↑⌈|q| * ↑C.prec / 2 ^ C.emin⌉ / ↑C.prec ≤ (1 + ↑⌊|q| * ↑C.prec / 2 ^ C.emin⌋) / ↑C.prec
⊢ ↑⌈|q| * ↑C.prec / 2 ^ C.emin⌉ / ↑C.prec ≤ (1 + ↑⌊|q| * ↑C.prec / 2 ^ C.emin⌋) / ↑C.prec
error: Lean exited with code 1
✖ [3092/3095] Building Flean.Rounding (6.9s)
trace: .> LEAN_PATH=/home/runner/work/Flean/Flean/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/Flean/Flean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /home/runner/work/Flean/Flean/Flean/Rounding.lean -o /home/runner/work/Flean/Flean/.lake/build/lib/lean/Flean/Rounding.olean -i /home/runner/work/Flean/Flean/.lake/build/lib/lean/Flean/Rounding.ilean -c /home/runner/work/Flean/Flean/.lake/build/ir/Flean/Rounding.c --setup /home/runner/work/Flean/Flean/.lake/build/ir/Flean/Rounding.setup.json --json
error: Flean/Rounding.lean:366:2: Type mismatch
  this
has type
  2 ^ Int.log 2 |q| * (↑C.prec + ↑⌊(|q| - 2 ^ Int.log 2 |q|) * ↑C.prec / 2 ^ Int.log 2 |q|⌋) ≤ ↑C.prec * |q|
but is expected to have type
  2 ^ Int.log 2 |q| * (↑C.prec + ↑⌊(|q| - 2 ^ Int.log 2 |q|) * ↑C.prec / 2 ^ Int.log 2 |q|⌋) ≤ |q| * ↑C.prec
error: Lean exited with code 1
Some required targets logged failures:
- Flean.Subnorm
- Flean.Rounding
error: build failed