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

⚠ [1363/1367] Replayed FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
warning: ././././FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean:67:8: Continuous.prod_mk has been deprecated: use Continuous.prodMk instead
warning: ././././FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean:166:0: declaration uses 'sorry'
warning: ././././FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean:200:0: declaration uses 'sorry'
⚠ [6462/6518] Replayed FLT.AutomorphicRepresentation.Example
warning: ././././FLT/AutomorphicRepresentation/Example.lean:83:52: add_right_eq_self has been deprecated: use add_eq_left instead
warning: ././././FLT/AutomorphicRepresentation/Example.lean:119:25: add_right_eq_self has been deprecated: use add_eq_left instead
warning: ././././FLT/AutomorphicRepresentation/Example.lean:304:6: declaration uses 'sorry'
warning: ././././FLT/AutomorphicRepresentation/Example.lean:425:21: Int.mul_sign has been deprecated: use Int.mul_sign_self instead
warning: ././././FLT/AutomorphicRepresentation/Example.lean:472:6: declaration uses 'sorry'
warning: ././././FLT/AutomorphicRepresentation/Example.lean:1051:6: declaration uses 'sorry'
warning: ././././FLT/AutomorphicRepresentation/Example.lean:1058:6: declaration uses 'sorry'
warning: ././././FLT/AutomorphicRepresentation/Example.lean:1062:6: declaration uses 'sorry'
warning: ././././FLT/AutomorphicRepresentation/Example.lean:1065:6: declaration uses 'sorry'
⚠ [6463/6518] Replayed FLT.EllipticCurve.Torsion
warning: ././././FLT/EllipticCurve/Torsion.lean:34:14: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:39:8: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:43:8: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:47:8: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:54:8: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:60:4: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:63:6: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:66:6: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:72:4: declaration uses 'sorry'
warning: ././././FLT/EllipticCurve/Torsion.lean:76:4: declaration uses 'sorry'
⚠ [6464/6518] Replayed FLT.Basic.Reductions
warning: ././././FLT/Basic/Reductions.lean:323:8: declaration uses 'sorry'
warning: ././././FLT/Basic/Reductions.lean:333:8: declaration uses 'sorry'
⚠ [6477/6518] Replayed FLT.Junk.Algebra
warning: ././././FLT/Junk/Algebra.lean:1:0: using 'exit' to interrupt Lean
⚠ [6478/6518] Replayed FLT.Junk.Algebra2
warning: ././././FLT/Junk/Algebra2.lean:1:0: using 'exit' to interrupt Lean
✖ [6479/6518] Running Mathlib.LinearAlgebra.FiniteDimensional
error: no such file or directory (error code: 2)
file: ././.lake/packages/mathlib/././Mathlib/LinearAlgebra/FiniteDimensional.lean
✖ [6480/6518] Running FLT.Mathlib.Algebra.IsQuaternionAlgebra
error: ././././FLT/Mathlib/Algebra/IsQuaternionAlgebra.lean: bad import 'Mathlib.LinearAlgebra.FiniteDimensional'
⚠ [6483/6518] Replayed FLT.HaarMeasure.DistribHaarChar.Basic
warning: ././././FLT/HaarMeasure/DistribHaarChar/Basic.lean:37:19: Simps.Config.lemmasOnly has been deprecated: use -isSimp instead
⚠ [6485/6518] Replayed FLT.Mathlib.MeasureTheory.Group.Action
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:25:0: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:24:2: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:30:0: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:29:2: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:35:0: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:34:2: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:40:0: declaration uses 'sorry'
warning: ././././FLT/Mathlib/MeasureTheory/Group/Action.lean:39:2: declaration uses 'sorry'
⚠ [6486/6518] Replayed FLT.Mathlib.NumberTheory.Padics.PadicIntegers
warning: ././././FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean:58:6: declaration uses 'sorry'
⚠ [6487/6518] Replayed FLT.HaarMeasure.MeasurableSpacePadics
warning: ././././FLT/HaarMeasure/MeasurableSpacePadics.lean:67:14: declaration uses 'sorry'
✖ [6490/6518] Building FLT.Mathlib.Data.Finset.Lattice.Fold
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././FLT/Mathlib/Data/Finset/Lattice/Fold.lean -R ./././. -o ././.lake/build/lib/lean/FLT/Mathlib/Data/Finset/Lattice/Fold.olean -i ././.lake/build/lib/lean/FLT/Mathlib/Data/Finset/Lattice/Fold.ilean -c ././.lake/build/ir/FLT/Mathlib/Data/Finset/Lattice/Fold.c --json
error: ././././FLT/Mathlib/Data/Finset/Lattice/Fold.lean:3:9: 'Finset.le_sup_dite_pos' has already been declared
error: ././././FLT/Mathlib/Data/Finset/Lattice/Fold.lean:11:10: 'Finset.le_sup_dite_neg' has already been declared
error: Lean exited with code 1
✖ [6497/6518] Running Mathlib.Topology.Homeomorph
error: no such file or directory (error code: 2)
file: ././.lake/packages/mathlib/././Mathlib/Topology/Homeomorph.lean
✖ [6498/6518] Running FLT.Mathlib.Topology.Homeomorph
error: ././././FLT/Mathlib/Topology/Homeomorph.lean: bad import 'Mathlib.Topology.Homeomorph'
✖ [6500/6518] Running FLT.QuaternionAlgebra.NumberField
error: ././././FLT/QuaternionAlgebra/NumberField.lean: bad import 'FLT.Mathlib.Algebra.IsQuaternionAlgebra'
✖ [6502/6518] Running FLT
error: ././././FLT.lean: bad import 'FLT.Mathlib.Algebra.IsQuaternionAlgebra'
error: ././././FLT.lean: bad import 'FLT.Mathlib.Topology.Homeomorph'
error: ././././FLT.lean: bad import 'FLT.QuaternionAlgebra.NumberField'
✖ [6505/6518] Running FermatsLastTheorem
error: ././././FermatsLastTheorem.lean: bad import 'FLT'
✖ [6506/6518] Building FLT.Mathlib.Analysis.Normed.Ring.WithAbs
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean -R ./././. -o ././.lake/build/lib/lean/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.olean -i ././.lake/build/lib/lean/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.ilean -c ././.lake/build/ir/FLT/Mathlib/Analysis/Normed/Ring/WithAbs.c --json
error: ././././FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean:13:27: failed to synthesize
Field (WithAbs v)

Additional diagnostic information may be available using the set_option diagnostics true command.
error: ././././FLT/Mathlib/Analysis/Normed/Ring/WithAbs.lean:20:2: unknown identifier 'isUniformInducing_of_comp'
error: Lean exited with code 1
✖ [6510/6518] Building FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean -R ./././. -o ././.lake/build/lib/lean/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.olean -i ././.lake/build/lib/lean/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.ilean -c ././.lake/build/ir/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.c --json
error: ././././FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean:3:8: 'IsDedekindDomain.HeightOneSpectrum.adicValued_apply'' has already been declared
error: Lean exited with code 1
✖ [6516/6518] Building FLT.GlobalLanglandsConjectures.GLnDefs
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib/lean:././.lake/packages/batteries/.lake/build/lib/lean:././.lake/packages/Qq/.lake/build/lib/lean:././.lake/packages/aesop/.lake/build/lib/lean:././.lake/packages/proofwidgets/.lake/build/lib/lean:././.lake/packages/importGraph/.lake/build/lib/lean:././.lake/packages/LeanSearchClient/.lake/build/lib/lean:././.lake/packages/plausible/.lake/build/lib/lean:././.lake/packages/mathlib/.lake/build/lib/lean:././.lake/packages/checkdecls/.lake/build/lib/lean:././.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean -R ./././. -o ././.lake/build/lib/lean/FLT/GlobalLanglandsConjectures/GLnDefs.olean -i ././.lake/build/lib/lean/FLT/GlobalLanglandsConjectures/GLnDefs.ilean -c ././.lake/build/ir/FLT/GlobalLanglandsConjectures/GLnDefs.c --json
warning: ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean:91:0: declaration uses 'sorry'
warning: ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean:94:9: declaration uses 'sorry'
warning: ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean:238:0: declaration uses 'sorry'
warning: ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean:248:4: declaration uses 'sorry'
error: ././././FLT/GlobalLanglandsConjectures/GLnDefs.lean:294:17: unknown identifier 'obj_carrier'
error: Lean exited with code 1
Some required builds logged failures:

• Mathlib.LinearAlgebra.FiniteDimensional
• FLT.Mathlib.Algebra.IsQuaternionAlgebra
• FLT.Mathlib.Data.Finset.Lattice.Fold
• Mathlib.Topology.Homeomorph
• FLT.Mathlib.Topology.Homeomorph
• FLT.QuaternionAlgebra.NumberField
• FLT
• FermatsLastTheorem
• FLT.Mathlib.Analysis.Normed.Ring.WithAbs
• FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
• FLT.GlobalLanglandsConjectures.GLnDefs
  error: build failed