`lake build` failed

[yangky11]

Hi,

I was trying to run lake update && lake build after cloning the repo. And it gave me the error message below. Could you please help? Thank you!

Building Aesop.Nanos
Building Aesop.Check
Building Std.Util.ExtendedBinder
Building Std.Tactic.OpenPrivate
Building Std.Tactic.HaveI
Building Std.Tactic.Unreachable
Building Std.Lean.TagAttribute
Building Std.Data.Option.Init.Lemmas
Building Std.Tactic.GuardExpr
Building Std.Tactic.ByCases
Building Std.Tactic.SeqFocus
Building Std.Tactic.TryThis
Building Std.Lean.Parser
Building Std.Lean.Meta.Basic
Building Std.Util.TermUnsafe
Building Std.Lean.Tactic
Building Std.Lean.NameMapAttribute
Building Std.Data.List.Init.Lemmas
Building Std.Data.Ord
Building Std.Classes.Dvd
Building Std.Classes.BEq
Building Std.Control.ForInStep.Basic
Building Std.Tactic.RCases
Building Std.Lean.Command
Building Std.Lean.Meta.LCtx
Building Std.Lean.Expr
Building Std.Lean.Meta.Expr
Building Std.Lean.PersistentHashMap
Building Std.Lean.PersistentHashSet
Building Aesop.Options.Public
Building Std.Lean.Meta.Inaccessible
Building Std.Lean.HashSet
Building Std.Lean.MonadBacktrack
Building Aesop.Percent
Building Std.Lean.AttributeExtra
Building Std.Linter.UnreachableTactic
Building Std.Tactic.SimpTrace
Building Std.Tactic.ShowTerm
Building Std.Tactic.NoMatch
Building Std.Control.ForInStep.Lemmas
Building Std.Data.Nat.Basic
Building Std.Classes.SetNotation
Building Std.Tactic.Lint.Basic
Building Std.Lean.Meta.AssertHypotheses
error: > LEAN_PATH=./build/lib:./lake-packages/std/build/lib DYLD_LIBRARY_PATH=/Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/lib:./lake-packages/std/build/lib /Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/bin/lean -DwarningAsError=true -Dlinter.missingDocs=true ./lake-packages/std/././Std/Linter/UnreachableTactic.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Linter/UnreachableTactic.olean -i ./lake-packages/std/build/lib/Std/Linter/UnreachableTactic.ilean -c ./lake-packages/std/build/ir/Std/Linter/UnreachableTactic.c
error: stdout:
./lake-packages/std/././Std/Linter/UnreachableTactic.lean:87:45: error: invalid {...} notation, expected type is not of the form (C ...)
  Linter
error: external command `/Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/bin/lean` exited with code 1
Building Std.Lean.Meta.Clear
Building Std.Lean.Meta.InstantiateMVars
Building Std.Tactic.Simpa
Building Aesop.Options.Internal
Building Aesop.Constants
Building Std.Linter.UnnecessarySeqFocus
Building Std.Lean.Meta.SavedState
Building Aesop.Options
Building Std.Data.Array.Init.Basic
error: > LEAN_PATH=./build/lib:./lake-packages/std/build/lib DYLD_LIBRARY_PATH=/Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/lib:./lake-packages/std/build/lib /Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/bin/lean -DwarningAsError=true -Dlinter.missingDocs=true ./lake-packages/std/././Std/Linter/UnnecessarySeqFocus.lean -R ./lake-packages/std/./. -o ./lake-packages/std/build/lib/Std/Linter/UnnecessarySeqFocus.olean -i ./lake-packages/std/build/lib/Std/Linter/UnnecessarySeqFocus.ilean -c ./lake-packages/std/build/ir/Std/Linter/UnnecessarySeqFocus.c
error: stdout:
./lake-packages/std/././Std/Linter/UnnecessarySeqFocus.lean:151:47: error: invalid {...} notation, expected type is not of the form (C ...)
  Linter
error: external command `/Users/kaiyuy/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/bin/lean` exited with code 1
Building Std.Data.Array.Basic
Building Std.Tactic.Lint.Misc
Building Std.Classes.Order
Building Std.Data.Char
Building Std.Tactic.Ext.Attr
Building Std.Data.String.Lemmas

[digama0]

You should not run lake update unless you are a maintainer / willing to fix bugs caused by updating lean or dependencies. Also, make sure that the version of lean used in aesop (in the lean-toolchain file) matches the version of lean used in std (in lake-packages/std/lean-toolchain), as those errors look like a version mismatch issue.

[yangky11]

Thanks Mario!