✖ [3/162] Building Std.Util.ExtendedBinder
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Util/ExtendedBinder.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Util/ExtendedBinder.olean -i ././.lake/packages/std/.lake/build/lib/Std/Util/ExtendedBinder.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Util/ExtendedBinder.c --json
error: ././.lake/packages/std/././Std/Util/ExtendedBinder.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [5/162] Building Std.Tactic.OpenPrivate
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/OpenPrivate.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/OpenPrivate.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/OpenPrivate.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/OpenPrivate.c --json
error: ././.lake/packages/std/././Std/Tactic/OpenPrivate.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [7/162] Building Std.Tactic.HaveI
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/HaveI.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/HaveI.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/HaveI.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/HaveI.c --json
error: ././.lake/packages/std/././Std/Tactic/HaveI.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [8/162] Building Std.Lean.Command
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Command.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Command.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Command.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Command.c --json
error: ././.lake/packages/std/././Std/Lean/Command.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [9/162] Building Std.Tactic.Unreachable
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/Unreachable.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/Unreachable.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/Unreachable.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/Unreachable.c --json
error: ././.lake/packages/std/././Std/Tactic/Unreachable.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [11/162] Building Std.Lean.TagAttribute
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/TagAttribute.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/TagAttribute.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/TagAttribute.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/TagAttribute.c --json
error: ././.lake/packages/std/././Std/Lean/TagAttribute.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [15/162] Building Std.Util.TermUnsafe
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Util/TermUnsafe.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Util/TermUnsafe.olean -i ././.lake/packages/std/.lake/build/lib/Std/Util/TermUnsafe.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Util/TermUnsafe.c --json
error: ././.lake/packages/std/././Std/Util/TermUnsafe.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [17/162] Building Std.Tactic.ByCases
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/ByCases.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/ByCases.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/ByCases.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/ByCases.c --json
error: ././.lake/packages/std/././Std/Tactic/ByCases.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [18/162] Building Std.Tactic.SeqFocus
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/SeqFocus.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/SeqFocus.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/SeqFocus.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/SeqFocus.c --json
error: ././.lake/packages/std/././Std/Tactic/SeqFocus.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [20/162] Building Std.Lean.Position
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Position.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Position.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Position.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Position.c --json
error: ././.lake/packages/std/././Std/Lean/Position.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [21/162] Building Std.Data.Json
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/Json.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/Json.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/Json.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/Json.c --json
error: ././.lake/packages/std/././Std/Data/Json.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [22/162] Building Std.Lean.Syntax
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Syntax.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Syntax.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Syntax.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Syntax.c --json
error: ././.lake/packages/std/././Std/Lean/Syntax.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [25/162] Building Std.Lean.LocalContext
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/LocalContext.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/LocalContext.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/LocalContext.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/LocalContext.c --json
error: ././.lake/packages/std/././Std/Lean/LocalContext.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashMap/Basic.olean' of module Std.Data.HashMap.Basic does not exist
error: Lean exited with code 1
✖ [62/162] Building Std.Data.Option.Init.Lemmas
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/Option/Init/Lemmas.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/Option/Init/Lemmas.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/Option/Init/Lemmas.c --json
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:16:16: 'Option.getD_none' has already been declared
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:17:16: 'Option.getD_some' has already been declared
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:19:16: 'Option.map_none'' has already been declared
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:20:16: 'Option.map_some'' has already been declared
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:22:16: 'Option.none_bind' has already been declared
error: ././.lake/packages/std/././Std/Data/Option/Init/Lemmas.lean:23:16: 'Option.some_bind' has already been declared
error: Lean exited with code 1
✖ [63/162] Building Std.Lean.Parser
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Parser.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Parser.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Parser.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Parser.c --json
error: ././.lake/packages/std/././Std/Lean/Parser.lean:14:4: 'Lean.Parser.Tactic.simpArg' has already been declared
error: ././.lake/packages/std/././Std/Lean/Parser.lean:16:0: 'Lean.Parser.Tactic.simpArgs' has already been declared
error: ././.lake/packages/std/././Std/Lean/Parser.lean:29:4: 'Lean.Parser.Tactic.dsimpArg' has already been declared
error: ././.lake/packages/std/././Std/Lean/Parser.lean:31:0: 'Lean.Parser.Tactic.dsimpArgs' has already been declared
error: Lean exited with code 1
✖ [65/162] Building Std.Lean.Tactic
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Tactic.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Tactic.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Tactic.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Tactic.c --json
error: ././.lake/packages/std/././Std/Lean/Tactic.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashMap/Basic.olean' of module Std.Data.HashMap.Basic does not exist
error: Lean exited with code 1
✖ [66/162] Building Std.Util.ProofWanted
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Util/ProofWanted.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Util/ProofWanted.olean -i ././.lake/packages/std/.lake/build/lib/Std/Util/ProofWanted.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Util/ProofWanted.c --json
error: ././.lake/packages/std/././Std/Util/ProofWanted.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashSet/Basic.olean' of module Std.Data.HashSet.Basic does not exist
error: Lean exited with code 1
✖ [68/162] Building Std.Lean.InfoTree
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/InfoTree.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/InfoTree.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/InfoTree.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/InfoTree.c --json
error: ././.lake/packages/std/././Std/Lean/InfoTree.lean:7:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashMap/Basic.olean' of module Std.Data.HashMap.Basic does not exist
error: Lean exited with code 1
✖ [72/162] Building Std.Data.List.Init.Basic
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/List/Init/Basic.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/List/Init/Basic.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/List/Init/Basic.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/List/Init/Basic.c --json
error: ././.lake/packages/std/././Std/Data/List/Init/Basic.lean:14:4: 'List.zipWithAll' has already been declared
error: ././.lake/packages/std/././Std/Data/List/Init/Basic.lean:19:16: 'List.zipWithAll_nil_right' has already been declared
error: ././.lake/packages/std/././Std/Data/List/Init/Basic.lean:23:16: 'List.zipWithAll_nil_left' has already been declared
error: ././.lake/packages/std/././Std/Data/List/Init/Basic.lean:27:16: 'List.zipWithAll_cons_cons' has already been declared
error: Lean exited with code 1
✖ [74/162] Building Std.Tactic.RCases
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Tactic/RCases.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Tactic/RCases.olean -i ././.lake/packages/std/.lake/build/lib/Std/Tactic/RCases.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Tactic/RCases.c --json
error: ././.lake/packages/std/././Std/Tactic/RCases.lean:6:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashMap/Basic.olean' of module Std.Data.HashMap.Basic does not exist
error: Lean exited with code 1
✖ [75/162] Building Std.Lean.Meta.Expr
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/Meta/Expr.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/Meta/Expr.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/Meta/Expr.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/Meta/Expr.c --json
error: ././.lake/packages/std/././Std/Lean/Meta/Expr.lean:7:0: object file '././.lake/packages/std/.lake/build/lib/Std/Data/HashMap/Basic.olean' of module Std.Data.HashMap.Basic does not exist
error: Lean exited with code 1
✖ [92/162] Building Std.Data.Array.Init.Basic
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/Array/Init/Basic.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/Array/Init/Basic.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/Array/Init/Basic.c --json
error: ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean:16:4: 'Array.zipWithIndex' has already been declared
error: ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean:20:14: 'Array.toListAppend' has already been declared
error: ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean:28:4: 'Array.ofFn' has already been declared
error: ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean:35:4: 'Array.range' has already been declared
error: ././.lake/packages/std/././Std/Data/Array/Init/Basic.lean:39:4: 'Array.flatten' has already been declared
error: Lean exited with code 1
✖ [96/162] Building Std.Data.Fin.Init.Lemmas
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/Fin/Init/Lemmas.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/Fin/Init/Lemmas.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/Fin/Init/Lemmas.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/Fin/Init/Lemmas.c --json
error: ././.lake/packages/std/././Std/Data/Fin/Init/Lemmas.lean:7:16: 'Fin.zero_eta' has already been declared
error: Lean exited with code 1
✖ [102/162] Building Std.Classes.Dvd
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Classes/Dvd.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Classes/Dvd.olean -i ././.lake/packages/std/.lake/build/lib/Std/Classes/Dvd.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Classes/Dvd.c --json
error: ././.lake/packages/std/././Std/Classes/Dvd.lean:8:6: 'Dvd' has already been declared
error: Lean exited with code 1
✖ [104/162] Building Std.Classes.BEq
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Classes/BEq.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Classes/BEq.olean -i ././.lake/packages/std/.lake/build/lib/Std/Classes/BEq.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Classes/BEq.c --json
error: ././.lake/packages/std/././Std/Classes/BEq.lean:14:6: 'PartialEquivBEq' has already been declared
error: ././.lake/packages/std/././Std/Classes/BEq.lean:20:16: 'beq_eq_false_iff_ne' has already been declared
error: Lean exited with code 1
✖ [108/162] Building Std.Data.Ord
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Data/Ord.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Data/Ord.olean -i ././.lake/packages/std/.lake/build/lib/Std/Data/Ord.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Data/Ord.c --json
error: ././.lake/packages/std/././Std/Data/Ord.lean:9:18: (kernel) constant has already been declared 'Ordering.ofNat'
error: ././.lake/packages/std/././Std/Data/Ord.lean:12:4: 'Ordering.swap' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:35:20: 'Ordering.then' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:42:4: 'Ordering.isEq' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:49:4: 'Ordering.isNe' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:56:4: 'Ordering.isLT' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:63:4: 'Ordering.isGT' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:70:4: 'Ordering.isGE' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:81:14: 'compareLex' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:87:14: 'compareOn' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:96:14: 'Ord.toBEq' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:102:14: 'Ord.toLT' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:108:14: 'Ord.toLE' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:114:14: 'Ord.opposite' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:120:14: 'Ord.on' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:126:14: 'Ord.lex' has already been declared
error: ././.lake/packages/std/././Std/Data/Ord.lean:133:14: 'Ord.lex'' has already been declared
error: Lean exited with code 1
✖ [134/162] Building Std.Lean.PersistentHashMap
trace: .> LEAN_PATH=././.lake/packages/std/.lake/build/lib:././.lake/packages/auto/.lake/build/lib:././.lake/packages/Duper/.lake/build/lib:././.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/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/shreyas/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dlinter.missingDocs=true ././.lake/packages/std/././Std/Lean/PersistentHashMap.lean -R ././.lake/packages/std/./. -o ././.lake/packages/std/.lake/build/lib/Std/Lean/PersistentHashMap.olean -i ././.lake/packages/std/.lake/build/lib/Std/Lean/PersistentHashMap.ilean -c ././.lake/packages/std/.lake/build/ir/Std/Lean/PersistentHashMap.c --json
error: ././.lake/packages/std/././Std/Lean/PersistentHashMap.lean:18:17: invalid field 'size', the environment does not contain 'Lean.PersistentHashMap.size'
  m
has type
  PersistentHashMap α β
error: ././.lake/packages/std/././Std/Lean/PersistentHashMap.lean:20:6: invalid field 'size', the environment does not contain 'Lean.PersistentHashMap.size'
  m
has type
  PersistentHashMap α β
error: ././.lake/packages/std/././Std/Lean/PersistentHashMap.lean:25:4: 'Lean.PersistentHashMap.toArray' has already been declared
error: Lean exited with code 1
Some required builds logged failures:
- Std.Util.ExtendedBinder
- Std.Tactic.OpenPrivate
- Std.Tactic.HaveI
- Std.Lean.Command
- Std.Tactic.Unreachable
- Std.Lean.TagAttribute
- Std.Util.TermUnsafe
- Std.Tactic.ByCases
- Std.Tactic.SeqFocus
- Std.Lean.Position
- Std.Data.Json
- Std.Lean.Syntax
- Std.Lean.LocalContext
- Std.Data.Option.Init.Lemmas
- Std.Lean.Parser
- Std.Lean.Tactic
- Std.Util.ProofWanted
- Std.Lean.InfoTree
- Std.Data.List.Init.Basic
- Std.Tactic.RCases
- Std.Lean.Meta.Expr
- Std.Data.Array.Init.Basic
- Std.Data.Fin.Init.Lemmas
- Std.Classes.Dvd
- Std.Classes.BEq
- Std.Data.Ord
- Std.Lean.PersistentHashMap
error: build failed