I have a "build failed" problem

[yuchen814]

Thank you very much if you can help me solve this problem！
Error message：
✖ [267/528] Building Batteries.Data.List.Basic
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib:/Users/yuchen/.elan/toolchains/leanprover--lean4---v4.11.0/lib/lean:/Users/yuchen/.elan/toolchains/leanprover--lean4---v4.11.0/lib /Users/yuchen/.elan/toolchains/leanprover--lean4---v4.11.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean -R ././.lake/packages/batteries/./. -o ././.lake/packages/batteries/.lake/build/lib/Batteries/Data/List/Basic.olean -i ././.lake/packages/batteries/.lake/build/lib/Batteries/Data/List/Basic.ilean -c ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Basic.c --json
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:534:19: unsolved goals
α : Type u_1
l : List α
L : List (List α)
h : l.isEmpty = true ∨ L.any isEmpty = true
⊢ (L.sections.bind fun s => []) = []
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:542:6: unknown constant 'Array.foldl_eq_foldl_toList'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:542:6: tactic 'rewrite' failed, equality or iff proof expected
?m.48353
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).data
⊢ ((foldr sectionsTR.go #[[]] L).data.bind fun s => map (fun a => a :: s) l) =
(Array.foldl (fun acc' l' => foldl (fun acc' a => acc'.push (a :: l')) acc' l) #[]
(foldr sectionsTR.go #[[]] L)).data
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:580:6: unknown constant 'Array.foldl_toList_eq_bind'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:580:6: tactic 'rewrite' failed, equality or iff proof expected
?m.49271
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ (l₁.bind fun a => map (Prod.mk a) l₂) = (foldl (fun acc a => foldl (fun acc b => acc.push (a, b)) acc l₂) #[] l₁).data
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:596:6: unknown constant 'Array.foldl_toList_eq_bind'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:596:6: tactic 'rewrite' failed, equality or iff proof expected
?m.49853
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ (l₁.bind fun a => map (Sigma.mk a) (l₂ a)) =
(foldl (fun acc a => foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).data
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:696:18: unknown constant 'List.splitAt'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:805:44: unknown constant 'Array.foldl_toList_eq_map'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:805:16: unsolved goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
acc : Array γ
head✝ : α
tail✝ : List α
⊢ (foldl (fun acc a => acc.push (f a none)) (acc.push (f head✝ none)) tail✝).data =
acc.data ++ f head✝ none :: map (fun a => f a none) tail✝
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:874:43: unknown constant 'Array.foldl_toList_eq_map'
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:874:16: unsolved goals
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
acc : Array γ
head✝ : α
tail✝ : List α
⊢ (foldl (fun acc a => acc.push (f a none)) (acc.push (f head✝ none)) tail✝).data =
acc.data ++ f head✝ none :: map (fun a => f a none) tail✝
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:971:22: invalid field 'splitAt', the environment does not contain 'List.splitAt'
xs
has type
List α
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:982:22: invalid field 'splitAt', the environment does not contain 'List.splitAt'
xs
has type
List α
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:989:17: declaration uses 'sorry'
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:989:17: declaration uses 'sorry'
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:987:10: declaration uses 'sorry'
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:990:4: unused variable n
note: this linter can be disabled with set_option linter.unusedVariables false
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:990:11: unused variable xs
note: this linter can be disabled with set_option linter.unusedVariables false
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:1098:13: unused variable l₁
note: this linter can be disabled with set_option linter.unusedVariables false
warning: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:1098:16: unused variable l₂
note: this linter can be disabled with set_option linter.unusedVariables false
error: ././.lake/packages/batteries/././Batteries/Data/List/Basic.lean:1098:46: expected token
error: Lean exited with code 1
Some required builds logged failures:

• Batteries.Classes.SatisfiesM
• Aesop.Script.GoalWithMVars
• Aesop.RuleTac.FVarIdSubst
• Aesop.Script.OptimizeSyntax
• Batteries.Lean.HashSet
• Batteries.Lean.Meta.Inaccessible
• Aesop.Util.EqualUpToIds
• Batteries.Linter.UnreachableTactic
• Batteries.Tactic.Lint.Misc
• Batteries.Data.Nat.Lemmas
• Aesop.Util.UnorderedArraySet
• Batteries.Data.List.Basic
  error: build failed

My lean version：4.11.0
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.6.0"

[yuchen814]

oh, sorry, I think this is also related to mathlib, it will be automatically updated to 4.13.0-rc3 when I update. Seems to have similar problems already

[yangky11]

I just updated LeanCopilot to support v4.14.0 and v4.15.0-rc1. Can you try again and see if the issue still persists?