`/Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lake setup-file /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/Mathlib/RepresentationTheory/Irreducible.lean -` failed:

stderr:
✖ [2/62] Building Mathlib.Tactic.Linter.DirectoryDependency (248ms)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/Mathlib/Tactic/Linter/DirectoryDependency.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean/Mathlib/Tactic/Linter/DirectoryDependency.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean/Mathlib/Tactic/Linter/DirectoryDependency.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/ir/Mathlib/Tactic/Linter/DirectoryDependency.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/ir/Mathlib/Tactic/Linter/DirectoryDependency.setup.json --json
error: Mathlib/Tactic/Linter/DirectoryDependency.lean:6:0: object file '/Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean/Lean/Elab/AssertExists.olean' of module Lean.Elab.AssertExists does not exist
error: Lean exited with code 1
✔ [28/68] Built Batteries.Tactic.Unreachable (724ms)
✔ [31/68] Built Batteries.Lean.Meta.Inaccessible (688ms)
✔ [32/71] Built Batteries.Util.LibraryNote (1.1s)
✔ [33/74] Built Batteries.CodeAction.Deprecated (1.4s)
✔ [34/74] Built ImportGraph.Lean.Environment (450ms)
✔ [35/78] Built Batteries.Tactic.Lint.Basic (1.4s)
✔ [37/78] Built Batteries.Tactic.OpenPrivate (1.5s)
✔ [38/78] Built ImportGraph.Util.FindSorry (484ms)
✔ [39/78] Built Qq.SortLocalDecls (740ms)
✔ [40/78] Built Qq.Typ (1.9s)
✔ [41/83] Built ImportGraph.RequiredModules (1.2s)
✔ [42/83] Built Qq.ForLean.ToExpr (1.9s)
✔ [43/83] Built Qq.ForLean.Do (1.6s)
✔ [44/86] Built Batteries.Tactic.Lint.TypeClass (893ms)
✔ [45/86] Built Qq.ForLean.ReduceEval (2.2s)
✔ [46/103] Built Batteries.Lean.NameMapAttribute (811ms)
✔ [47/119] Built ImportGraph.Imports (1.2s)
✔ [51/119] Built Batteries.Tactic.Alias (2.8s)
✔ [52/130] Built Batteries.Tactic.Lint.Frontend (2.6s)
✔ [53/135] Built Batteries.Tactic.Lint.Misc (1.0s)
✔ [56/136] Built Batteries.Util.ExtendedBinder (1.1s)
✔ [57/140] Built Batteries.Tactic.Lint.Simp (2.2s)
✔ [58/145] Built Batteries.Logic (894ms)
✔ [59/159] Built Batteries.Lean.Syntax (484ms)
✔ [60/159] Built Batteries.Tactic.Init (1.4s)
✔ [61/177] Built Batteries.Lean.Expr (972ms)
✔ [63/182] Built Batteries.Tactic.Lint (677ms)
✔ [106/191] Built Batteries.Linter.UnreachableTactic (1.2s)
✔ [110/194] Built Batteries.Data.Array.Basic (623ms)
✔ [111/194] Built Batteries.Control.Lemmas (517ms)
✔ [112/194] Built Batteries.Lean.MonadBacktrack (533ms)
✔ [113/194] Built Batteries.Tactic.PermuteGoals (1.1s)
✖ [114/194] Building Batteries.Tactic.Trans (4.3s)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Tactic/Trans.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Trans.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Trans.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Trans.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Trans.setup.json --json
error: Batteries/Tactic/Trans.lean:31:37: Invalid field `insertKeyValue`: The environment does not contain `Lean.Meta.DiscrTree.insertKeyValue`, so it is not possible to project the field `insertKeyValue` from an expression
  dt
of type `DiscrTree Name`
error: Lean exited with code 1
✔ [115/194] Built Batteries.Data.Array.Merge (2.3s)
✔ [116/194] Built Aesop.Script.Tactic (1.3s)
✔ [117/194] Built Aesop.Script.GoalWithMVars (1.4s)
✔ [118/194] Built Aesop.Percent (577ms)
✔ [119/194] Built Batteries.Control.LawfulMonadState (1.9s)
✔ [120/194] Built Aesop.RuleTac.FVarIdSubst (1.4s)
✔ [121/197] Built Aesop.Forward.SlotIndex (545ms)
✔ [122/197] Built Aesop.Forward.LevelIndex (592ms)
✔ [123/197] Built Aesop.Util.UnionFind (874ms)
✔ [124/197] Built Aesop.Nanos (714ms)
✔ [125/197] Built Aesop.Forward.PremiseIndex (589ms)
✔ [126/197] Built Aesop.Rule.Name (1.2s)
✔ [127/199] Built Aesop.Check (645ms)
✔ [128/203] Built Aesop.Util.UnorderedArraySet (701ms)
✔ [129/205] Built Aesop.Index.DiscrTreeConfig (1.5s)
✔ [130/205] Built Batteries.Control.OptionT (781ms)
✔ [131/205] Built Aesop.RuleTac.RuleTerm (638ms)
✔ [132/205] Built Aesop.ElabM (1.3s)
✔ [133/206] Built Aesop.Options.Public (1.6s)
✔ [134/206] Built Batteries.Lean.Meta.UnusedNames (767ms)
✔ [135/210] Built Aesop.Util.Tactic (1.3s)
✔ [136/210] Built Aesop.Util.OrderedHashSet (637ms)
✔ [137/213] Built Batteries.Control.AlternativeMonad (1.3s)
✔ [138/213] Built Aesop.Util.Unfold (1.7s)
✔ [139/213] Built Batteries.Lean.Meta.Expr (463ms)
✔ [140/216] Built Batteries.Lean.PersistentHashMap (467ms)
✔ [141/217] Built Aesop.Options.Internal (1.4s)
✔ [142/219] Built Batteries.Lean.Meta.Basic (897ms)
✔ [143/219] Built Batteries.Lean.PersistentHashSet (849ms)
✔ [144/219] Built Aesop.RuleTac.ElabRuleTerm (1.9s)
✔ [145/219] Built Batteries.Lean.Meta.DiscrTree (698ms)
✔ [146/219] Built Batteries.Lean.Meta.InstantiateMVars (575ms)
✔ [147/227] Built Batteries.Lean.Meta.SavedState (702ms)
✔ [148/227] Built Aesop.RuleSet.Name (1.3s)
✔ [149/239] Built Aesop.Options (1.2s)
✔ [150/239] Built Aesop.Util.Tactic.Unfold (1.0s)
✔ [151/242] Built Qq.Macro (9.7s)
✔ [152/251] Built Aesop.Script.TacticState (1.7s)
✔ [153/256] Built Aesop.Constants (705ms)
✔ [154/257] Built Aesop.Util.Basic (4.5s)
✔ [155/257] Built Aesop.Search.Expansion.Simp (1.2s)
✔ [156/257] Built Aesop.RuleSet.Filter (1.4s)
✔ [157/267] Built Aesop.Script.OptimizeSyntax (1.6s)
✔ [158/267] Built Batteries.Lean.HashSet (698ms)
✔ [159/273] Built Batteries.Lean.TagAttribute (634ms)
✔ [160/274] Built Aesop.Exception (1.5s)
✔ [161/274] Built Batteries.Tactic.SeqFocus (1.1s)
✔ [162/274] Built Aesop.Util.EqualUpToIds (3.2s)
✔ [163/295] Built Aesop.Script.CtorNames (1.7s)
✔ [164/295] Built Batteries.Util.ProofWanted (782ms)
✔ [165/327] Built Batteries.Control.ForInStep.Basic (682ms)
✔ [169/332] Built Qq.Delab (3.1s)
✔ [170/332] Built Aesop.Forward.Substitution (2.3s)
✔ [171/332] Built Batteries.Lean.AttributeExtra (623ms)
✖ [174/341] Building Aesop.Tracing (2.1s)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/Aesop/Tracing.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Tracing.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Tracing.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/ir/Aesop/Tracing.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/ir/Aesop/Tracing.setup.json --json
error: Aesop/Tracing.lean:156:37: Application type mismatch: The argument
  fun x => msg
has type
  ?m.16 → m MessageData
but is expected to have type
  m MessageData
in the application
  @withTraceNodeBefore α m ?m.7 ?m.8 ?m.9 ?m.10 ?m.11 ?m.12 ?m.13 ?m.14 ?m.15 opt.traceClass fun x => msg
error: Lean exited with code 1
✔ [182/411] Built Aesop.Script.Util (1.3s)
✔ [191/411] Built Aesop.Frontend.Basic (1.2s)
✔ [203/475] Built Batteries.Lean.Except (664ms)
✔ [211/477] Built Aesop.RuleTac.Forward.Basic (1.6s)
✔ [212/477] Built Batteries.Tactic.Congr (1.5s)
✔ [213/479] Built Aesop.RulePattern.Cache (1.4s)
✔ [289/481] Built Batteries.Tactic.Exact (883ms)
✔ [290/482] Built Qq.MetaM (1.8s)
✔ [291/482] Built Batteries.Linter.UnnecessarySeqFocus (1.9s)
✔ [293/483] Built Batteries.Lean.Position (524ms)
✔ [295/484] Built Batteries.CodeAction.Attr (1.2s)
✔ [296/484] Built Batteries.Data.List.ArrayMap (453ms)
✔ [297/485] Built Batteries.Linter (687ms)
✔ [298/485] Built Batteries.Tactic.Case (2.5s)
✔ [299/485] Built Qq.MatchImpl (1.7s)
✔ [300/485] Built Qq.Simp (1.5s)
✔ [301/485] Built Qq.AssertInstancesCommute (2.4s)
✔ [302/485] Built Plausible.Attr (877ms)
✔ [303/487] Built Plausible.Random (1.2s)
✔ [304/487] Built Batteries.CodeAction.Basic (1.4s)
✔ [305/487] Built Batteries.Data.List.Count (671ms)
✔ [306/487] Built Batteries.Data.List.Init.Lemmas (362ms)
✔ [307/487] Built Batteries.Tactic.Basic (833ms)
✔ [308/489] Built Batteries.Control.ForInStep.Lemmas (497ms)
✔ [309/489] Built Batteries.Tactic.GeneralizeProofs (4.9s)
✔ [310/489] Built Plausible.Gen (1.3s)
✖ [311/493] Building Batteries.Tactic.HelpCmd (5.5s)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Tactic/HelpCmd.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/HelpCmd.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/HelpCmd.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/HelpCmd.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/HelpCmd.setup.json --json
error: Batteries/Tactic/HelpCmd.lean:77:28: Invalid field `find?`: The environment does not contain `Lean.KVMap.find?`, so it is not possible to project the field `find?` from an expression
  opts
of type `KVMap`
error: Lean exited with code 1
✔ [312/500] Built Batteries.Classes.Order (1.2s)
✔ [313/500] Built Batteries.CodeAction.Misc (3.8s)
✔ [314/522] Built Qq.Commands (2.3s)
✖ [315/522] Building Batteries.Data.Array.Match (1.2s)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:138:2: `Rel` is not a field of structure `FinitenessRelation`
error: Batteries/Data/Array/Match.lean:137:44: Fields missing: `rel`

Field `rel` must be explicitly provided; its synthesized value is
  InvImage IterM.IsPlausibleSuccessorOf ?m.18
error: Batteries/Data/Array/Match.lean:146:6: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Batteries/Data/Array/Match.lean:154:10: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Batteries/Data/Array/Match.lean:162:10: failed to synthesize
  Iterator ?m.19 ?m.20 ?m.21

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Lean exited with code 1
✔ [331/536] Built Plausible.Arbitrary (944ms)
✔ [342/540] Built Batteries.Lean.EStateM (881ms)
✔ [343/541] Built Batteries.Data.List.Basic (4.9s)
✔ [345/543] Built Plausible.ArbitraryFueled (601ms)
✖ [349/544] Building Batteries.Util.Cache (887ms)
trace: .> LEAN_PATH=/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Cli/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/Qq/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/aesop/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/plausible/.lake/build/lib/lean:/Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/build/lib/lean /Users/stepannesterov/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/Batteries/Util/Cache.lean -o /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Util/Cache.olean -i /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Util/Cache.ilean -c /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Util/Cache.c --setup /Users/stepannesterov/Lean/Stepan-s-mathlib4-fork/.lake/packages/batteries/.lake/build/ir/Batteries/Util/Cache.setup.json --json
error: Batteries/Util/Cache.lean:150:8: Invalid field `insertKeyValue`: The environment does not contain `Lean.Meta.DiscrTree.insertKeyValue`, so it is not possible to project the field `insertKeyValue` from an expression
  t
of type `DiscrTree α`
error: Lean exited with code 1
✔ [353/547] Built Plausible.Sampleable (1.6s)
✔ [354/547] Built Batteries.Classes.SatisfiesM (1.4s)
✔ [359/554] Built Batteries.Data.List.Pairwise (1.1s)
✔ [365/555] Built Batteries.Data.MLList.Basic (1.6s)
✔ [367/581] Built Batteries.Data.List.Monadic (693ms)
✔ [385/618] Built Batteries.Control.Nondet.Basic (1.0s)
✔ [398/723] Built ImportGraph.Meta (1.6s)
✔ [406/781] Built Batteries.Classes.RatCast (591ms)
✔ [433/1771] Built Batteries.Data.Nat.Basic (694ms)
✔ [434/1843] Built Plausible.DeriveArbitrary (3.6s)
✔ [436/1912] Built ProofWidgets.Compat (758ms)
✔ [437/1912] Built Plausible.Testable (3.3s)
✔ [438/1912] Built ProofWidgets.Util (944ms)
✔ [439/1912] Built Batteries.Data.Nat.Lemmas (1.4s)
✔ [440/1912] Built Plausible.Functions (1.1s)
✔ [441/1912] Built Plausible.Tactic (1.1s)
✔ [442/1912] Built ProofWidgets.Cancellable (1.3s)
✔ [443/1912] Built ProofWidgets.Component.Basic (1.4s)
✔ [444/1912] Built Plausible (565ms)
✔ [445/1912] Built Batteries.Data.Fin.Basic (1.4s)
✔ [446/1912] Built ProofWidgets.Component.MakeEditLink (798ms)
✔ [447/1912] Built Qq.Match (9.8s)
✔ [448/1912] Built Batteries.Data.BinomialHeap.Basic (7.0s)
✔ [457/1912] Built Batteries.Data.List.Lemmas (6.8s)
✔ [460/1912] Built Batteries.Data.Fin.Lemmas (1.7s)
✔ [461/1912] Built Batteries.Data.List.Perm (1.3s)
✔ [462/1912] Built Qq (1.6s)
✔ [921/1912] Built ProofWidgets.Data.Html (3.4s)
✔ [923/1912] Built ProofWidgets.Component.FilterDetails (591ms)
✔ [924/1912] Built ProofWidgets.Component.OfRpcMethod (826ms)
✔ [930/1912] Built Batteries.Data.List.Scan (3.0s)
Some required targets logged failures:
- Mathlib.Tactic.Linter.DirectoryDependency
- Batteries.Tactic.Trans
- Aesop.Tracing
- Batteries.Tactic.HelpCmd
- Batteries.Data.Array.Match
- Batteries.Util.Cache
Failed to build module dependencies.