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:

• lake-manifest.json

Build Output

warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it
⚠ [753/989] Replayed ABCExceptions.ForMathlib.Misc
warning: ABCExceptions/ForMathlib/Misc.lean:35:22: `lt_or_le` has been deprecated: use `lt_or_ge` instead
⚠ [1849/1852] Replayed ABCExceptions.Section4
warning: ABCExceptions/Section4.lean:189:77: `le_of_not_le` has been deprecated: use `le_of_not_ge` instead
warning: ABCExceptions/Section4.lean:519:8: `LT.lt.not_lt` has been deprecated: use `LT.lt.not_gt` instead
warning: ABCExceptions/Section4.lean:712:11: `LE.le.not_lt` has been deprecated: use `LE.le.not_gt` instead
warning: ABCExceptions/Section4.lean:746:8: `LE.le.not_lt` has been deprecated: use `LE.le.not_gt` instead
warning: ABCExceptions/Section4.lean:1071:8: `LT.lt.not_le` has been deprecated: use `LT.lt.not_ge` instead
warning: ABCExceptions/Section4.lean:1079:22: `le_or_lt` has been deprecated: use `le_or_gt` instead
warning: ABCExceptions/Section4.lean:1103:11: `LT.lt.not_lt` has been deprecated: use `LT.lt.not_gt` instead
warning: ABCExceptions/Section4.lean:1131:8: `LT.lt.not_le` has been deprecated: use `LT.lt.not_ge` instead
warning: ABCExceptions/Section4.lean:1530:10: `LE.le.not_lt` has been deprecated: use `LE.le.not_gt` instead
warning: ABCExceptions/Section4.lean:1573:8: `le_or_lt` has been deprecated: use `le_or_gt` instead
warning: ABCExceptions/Section4.lean:1596:50: `le_of_not_le` has been deprecated: use `le_of_not_ge` instead
warning: ABCExceptions/Section4.lean:1600:67: `le_of_not_le` has been deprecated: use `le_of_not_ge` instead
✖ [1850/1852] Building ABCExceptions.Section2
trace: .> LEAN_PATH=/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/packages/checkdecls/.lake/build/lib/lean:/home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false -Dlinter.style.longLine=true -Dlinter.style.multiGoal=true -Dlinter.oldObtain=true -Dlinter.flexible=true /home/runner/work/ABC-Exceptions/ABC-Exceptions/ABCExceptions/Section2.lean -R /home/runner/work/ABC-Exceptions/ABC-Exceptions -o /home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/build/lib/lean/ABCExceptions/Section2.olean -i /home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/build/lib/lean/ABCExceptions/Section2.ilean -c /home/runner/work/ABC-Exceptions/ABC-Exceptions/.lake/build/ir/ABCExceptions/Section2.c --json
warning: ABCExceptions/Section2.lean:376:10: `LT.lt.not_le` has been deprecated: use `LT.lt.not_ge` instead
warning: ABCExceptions/Section2.lean:622:58: `le_or_lt` has been deprecated: use `le_or_gt` instead
error: ABCExceptions/Section2.lean:819:4: type mismatch
  a
has type
  ℕ : Type
but is expected to have type
  Fin n : Type
error: ABCExceptions/Section2.lean:821:2: simp made no progress
error: ABCExceptions/Section2.lean:825:8: type mismatch
  a
has type
  ℕ : Type
but is expected to have type
  Fin n : Type
error: ABCExceptions/Section2.lean:827:2: simp made no progress
error: ABCExceptions/Section2.lean:833:62: type mismatch
  K'
has type
  ℕ : Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:925:26: type mismatch
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:926:9: type mismatch
  K
has type
  ℕ : Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:926:25: type mismatch
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:927:8: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑(?m.51157 - ?m.51156)
data : ProofData
⊢ sorry - 1 = sorry
error: ABCExceptions/Section2.lean:969:26: type mismatch
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:973:12: unsolved goals
data : ProofData
h1n : 1 ≤ n
hnX : n ≤ X
⊢ ↑(sorry ()) + 1 = K
error: ABCExceptions/Section2.lean:1026:54: Application type mismatch: In the application
  j ≠ K - 1
the argument
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:1032:18: type mismatch
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:1032:48: Application type mismatch: In the application
  j ≠ K - 1
the argument
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:1035:19: type mismatch
  K
has type
  ℕ : Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:1035:35: type mismatch
  K - 1
has type
  ℕ : outParam Type
but is expected to have type
  Fin d : Type
error: ABCExceptions/Section2.lean:1036:18: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑(?m.69614 - ?m.69613)
data : ProofData
⊢ sorry - 1 = sorry
error: ABCExceptions/Section2.lean:1051:37: simp made no progress
warning: ABCExceptions/Section2.lean:1273:9: `le_or_lt` has been deprecated: use `le_or_gt` instead
error: Lean exited with code 1
Some required builds logged failures:
- ABCExceptions.Section2
error: build failed