✔ [3/40] Built Batteries.Lean.Position (758ms)
✔ [4/40] Built Batteries.Tactic.Unreachable (705ms)
✔ [7/48] Built Batteries.Lean.Meta.Inaccessible (620ms)
✔ [8/49] Built Batteries.Tactic.Lint.Basic (1.4s)
✔ [9/51] Built ImportGraph.Imports.ImportGraph (561ms)
✔ [10/53] Built Mathlib.Tactic.Linter.DirectoryDependency (1.9s)
✔ [11/53] Built ImportGraph.Lean.Environment (496ms)
✔ [12/53] Built ImportGraph.Imports.Redundant (629ms)
✔ [13/53] Built Batteries.Tactic.Lint.Misc (1.4s)
✔ [14/56] Built ImportGraph.Imports.RequiredModules (1.1s)
✔ [15/57] Built Batteries.Util.LibraryNote (1.2s)
✔ [16/59] Built Batteries.Lean.Syntax (433ms)
✔ [17/59] Built ImportGraph.Graph.TransitiveClosure (700ms)
✔ [18/59] Built ImportGraph.Tools.ImportDiff (931ms)
✔ [19/59] Built Mathlib.Tactic.Linter.Header (1.8s)
✔ [20/59] Built ImportGraph.Tools.MinImports (814ms)
✔ [21/59] Built ImportGraph.Tools.RedundantImports (720ms)
✔ [22/59] Built ImportGraph.Tools.FindHome (1.1s)
✔ [23/59] Built Batteries.Tactic.HelpCmd (2.9s)
✔ [24/59] Built Mathlib.Tactic.TypeStar (726ms)
✔ [25/59] Built Mathlib.Tactic.MinImports (1.7s)
✔ [26/59] Built Mathlib.Util.ParseCommand (765ms)
✔ [27/59] Built Batteries.Util.ProofWanted (3.2s)
✔ [28/59] Built Mathlib.Tactic.DeclarationNames (705ms)
✔ [29/59] Built Mathlib.Tactic.Linter.TacticDocumentation (670ms)
✔ [30/59] Built Mathlib.Tactic.Linter.UnusedTacticExtension (1.0s)
✔ [31/59] Built Mathlib.Tactic.Linter.Whitespace (1.7s)
✔ [32/59] Built Mathlib.Tactic.Linter.PrivateModule (920ms)
✔ [33/59] Built Mathlib.Lean.Environment (595ms)
✔ [34/59] Built Mathlib.Lean.Elab.Tactic.Meta (710ms)
✔ [35/59] Built Mathlib.Tactic.Linter.OldObtain (859ms)
✔ [36/59] Built Mathlib.Tactic.Linter.Multigoal (1.1s)
✔ [37/59] Built Mathlib.Lean.Expr.Basic (1.8s)
✔ [38/59] Built Mathlib.Tactic.Linter.HashCommandLinter (1.2s)
✔ [39/59] Built Mathlib.Tactic.Linter.GlobalAttributeIn (1.0s)
✔ [40/59] Built Mathlib.Tactic.Linter.EmptyLine (1.2s)
✔ [41/59] Built Mathlib.Tactic.Linter.FlexibleLinter (2.9s)
✔ [42/59] Built Mathlib.Tactic.Linter.DocString (1.6s)
✔ [43/59] Built Mathlib.Tactic.Linter.AuxLemma (853ms)
✔ [44/59] Built Mathlib.Tactic.Linter.DocPrime (1.9s)
✔ [45/61] Built Mathlib.Tactic.Lemma (687ms)
✔ [46/61] Built Mathlib.Tactic.Linter.DeprecatedSyntaxLinter (1.6s)
✔ [47/61] Built Mathlib.Lean.Linter (610ms)
✔ [48/61] Built ImportGraph.Tools (903ms)
✔ [49/61] Built Mathlib.Tactic.AdaptationNote (1.1s)
✔ [50/61] Built Mathlib.Tactic.ExtractGoal (1.6s)
✔ [51/66] Built Mathlib.Lean.Elab.InfoTree (1.0s)
✔ [53/66] Built Mathlib.Tactic.Linter.UnusedTactic (1.3s)
✔ [54/69] Built Mathlib.Lean.ContextInfo (1.1s)
✔ [55/69] Built Batteries.Tactic.Lint.TypeClass (992ms)
✔ [56/70] Built Mathlib.Tactic.Linter.Style (2.9s)
✔ [57/70] Built Mathlib.Tactic.Linter.UnusedInstancesInType (1.8s)
✔ [58/76] Built Batteries.Tactic.Lint.Simp (1.8s)
✔ [59/79] Built Mathlib.Tactic.TacticAnalysis (1.9s)
✔ [60/79] Built Batteries.Lean.NameMapAttribute (795ms)
✔ [61/80] Built Batteries.Tactic.Lint.Frontend (2.7s)
✔ [62/81] Built Mathlib.Tactic.Linter.OverlappingInstances (2.7s)
✔ [63/81] Built Batteries.CodeAction.Deprecated (1.2s)
✔ [64/84] Built Batteries.Tactic.Lint (602ms)
✔ [65/91] Built Mathlib.Tactic.Linter.Lint (1.1s)
✔ [66/100] Built Batteries.Tactic.Trans (3.1s)
✔ [67/108] Built Batteries.Tactic.Alias (2.5s)
✔ [68/111] Built Mathlib.Tactic.TacticAnalysis.Declarations (3.9s)
✔ [69/117] Built Batteries.Util.ExtendedBinder (1.1s)
✔ [70/121] Built Batteries.Logic (732ms)
✔ [71/121] Built Mathlib.Init (929ms)
✔ [72/125] Built Batteries.Lean.Expr (929ms)
✔ [73/125] Built Batteries.Tactic.Init (1.6s)
✔ [74/125] Built Batteries.Linter.UnreachableTactic (1.2s)
✔ [75/125] Built Mathlib.Lean.Elab.Term (804ms)
✔ [76/125] Built Mathlib.Tactic.Simps.NotationClass (1.4s)
✔ [77/125] Built Mathlib.Tactic.Inhabit (1.1s)
✔ [78/125] Built Mathlib.Logic.IsEmpty.Defs (1.1s)
✔ [79/125] Built Mathlib.Util.CompileInductive (2.4s)
✔ [80/125] Built Mathlib.Logic.Nonempty (1.2s)
✔ [81/125] Built Mathlib.Tactic.Push.Attr (1.7s)
✔ [82/125] Built Mathlib.Tactic.ExtendDoc (938ms)
✔ [83/125] Built Mathlib.Logic.ExistsUnique (1.8s)
✔ [84/125] Built Mathlib.Lean.PrettyPrinter.Delaborator (1.2s)
✔ [85/125] Built Mathlib.Util.AddRelatedDecl (2.0s)
✔ [86/125] Built Mathlib.Data.String.Defs (965ms)
✔ [87/125] Built Mathlib.Tactic.Translate.Attributes (866ms)
✔ [88/125] Built Mathlib.Tactic.Eqns (903ms)
✔ [89/125] Built Mathlib.Tactic.Translate.UnfoldBoundary (2.4s)
✔ [90/125] Built Mathlib.Lean.Meta.Simp (1.5s)
✔ [91/125] Built Mathlib.Lean.Name (1.4s)
✔ [92/125] Built Mathlib.Tactic.SimpRw (1.4s)
✔ [93/125] Built Mathlib.Tactic.Translate.Reorder (4.6s)
✔ [94/125] Built Mathlib.Lean.Meta (1.2s)
✔ [95/127] Built Mathlib.Util.WithWeakNamespace (885ms)
✔ [96/127] Built Mathlib.Tactic.Attr.Register (1.8s)
✔ [97/129] Built Mathlib.Tactic.Use (2.2s)
✔ [98/129] Built Mathlib.Logic.Nontrivial.Defs (1.3s)
✔ [99/129] Built Mathlib.Tactic.Core (2.2s)
✔ [100/129] Built Mathlib.Tactic.Translate.GuessName (1.9s)
✔ [101/129] Built Mathlib.Tactic.MkIffOfInductiveProp (2.8s)
✔ [102/129] Built Mathlib.Tactic.ScopedNS (3.8s)
✔ [103/129] Built Mathlib.Logic.Function.Defs (2.5s)
✔ [104/129] Built Mathlib.Tactic.Substs (1.4s)
✔ [105/129] Built Mathlib.Logic.Basic (4.8s)
✔ [106/129] Built Mathlib.Tactic.SplitIfs (1.0s)
✔ [107/130] Built Mathlib.Tactic.SetNotationForOrder (3.0s)
✔ [108/135] Built Mathlib.Tactic.Simps.Basic (8.8s)
✔ [109/135] Built Mathlib.Logic.Relator (1.3s)
✔ [110/137] Built Mathlib.Util.AtLocation (1.4s)
✔ [111/137] Built Mathlib.Tactic.Conv (2.7s)
✔ [112/139] Built Mathlib.Data.Nat.Notation (1.1s)
✔ [113/141] Built Mathlib.Data.Stream.Defs (1.9s)
✖ [114/141] Building Batteries.Data.Nat.Basic (644ms)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0/bin/lean /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/Batteries/Data/Nat/Basic.lean -o /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.olean -i /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Nat/Basic.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.c --setup /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.setup.json --json
error: Batteries/Data/Nat/Basic.lean:95:4: `Nat.sqrt` has already been declared
error: Lean exited with code 1
✔ [116/141] Built Mathlib.Tactic.Push (3.9s)
✔ [117/148] Built Mathlib.Data.Int.Notation (888ms)
✔ [119/149] Built Batteries.Lean.TagAttribute (541ms)
✔ [120/149] Built Mathlib.Tactic.Contrapose (1.6s)
✔ [121/151] Built Batteries.Tactic.SeqFocus (1.1s)
✔ [122/152] Built Batteries.Lean.AttributeExtra (628ms)
✔ [123/156] Built Mathlib.Util.Notation3 (11s)
✔ [124/156] Built Mathlib.Data.Ordering.Basic (782ms)
✔ [125/158] Built Mathlib.Tactic.Translate.Core (13s)
✔ [126/158] Built Batteries.Lean.Except (620ms)
✔ [127/158] Built Batteries.Tactic.Exact (702ms)
✔ [130/160] Built Mathlib.Tactic.GCongr.ForwardAttr (955ms)
✔ [131/166] Built Batteries.Linter.UnnecessarySeqFocus (1.6s)
✔ [132/166] Built Aesop.Script.Tactic (496ms)
✔ [133/166] Built Batteries.Control.Lemmas (623ms)
✔ [134/167] Built Batteries.Linter (634ms)
✔ [135/167] Built Mathlib.Tactic.Translate.TagUnfoldBoundary (1.4s)
✔ [136/169] Built Aesop.Script.GoalWithMVars (648ms)
✔ [137/172] Built Batteries.Tactic.Basic (723ms)
✔ [138/172] Built Aesop.Nanos (737ms)
✔ [139/173] Built Batteries.Control.LawfulMonadState (1.7s)
✔ [140/173] Built Aesop.Index.DiscrTreeConfig (513ms)
✔ [141/173] Built Batteries.Classes.Order (1.3s)
✔ [142/175] Built Batteries.Control.OptionT (872ms)
✔ [143/181] Built Mathlib.Tactic.Translate.ToDual (2.2s)
✔ [144/181] Built Batteries.Data.Array.Merge (1.0s)
✔ [145/181] Built Batteries.Lean.MonadBacktrack (457ms)
✔ [146/181] Built Batteries.Tactic.PermuteGoals (955ms)
✔ [147/184] Built Batteries.Control.AlternativeMonad (1.1s)
✔ [148/184] Built Mathlib.Tactic.ToDual (1000ms)
✔ [149/185] Built Aesop.Util.UnorderedArraySet (673ms)
✔ [150/185] Built Aesop.Check (825ms)
✔ [151/185] Built Batteries.Lean.Meta.Basic (762ms)
✔ [152/185] Built Aesop.Rule.Name (996ms)
✔ [153/185] Built Aesop.Options.Public (1.0s)
✔ [154/186] Built Mathlib.Order.Defs.Prop (986ms)
✔ [155/186] Built Mathlib.Order.Defs.PartialOrder (2.3s)
✔ [156/186] Built Batteries.Lean.Meta.SavedState (738ms)
✔ [157/186] Built Mathlib.Data.Set.Defs (2.9s)
✔ [158/186] Built Aesop.Options.Internal (493ms)
✔ [159/189] Built Aesop.Script.TacticState (866ms)
✔ [160/189] Built Aesop.Util.Basic (3.2s)
✔ [161/191] Built Aesop.Script.OptimizeSyntax (913ms)
✔ [162/195] Built Mathlib.Order.Defs.LinearOrder (2.4s)
✔ [163/196] Built Mathlib.Order.Defs.Unbundled (2.4s)
✔ [164/196] Built Aesop.Tracing (1.0s)
✔ [165/196] Built Aesop.Forward.LevelIndex (555ms)
✔ [166/196] Built Aesop.Forward.PremiseIndex (474ms)
✔ [167/196] Built Aesop.Util.EqualUpToIds (5.8s)
✔ [168/196] Built Aesop.Percent (1.2s)
✔ [169/196] Built Mathlib.Logic.Relation (4.3s)
✔ [170/196] Built Aesop.Stats.Basic (2.8s)
✔ [171/196] Built Mathlib.Logic.Function.Basic (5.3s)
✔ [172/196] Built Aesop.Script.Util (966ms)
✔ [173/196] Built Aesop.Forward.Substitution (1.7s)
⚠ [174/200] Built PolyFun.Control.Bisimulation (2.5s)
warning: PolyFun/Control/Bisimulation.lean:49:0: `LTS`: universes `uMove`, `uState` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.
Note: This linter can be disabled with `set_option linter.checkUnivs false`
✔ [175/200] Built Mathlib.Logic.Unique (1.7s)
✔ [176/200] Built Mathlib.Data.Subtype (1.0s)
✔ [177/200] Built Aesop.RulePattern.Cache (502ms)
✔ [178/200] Built Aesop.Index.Basic (1.0s)
✔ [179/200] Built Aesop.Script.Step (1.7s)
✔ [180/202] Built Mathlib.Data.FunLike.Basic (1.4s)
✔ [181/202] Built Mathlib.Tactic.GCongr.Core (10s)
✔ [182/202] Built Aesop.Script.SScript (753ms)
✔ [183/202] Built Aesop.BaseM (870ms)
✔ [184/202] Built Aesop.Script.UScript (737ms)
✔ [185/203] Built PolyFun.Control.Coalgebra (1.1s)
✔ [187/203] Built Mathlib.Data.FunLike.Embedding (1.3s)
✔ [188/203] Built Aesop.Forward.SlotIndex (777ms)
✔ [189/203] Built Mathlib.Data.Quot (3.4s)
✔ [190/203] Built Aesop.Script.Check (870ms)
✔ [191/209] Built Aesop.Script.UScriptToSScript (1.5s)
✔ [192/209] Built Aesop.RuleTac.GoalDiff (1.7s)
✔ [193/209] Built Aesop.Util.UnionFind (744ms)
✔ [194/209] Built Aesop.RulePattern (2.4s)
✔ [195/213] Built Mathlib.Data.FunLike.Equiv (1.1s)
✔ [196/213] Built Aesop.RuleTac.RuleTerm (612ms)
✔ [197/213] Built Aesop.Script.StructureStatic (1.5s)
✔ [198/213] Built Batteries.Data.UInt (1.4s)
✔ [199/215] Built Aesop.Script.StructureDynamic (2.3s)
✔ [200/215] Built Aesop.RuleTac.Basic (899ms)
✔ [201/215] Built Aesop.Script.CtorNames (1.0s)
✔ [202/217] Built Aesop.Script.Main (1.4s)
✔ [203/217] Built Aesop.ElabM (881ms)
✔ [204/218] Built Aesop.RuleTac.ElabRuleTerm (1.5s)
✔ [205/218] Built Aesop.Util.Tactic.Ext (1.7s)
✔ [206/222] Built Aesop.Util.Tactic (594ms)
✔ [207/225] Built Aesop.Script.ScriptM (1.0s)
✔ [208/225] Built Aesop.RuleTac.Forward.Basic (945ms)
✔ [209/227] Built Aesop.Util.Unfold (1.3s)
✔ [210/227] Built Mathlib.Logic.Equiv.Defs (5.7s)
⚠ [211/231] Built Batteries.Data.Array.Basic (5.7s)
warning: Batteries/Data/Array/Basic.lean:149:0: Definition `unsafe_sizeFitsUSize` is a proposition; use `theorem` instead of `def`
Note: This linter can be disabled with `set_option linter.defProp false`
✔ [212/231] Built Batteries.Lean.Meta.UnusedNames (672ms)
✔ [213/231] Built Aesop.Constants (507ms)
✔ [214/231] Built Aesop.Util.Tactic.Unfold (954ms)
✔ [215/231] Built Aesop.EMap (1.2s)
✔ [216/232] Built Aesop.Forward.RuleInfo (1.9s)
✔ [217/236] Built Aesop.Util.OrderedHashSet (920ms)
✔ [218/237] Built Aesop.Rule.Forward (847ms)
✔ [219/237] Built Batteries.Lean.Meta.Expr (756ms)
✔ [220/239] Built Batteries.Lean.PersistentHashMap (719ms)
✔ [221/240] Built Aesop.Forward.Match.Types (883ms)
✔ [222/240] Built Aesop.Script.SpecificTactics (3.6s)
✔ [223/240] Built Batteries.Lean.Meta.InstantiateMVars (638ms)
✔ [224/244] Built Batteries.Lean.Meta.DiscrTree (534ms)
✔ [225/244] Built Batteries.Lean.PersistentHashSet (587ms)
✔ [226/244] Built Aesop.RuleTac.Descr (698ms)
✔ [227/247] Built Aesop.RuleSet.Name (436ms)
✔ [228/248] Built Aesop.Index.Forward (1.0s)
✔ [229/250] Built Aesop.Rule.Basic (592ms)
✔ [230/252] Built Aesop.Index.RulePattern (1.2s)
✔ [231/252] Built Aesop.RuleSet.Filter (614ms)
✔ [232/254] Built Batteries.Lean.HashSet (466ms)
✔ [233/255] Built Aesop.Rule (931ms)
✔ [234/256] Built Aesop.RuleTac.Apply (1.1s)
✔ [235/256] Built Aesop.Index (1.9s)
✔ [236/256] Built Aesop.RuleTac.Cases (1.2s)
✔ [237/258] Built Aesop.RuleSet.Member (809ms)
✔ [238/259] Built Aesop.Tree.UnsafeQueue (846ms)
✔ [239/260] Built Aesop.RuleTac.Preprocess (652ms)
✔ [240/262] Built Aesop.Search.Expansion.Basic (714ms)
✔ [241/268] Built Aesop.RuleTac.Tactic (1.1s)
✔ [242/269] Built Aesop.Forward.Match (2.3s)
✔ [243/269] Built Aesop.Search.Expansion.Simp (753ms)
✔ [244/269] Built Aesop.Exception (647ms)
✔ [245/270] Built Aesop.Tree.Data.ForwardRuleMatches (811ms)
✔ [246/271] Built Aesop.RuleTac.Forward (2.6s)
✔ [247/277] Built Aesop.RuleTac (754ms)
✔ [248/279] Built Batteries.Control.ForInStep.Basic (471ms)
✔ [249/279] Built Mathlib.Logic.Equiv.Prod (14s)
✔ [250/281] Built PolyFun.Control.Comonad.Basic (1.7s)
✔ [251/282] Built Aesop.RuleSet (5.0s)
✔ [252/284] Built Aesop.Builder.Basic (830ms)
✔ [253/284] Built Aesop.Frontend.Extension.Init (992ms)
✔ [254/284] Built Aesop.Builder.Constructors (1.0s)
✔ [255/286] Built Aesop.Builder.Cases (987ms)
✔ [256/286] Built Aesop.Builder.NormSimp (1.0s)
✔ [257/287] Built Aesop.Builder.Tactic (889ms)
✔ [258/290] Built Aesop.Frontend.Extension (1.1s)
✔ [259/291] Built Aesop.Forward.State (9.4s)
✔ [260/293] Built Aesop.Builder.Apply (846ms)
✔ [261/293] Built Aesop.Builder.Unfold (746ms)
✔ [262/293] Built Batteries.Data.BinomialHeap.Basic (7.7s)
✔ [263/293] Built Aesop.Forward.State.ApplyGoalDiff (982ms)
✖ [264/293] Building Aesop.Builder.Forward (2.3s)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0/bin/lean /home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/Aesop/Builder/Forward.lean -o /home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.olean -i /home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean/Aesop/Builder/Forward.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.c --setup /home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.setup.json --json
error: Aesop/Builder/Forward.lean:32:8: typeclass instance problem is stuck
Max ?m.15
Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Max` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
error: Lean exited with code 1
✔ [265/293] Built Aesop.Stats.Extension (731ms)
✔ [266/297] Built Aesop.Tree.Data (2.5s)
✔ [267/297] Built Aesop.Forward.State.Initial (875ms)
✔ [268/300] Built Aesop.Builder.Default (767ms)
✔ [269/300] Built Aesop.Frontend.Basic (496ms)
✔ [270/300] Built Aesop.Stats.File (742ms)
✔ [271/300] Built Aesop.Stats.Report (1.3s)
✔ [272/300] Built Aesop.Tree.Traversal (981ms)
✔ [277/301] Built Aesop.Tree.RunMetaM (858ms)
✔ [278/302] Built Aesop.Tree.TreeM (1.4s)
✔ [280/303] Built Aesop.Search.Queue.Class (592ms)
✔ [282/303] Built Aesop.Tree.State (1.2s)
✔ [283/303] Built Aesop.Tree.Stats (1.1s)
✔ [284/303] Built Aesop.Tree.Free (846ms)
✔ [285/303] Built Aesop.Tree.Tracing (2.3s)
✔ [286/303] Built Aesop.Forward.State.UpdateGoal (830ms)
✔ [287/304] Built Aesop.Tree.ExtractProof (1.7s)
✔ [289/304] Built Aesop.Tree.ExtractScript (2.3s)
✔ [290/305] Built Aesop.Search.Queue (904ms)
✔ [292/306] Built Aesop.Search.SearchM (1.3s)
✔ [294/312] Built Aesop.Search.RuleSelection (1.0s)
✔ [297/312] Built Aesop.Tree.Check (2.0s)
✔ [299/312] Built Aesop.Tree.AddRapp (3.5s)
✔ [303/317] Built Qq.ForLean.ToExpr (666ms)
✔ [304/321] Built Qq.ForLean.ReduceEval (813ms)
✔ [305/323] Built Aesop.Saturate (8.5s)
✔ [308/328] Built Qq.Typ (659ms)
✔ [309/328] Built Qq.ForLean.Do (712ms)
✔ [312/334] Built Qq.SortLocalDecls (634ms)
✔ [313/337] Built Plausible.Shrinkable (759ms)
✔ [314/339] Built Plausible.Random (1.2s)
✔ [315/342] Built Plausible.Attr (675ms)
✔ [316/343] Built Aesop.Search.Expansion.Norm (4.6s)
✔ [317/343] Built Plausible.Gen (1.7s)
✔ [318/343] Built Plausible.DeriveShrinkable (2.6s)
✔ [319/344] Built Batteries.Tactic.Case (2.5s)
✔ [320/345] Built Plausible.Arbitrary (916ms)
✔ [321/346] Built Aesop.Search.Expansion (3.5s)
✔ [322/346] Built Batteries.CodeAction.Attr (1.2s)
✔ [323/346] Built Plausible.ArbitraryFueled (625ms)
✔ [324/346] Built Plausible.Sampleable (1.1s)
✔ [325/346] Built Qq.Macro (8.0s)
✔ [326/346] Built Batteries.CodeAction.Basic (1.2s)
✔ [327/351] Built Aesop.Search.ExpandSafePrefix (1.5s)
✔ [328/351] Built Batteries.Tactic.GeneralizeProofs (4.0s)
✔ [330/351] Built Plausible.Functions (856ms)
✔ [331/351] Built Batteries.CodeAction.Misc (3.2s)
✔ [332/351] Built Plausible.DeriveArbitrary (2.7s)
✔ [333/351] Built Qq.Commands (1.8s)
✖ [334/352] Building Plausible.Testable (2.8s)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0/bin/lean /home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/Plausible/Testable.lean -o /home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.olean -i /home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean/Plausible/Testable.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.c --setup /home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/ir/Plausible/Testable.setup.json --json
error: Plausible/Testable.lean:383:67: Application type mismatch: The argument
addShrinks (n + 1) res
has type
TestResult (β (SampleableExt.interp candidate))
but is expected to have type
?m.278 __r✝⁵ __r✝⁴ candidate __s✝ __r✝² res __r✝¹ __r✝ candidate
in the application
⟨candidate, addShrinks (n + 1) res⟩
error: Lean exited with code 1
✔ [338/355] Built LeanSearchClient.Basic (580ms)
✔ [339/356] Built Qq.Delab (2.2s)
✔ [340/356] Built Qq.MetaM (978ms)
✔ [341/359] Built Mathlib.Tactic.ApplyCongr (1.1s)
✔ [342/359] Built LeanSearchClient.Syntax (2.9s)
✔ [343/359] Built Aesop.Search.Main (5.4s)
✔ [344/359] Built Qq.MatchImpl (755ms)
✔ [346/359] Built Qq.AssertInstancesCommute (1.8s)
✔ [347/361] Built Qq.Simp (706ms)
✔ [348/361] Built Batteries.Data.List.Basic (5.7s)
✔ [350/362] Built Mathlib.Lean.Meta.Basic (1.1s)
✔ [351/363] Built Mathlib.Tactic.ApplyWith (1.2s)
✔ [352/363] Built Mathlib.Tactic.PPWithUniv (1.3s)
✔ [353/363] Built LeanSearchClient.LoogleSyntax (1.0s)
✔ [354/364] Built Batteries.CodeAction.Match (1.5s)
✔ [355/365] Built Mathlib.Tactic.ApplyAt (1.1s)
✔ [356/365] Built Mathlib.Tactic.ByCases (1.1s)
✔ [357/365] Built LeanSearchClient (626ms)
✔ [358/365] Built Mathlib.Tactic.ByContra (1.2s)
✔ [359/366] Built Batteries.CodeAction (663ms)
✔ [360/367] Built Mathlib.Tactic.Basic (1.9s)
✔ [361/368] Built Mathlib.Tactic.CasesM (1.8s)
✔ [362/369] Built Mathlib.Tactic.Check (1.6s)
✔ [363/369] Built Mathlib.Tactic.ClearExclamation (899ms)
✔ [364/369] Built Qq.Match (6.5s)
✔ [365/377] Built Mathlib.Tactic.Choose (2.4s)
✔ [366/377] Built Mathlib.Tactic.ClearExcept (989ms)
✔ [373/377] Built Qq (439ms)
✔ [374/390] Built Mathlib.Tactic.Clear_ (743ms)
✔ [377/392] Built ProofWidgets.Compat (598ms)
✔ [378/392] Built ProofWidgets.Util (1.1s)
✔ [379/396] Built Mathlib.Tactic.NthRewrite (1.2s)
✔ [380/398] Built ProofWidgets.Component.Basic (1.2s)
✔ [381/398] Built Mathlib.Control.Combinators (970ms)
✔ [382/398] Built Mathlib.Tactic.Attr.Core (929ms)
✔ [383/398] Built ProofWidgets.Component.Panel.Basic (964ms)
✔ [384/399] Built ProofWidgets.Component.MakeEditLink (1.1s)
✔ [385/400] Built Mathlib.Control.Basic (1.5s)
✔ [386/407] Built Mathlib.Tactic.DepRewrite (6.1s)
✔ [387/407] Built ProofWidgets.Data.Html (4.9s)
✔ [388/407] Built Mathlib.Lean.FoldEnvironment (1.3s)
✔ [389/411] Built ProofWidgets.Component.RefreshComponent (1.5s)
✔ [390/411] Built Mathlib.Lean.Meta.RefinedDiscrTree.Basic (2.0s)
✔ [391/411] Built ProofWidgets.Component.FilterDetails (873ms)
✔ [392/411] Built Mathlib.Lean.GoalsLocation (1.0s)
✔ [393/411] Built Mathlib.Tactic.Widget.SelectInsertParamsClass (1.1s)
✔ [394/414] Built Mathlib.Tactic.GRewrite.Core (10s)
✔ [395/416] Built Mathlib.Lean.Meta.RefinedDiscrTree.Initialize (2.4s)
✔ [396/416] Built Mathlib.Lean.Meta.KAbstractPositions (1.3s)
✔ [397/417] Built Mathlib.Lean.Meta.RefinedDiscrTree.Encode (1.0s)
✔ [398/417] Built Mathlib.Tactic.Widget.SelectPanelUtils (1.6s)
✔ [399/419] Built ProofWidgets.Cancellable (1.5s)
✔ [400/419] Built Mathlib.Tactic.Coe (1.4s)
✔ [401/421] Built ProofWidgets.Component.OfRpcMethod (1.3s)
✔ [402/422] Built Mathlib.Lean.Meta.RefinedDiscrTree.Lookup (2.5s)
✔ [403/423] Built Mathlib.Tactic.GRewrite.Elab (3.1s)
✔ [404/426] Built Mathlib.Lean.Meta.RefinedDiscrTree (1.0s)
✔ [405/426] Built Mathlib.Tactic.Constructor (1.1s)
✔ [406/427] Built Mathlib.Lean.Meta.CongrTheorems (2.4s)
✔ [407/427] Built Mathlib.Tactic.GRewrite (699ms)
✔ [408/428] Built Mathlib.Lean.MessageData.Trace (913ms)
✔ [409/428] Built Mathlib.Tactic.Widget.Conv (3.5s)
✔ [410/429] Built Mathlib.Tactic.DefEqTransformations (3.0s)
✔ [411/429] Built Mathlib.Tactic.DeprecateTo (2.1s)
✔ [412/430] Built Mathlib.Tactic.DSimpPercent (1.3s)
✔ [413/430] Built Mathlib.Tactic.TermCongr (5.3s)
✔ [414/431] Built Mathlib.Tactic.CongrExclamation (5.2s)
✔ [415/431] Built Mathlib.Tactic.ExistsI (1.3s)
✔ [416/431] Built Mathlib.Tactic.ErwQuestion (1.9s)
✔ [417/431] Built Mathlib.Tactic.ClickSuggestions.Util (4.9s)
✔ [418/433] Built Mathlib.Tactic.CongrM (1.0s)
✔ [419/433] Built Mathlib.Tactic.DefEqAbuse (2.9s)
✔ [420/433] Built Mathlib.Tactic.ClickSuggestions.Unfold (1.6s)
✔ [421/434] Built Mathlib.Tactic.FailIfNoProgress (1.8s)
✔ [422/437] Built Mathlib.Tactic.ClickSuggestions.SectionState (1.8s)
✔ [423/437] Built Batteries.Util.Cache (772ms)
✔ [424/437] Built Mathlib.Tactic.Convert (3.5s)
✔ [425/437] Built Mathlib.Tactic.FunProp.Decl (1.8s)
✔ [426/437] Built Mathlib.Tactic.ClickSuggestions.ApplyAt (1.8s)
✔ [427/437] Built Mathlib.Tactic.ClickSuggestions.Apply (1.8s)
✔ [428/439] Built Mathlib.Tactic.FunProp.Mor (1.4s)
✔ [429/444] Built Mathlib.Tactic.ClickSuggestions.Rewrite (2.6s)
✔ [430/444] Built Mathlib.Tactic.ClickSuggestions.GRewrite (3.3s)
✔ [431/449] Built Mathlib.Tactic.Find (1.4s)
✔ [432/450] Built Mathlib.Tactic.FunProp.ToBatteries (2.4s)
✔ [433/451] Built Mathlib.Tactic.GCongr.CoreAttrs (790ms)
✔ [434/451] Built Mathlib.Tactic.GrindAttrs (1.4s)
✔ [435/452] Built Batteries.Data.MLList.Basic (1.7s)
✔ [436/453] Built Mathlib.Tactic.ClickSuggestions.FindPremises (2.6s)
✔ [437/453] Built Mathlib.Tactic.GuardGoalNums (864ms)
✔ [438/453] Built Mathlib.Tactic.FunProp.FunctionData (2.1s)
✔ [439/453] Built Mathlib.Tactic.GuardHypNums (847ms)
✔ [440/455] Built Batteries.Control.Nondet.Basic (818ms)
✔ [441/456] Built Mathlib.Tactic.InferParam (1.1s)
✔ [442/456] Built Mathlib.Tactic.HigherOrder (1.5s)
✔ [443/456] Built Mathlib.Tactic.FunProp.Types (1.9s)
✔ [444/456] Built Mathlib.Tactic.Hint (1.4s)
✔ [445/458] Built Mathlib.Util.TermReduce (1.4s)
✔ [446/458] Built Mathlib.Tactic.ClickSuggestions.TryPremises (3.1s)
✔ [447/458] Built Mathlib.Tactic.GCongr (878ms)
✔ [448/459] Built Mathlib.Tactic.Lift (1.8s)
✔ [449/461] Built Mathlib.Tactic.Linter.HaveLetLinter (1.2s)
✔ [450/461] Built Mathlib.Tactic.FunProp.Theorems (2.5s)
✔ [451/462] Built Mathlib.Tactic.IrreducibleDef (2.3s)
✔ [452/463] Built Mathlib.Tactic.Linter.MinImports (1.7s)
✔ [453/463] Built Mathlib.Tactic.Linter.PPRoundtrip (1.3s)
✔ [454/463] Built Mathlib.Tactic.Linter.UpstreamableDecl (1.2s)
✔ [455/464] Built Mathlib.Tactic.ClickSuggestions (1.9s)
✔ [456/465] Built Mathlib.Tactic.FunProp.Attr (1.0s)
✔ [457/465] Built Mathlib.Tactic.OfNat (919ms)
✔ [458/465] Built Mathlib.Tactic.Linter (744ms)
✔ [459/466] Built Mathlib.Tactic.Observe (1.7s)
✔ [460/467] Built Mathlib.Tactic.RSuffices (1.4s)
✔ [461/471] Built Mathlib.Tactic.Recover (1.2s)
✔ [462/471] Built Mathlib.Tactic.Relation.Rfl (1.2s)
✔ [463/472] Built Mathlib.Util.Tactic (812ms)
✔ [464/473] Built Mathlib.Tactic.Rename (1.2s)
✔ [465/473] Built Mathlib.Tactic.Says (1.6s)
✔ [466/474] Built Mathlib.Tactic.RenameBVar (1.1s)
✔ [467/475] Built Mathlib.Tactic.Set (1.9s)
✔ [468/476] Built Mathlib.Tactic.SimpIntro (1.5s)
✔ [469/477] Built Mathlib.Tactic.Spread (1.7s)
✔ [470/478] Built Mathlib.Tactic.FunProp.Core (8.1s)
✔ [471/478] Built Mathlib.Tactic.Simproc.ExistsAndEq (2.0s)
✔ [472/479] Built Mathlib.Tactic.Subsingleton (1.9s)
✔ [473/480] Built Mathlib.Tactic.SuccessIfFailWithMsg (1.2s)
✔ [474/481] Built Mathlib.Tactic.SudoSetOption (1.0s)
✔ [475/482] Built Mathlib.Tactic.SwapVar (1.0s)
✔ [476/483] Built Mathlib.Tactic.ToFun (1.2s)
✔ [477/484] Built Mathlib.Tactic.FunProp.Elab (2.1s)
✔ [478/485] Built Mathlib.Tactic.ToExpr (1.2s)
✔ [479/485] Built Mathlib.Tactic.ToLevel (833ms)
✔ [480/486] Built Mathlib.Tactic.Trace (969ms)
✔ [481/487] Built Mathlib.Tactic.FunProp (892ms)
✔ [482/488] Built Mathlib.Tactic.UnsetOption (951ms)
✔ [483/489] Built Mathlib.Tactic.Tauto (3.1s)
✔ [484/490] Built Mathlib.Tactic.Widget.CongrM (1.1s)
✔ [485/491] Built Mathlib.Tactic.Widget.Calc (3.2s)
✔ [486/492] Built Mathlib.Tactic.Variable (3.6s)
✔ [487/497] Built Mathlib.Tactic.WLOG (2.0s)
✔ [488/497] Built Mathlib.Util.TransImports (1.1s)
✔ [489/497] Built Mathlib.Util.PrintSorries (1.6s)
⚠ [490/498] Built PolyFun.Control.Lawful.Basic (622ms)
warning: PolyFun/Control/Lawful/Basic.lean:31:0: automatically included section variable(s) unused in theorem `LawfulMonad.do_bind_pure`:
[Monad m]
[LawfulMonad m]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [Monad m] [LawfulMonad m] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [491/501] Built Mathlib.Tactic.Widget.LibraryRewrite (5.2s)
✔ [492/501] Built Mathlib.Util.CountHeartbeats (2.6s)
✔ [493/504] Built Mathlib.Util.WhatsNew (1.3s)
✔ [497/509] Built Mathlib.Data.Option.Defs (862ms)
✔ [498/509] Built Mathlib.Logic.IsEmpty.Basic (1.1s)
✔ [500/513] Built Batteries.Tactic.Congr (1.6s)
✔ [501/514] Built Mathlib.Logic.Function.Conjugate (1.2s)
✔ [503/515] Built Mathlib.Logic.Function.ULift (913ms)
✔ [504/515] Built Mathlib.Order.Notation (2.2s)
✔ [505/517] Built Mathlib.Logic.Function.Iterate (1.7s)
✔ [506/517] Built Mathlib.Tactic.FastInstance (2.5s)
✔ [507/517] Built Mathlib.Data.Bool.Basic (2.0s)
✔ [508/518] Built Mathlib.Logic.Pairwise (1.4s)
✔ [509/522] Built Mathlib.Data.Int.Order.Basic (1.6s)
✔ [510/533] Built Mathlib.Data.Set.CoeSort (1.1s)
✔ [511/540] Built Mathlib.Data.Prod.Basic (2.4s)
✔ [512/547] Built Mathlib.Control.EquivFunctor (1.5s)
✔ [514/550] Built Mathlib.Tactic.CrossRefAttribute (2.3s)
✔ [515/552] Built Mathlib.Tactic.FBinop (3.1s)
✔ [516/552] Built Mathlib.Data.Sigma.Basic (2.0s)
✔ [517/552] Built Mathlib.Data.SProd (1.6s)
✔ [519/558] Built Mathlib.Data.Sum.Basic (2.3s)
✔ [520/559] Built Mathlib.Control.ULift (1.4s)
✔ [521/559] Built Mathlib.Data.Prod.PProd (1.2s)
✔ [522/563] Built Mathlib.Tactic.Monotonicity.Attr (1.1s)
✔ [523/563] Built Mathlib.Order.Basic (7.6s)
✔ [525/563] Built Mathlib.Order.Bounds.Defs (1.1s)
✔ [526/563] Built Mathlib.Util.PPOptions (927ms)
✔ [527/570] Built Mathlib.Logic.Equiv.Sum (2.8s)
✔ [531/574] Built Mathlib.Order.ULift (1.3s)
✔ [532/576] Built Mathlib.Order.OrderDual (2.2s)
✔ [533/576] Built Mathlib.Tactic.Translate.ToAdditive (1.9s)
✔ [534/576] Built Mathlib.Order.Interval.Set.Defs (1.7s)
✔ [535/576] Built Mathlib.Order.Compare (2.1s)
✔ [537/579] Built Mathlib.Tactic.ToAdditive (1.2s)
✔ [538/587] Built Mathlib.Order.Max (2.0s)
✔ [540/590] Built Mathlib.Order.RelClasses (3.5s)
✔ [570/592] Built Batteries.Control.ForInStep.Lemmas (570ms)
✔ [571/592] Built Mathlib.Control.Functor (1.6s)
✔ [572/592] Built Mathlib.Util.Delaborators (7.2s)
✔ [574/592] Built Mathlib.Data.List.Monad (1.2s)
✔ [575/597] Built Mathlib.Algebra.Notation.Defs (2.0s)
✔ [576/597] Built Mathlib.Logic.OpClass (960ms)
✔ [577/614] Built Mathlib.Algebra.Notation.Prod (1.9s)
✔ [583/614] Built Mathlib.Algebra.Notation.Pi.Defs (1.0s)
✔ [584/637] Built Batteries.Data.List.Pairwise (1.0s)
✔ [587/641] Built Mathlib.Data.List.Defs (3.3s)
✔ [590/643] Built Mathlib.Algebra.NeZero (1.2s)
✔ [591/648] Built Mathlib.Algebra.Order.ZeroLEOne (1.5s)
✔ [599/649] Built Mathlib.Data.Finite.Defs (1.5s)
✔ [600/658] Built Mathlib.Algebra.Regular.Defs (1.2s)
✔ [601/664] Built Mathlib.Order.Lex (1.9s)
✔ [605/669] Built Mathlib.Data.Nat.BinaryRec (1.8s)
✔ [606/669] Built Mathlib.Logic.Nontrivial.Basic (1.4s)
✔ [607/669] Built Mathlib.Order.TypeTags (1.5s)
✔ [608/687] Built Mathlib.Data.Int.Init (4.0s)
✔ [614/716] Built Mathlib.Data.Option.NAry (2.0s)
✔ [623/757] Built Mathlib.Data.List.Flatten (2.7s)
✔ [624/757] Built Mathlib.Algebra.Notation.Pi.Basic (2.2s)
✔ [638/826] Built Mathlib.Lean.Expr.ExtraRecognizers (1.2s)
✔ [648/826] Built Mathlib.Data.Int.DivMod (1.1s)
✔ [669/826] Built Mathlib.Data.Countable.Defs (1.8s)
✔ [670/827] Built Mathlib.Tactic.Nontriviality.Core (2.8s)
✔ [671/827] Built Mathlib.Data.ENat.Defs (1.2s)
✔ [672/839] Built Mathlib.Tactic.Nontriviality (823ms)
✔ [676/841] Built Mathlib.Algebra.Group.Defs (10s)
✔ [680/841] Built Batteries.Data.List.Lemmas (17s)
✔ [682/841] Built Mathlib.Data.PNat.Notation (954ms)
✔ [683/841] Built Mathlib.Data.Nat.Bits (1.9s)
✔ [684/841] Built Mathlib.Algebra.GroupWithZero.Defs (2.6s)
✔ [687/841] Built Mathlib.Algebra.Group.Int.Defs (1.7s)
✔ [689/841] Built Mathlib.Algebra.Opposites (2.6s)
✔ [691/843] Built Mathlib.Algebra.Group.Nat.Defs (1.1s)
✔ [698/843] Built Mathlib.Algebra.Group.Semiconj.Defs (1.4s)
✔ [703/843] Built Mathlib.Algebra.Group.InjSurj (4.2s)
✔ [707/843] Built Mathlib.Algebra.BigOperators.Group.List.Defs (1.4s)
✔ [713/843] Built Mathlib.Algebra.GroupWithZero.Nat (1.0s)
✔ [720/855] Built Mathlib.Data.List.Pairwise (3.2s)
✔ [729/860] Built Batteries.Data.List.Count (2.0s)
✔ [730/860] Built Mathlib.Algebra.Group.Commute.Defs (1.9s)
✔ [732/860] Built Mathlib.Control.Applicative (1.5s)
✔ [734/865] Built Mathlib.Control.Traversable.Basic (1.9s)
✔ [735/870] Built Batteries.Data.List.Perm (3.5s)
✔ [790/873] Built Mathlib.Algebra.GroupWithZero.NeZero (1.1s)
✔ [793/877] Built Mathlib.Algebra.Group.Pi.Basic (3.2s)
✔ [794/877] Built Mathlib.Algebra.Group.Hom.Defs (10s)
✔ [800/877] Built Mathlib.Algebra.GroupWithZero.Pi (1.4s)
✔ [804/878] Built Mathlib.Algebra.Group.Units.Defs (6.5s)
✔ [815/885] Built Mathlib.Algebra.GroupWithZero.InjSurj (2.4s)
✔ [816/887] Built Mathlib.Algebra.Group.Nat.Units (1.0s)
✔ [819/887] Built Mathlib.Util.AtomM (1.3s)
✔ [820/888] Built Mathlib.Data.List.TFAE (1.3s)
✔ [821/888] Built Mathlib.Algebra.Group.Action.Defs (4.9s)
✔ [822/903] Built Mathlib.Data.FunLike.IsApply (2.1s)
✔ [833/927] Built Mathlib.Algebra.Group.Action.Faithful (1.6s)
✔ [843/939] Built Mathlib.Data.Bracket (1.0s)
✔ [851/969] Built Mathlib.Algebra.Group.Commute.Hom (1.1s)
✔ [872/977] Built Mathlib.Algebra.Group.Equiv.Defs (5.8s)
✔ [921/978] Built Mathlib.Logic.Function.CompTypeclasses (931ms)
✔ [943/981] Built Mathlib.Tactic.TFAE (4.6s)
✔ [965/989] Built Mathlib.Algebra.Group.Invertible.Defs (1.9s)
✔ [981/1014] Built Mathlib.Algebra.Group.Hom.CompTypeclasses (1.3s)
✔ [989/1014] Built Batteries.Classes.RatCast (590ms)
✔ [991/1044] Built Mathlib.Algebra.GroupWithZero.Regular (1.3s)
✔ [1009/1046] Built Mathlib.Algebra.Regular.Opposite (1.2s)
✔ [1011/1050] Built Mathlib.Data.Rat.Init (1.2s)
✔ [1019/1063] Built Mathlib.Lean.Expr.Rat (781ms)
✔ [1023/1068] Built Mathlib.Tactic.HaveI (1.2s)
✔ [1024/1089] Built Mathlib.Util.Qq (1000ms)
✔ [1039/1090] Built Mathlib.Algebra.Order.Group.Synonym (5.2s)
✔ [1060/1094] Built Mathlib.Tactic.TryThis (916ms)
✔ [1065/1124] Built Mathlib.Util.AtomM.Recurse (1.3s)
✔ [1066/1124] Built Mathlib.Algebra.Notation (1.2s)
✔ [1091/1127] Built Mathlib.Data.Int.Cast.Pi (842ms)
✔ [1093/1130] Built Mathlib.Algebra.Order.GroupWithZero.Synonym (1.3s)
✔ [1123/1137] Built Mathlib.Data.Ineq (745ms)
✔ [1125/1138] Built Mathlib.Tactic.FieldSimp.Attr (795ms)
✔ [1126/1142] Built Mathlib.Util.DischargerAsTactic (899ms)
✔ [1128/1146] Built Mathlib.Util.SynthesizeUsing (1.0s)
✔ [1135/1174] Built Mathlib.Lean.Meta.Tactic.Rewrite (793ms)
✔ [1155/1179] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (1.2s)
✔ [1156/1179] Built Mathlib.Util.ElabWithoutMVars (908ms)
✔ [1158/1240] Built Mathlib.Data.Tree.Basic (1.7s)
✔ [1212/1339] Built Mathlib.Algebra.Order.Group.Action.Synonym (1.5s)
✔ [1257/1363] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm (1.4s)
✔ [1268/1365] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss (1.2s)
✔ [1269/1399] Built Mathlib.Util.DelabNonCanonical (996ms)
✔ [1361/1403] Built Mathlib.Logic.Small.Defs (1.1s)
✔ [1363/1418] Built Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector (991ms)
✔ [1387/1418] Built Mathlib.Control.Monad.Basic (1.0s)
✔ [1404/1421] Built Mathlib.Data.Sigma.Lex (1.4s)
✔ [1407/1421] Built Mathlib.Algebra.Group.Commutator (881ms)
✔ [1411/1538] Built Mathlib.Logic.UnivLE (1.1s)
✔ [1520/1557] Built Mathlib.GroupTheory.GroupAction.IterateAct (1.2s)
✔ [1540/1581] Built Mathlib.Algebra.Group.ULift (2.6s)
✔ [1543/1593] Built Mathlib.Algebra.Torsor.Defs (2.3s)
✔ [1551/1670] Built Mathlib.Algebra.Group.PUnit (1.1s)
✔ [1612/1728] Built Mathlib.Algebra.GroupWithZero.ULift (1.2s)
✔ [1668/1733] Built Mathlib.Algebra.Group.Irreducible.Defs (1.2s)
✔ [1691/1738] Built Mathlib.Data.FunLike.Group (3.6s)
✔ [1697/1740] Built Mathlib.Data.Opposite (1.2s)
✔ [1698/1778] Built Mathlib.Tactic.CategoryTheory.CategoryStar (1.1s)
✔ [1699/1778] Built Mathlib.Logic.Lemmas (1.7s)
✔ [1716/1801] Built Mathlib.Combinatorics.Quiver.Basic (1.4s)
✔ [1718/1801] Built Mathlib.Tactic.ProxyType (3.4s)
✔ [1747/1802] Built Cslib.Foundations.Lint.Basic (707ms)
✔ [1752/1803] Built Batteries.Classes.Cast (680ms)
✔ [1753/1806] Built Mathlib.Control.Lawful (1.2s)
✔ [1754/1808] Built Mathlib.Control.Monad.Writer (1.9s)
✔ [1755/1808] Built Mathlib.Combinatorics.Quiver.Prefunctor (1.8s)
✔ [1757/1808] Built Batteries.Lean.EStateM (1.2s)
✔ [1759/1809] Built Batteries.Control.ForInStep (571ms)
✔ [1760/1809] Built Batteries.Classes.Deprecated (1.7s)
✔ [1761/1809] Built Batteries.Control.Monad (746ms)
✔ [1762/1809] Built Mathlib.Control.Monad.Cont (2.2s)
✔ [1765/1811] Built Mathlib.Combinatorics.Quiver.Push (1.6s)
✔ [1772/1811] Built Batteries.Data.Array.Init.Lemmas (870ms)
✔ [1777/1813] Built BatteriesRecycling.MonadSatisfying.Basic (1.9s)
✔ [1782/1814] Built Batteries.Classes.SatisfiesM (705ms)
✔ [1783/1814] Built Mathlib.Combinatorics.Quiver.Path (3.0s)
✖ [1788/1817] Building Batteries.Data.Array.Lemmas (2.2s)
trace: .> LEAN_PATH=/home/runner/work/PolyFun/PolyFun/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/packages/cslib/.lake/build/lib/lean:/home/runner/work/PolyFun/PolyFun/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.32.0/bin/lean /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean -o /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.olean -i /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Lemmas.ilean -c /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.c --setup /home/runner/work/PolyFun/PolyFun/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.setup.json --json
error: Batteries/Data/Array/Lemmas.lean:50:8: `Array.size_set!` has already been declared
error: Lean exited with code 1
✔ [1790/1818] Built Batteries.Data.Array.Match (1.7s)
✔ [1792/1819] Built Batteries.Data.Array.Pairwise (1.0s)
✔ [1795/1819] Built BatteriesRecycling.MonadSatisfying.Array (2.9s)
✔ [1796/1819] Built Mathlib.Combinatorics.Quiver.Symmetric (2.6s)
✔ [1801/1821] Built Batteries.Data.Bool (622ms)
✔ [1814/1823] Built Batteries.Data.List.Scan (2.9s)
✔ [1816/1824] Built Batteries.Data.Array.Monadic (589ms)
✔ [1818/1830] Built Batteries.Data.BitVec.Basic (404ms)
✔ [1823/1830] Built Batteries.Data.AssocList (3.1s)
✔ [1824/1830] Built Batteries.Data.BinomialHeap.Lemmas (817ms)
✔ [1825/1833] Built Batteries.Data.ByteSlice (724ms)
✔ [1826/1836] Built Batteries.Data.BinomialHeap (654ms)
✔ [1827/1840] Built Batteries.Data.ByteArray (1.2s)
✔ [1829/1843] Built Batteries.Data.FloatArray (541ms)
✔ [1830/1844] Built Batteries.Data.DList.Basic (967ms)
✔ [1831/1845] Built Batteries.Data.BinaryHeap.Basic (2.9s)
✔ [1832/1845] Built Batteries.Data.Char.Basic (1.5s)
✔ [1833/1846] Built Batteries.Lean.HashMap (627ms)
✔ [1834/1846] Built Batteries.Data.DList.Lemmas (802ms)
✔ [1835/1846] Built Batteries.Data.List.Init.Lemmas (429ms)
✔ [1836/1846] Built Batteries.Data.List.ArrayMap (552ms)
✔ [1837/1849] Built Batteries.Data.BinaryHeap (479ms)
✔ [1838/1849] Built Batteries.Data.List.Matcher (734ms)
✔ [1839/1850] Built Batteries.Data.Char.AsciiCasing (1.8s)
✔ [1840/1850] Built Batteries.Data.HashMap.Basic (1.2s)
✔ [1841/1850] Built BatteriesRecycling.MonadSatisfying.List (587ms)
✔ [1842/1854] Built Batteries.Data.DList (1.1s)
✔ [1843/1854] Built Batteries.Data.List.Monadic (409ms)
✔ [1844/1854] Built Batteries.Data.MLList.Heartbeats (652ms)
✔ [1845/1855] Built Batteries.Data.HashMap (703ms)
✔ [1846/1855] Built Batteries.Data.Char (692ms)
✔ [1849/1859] Built Batteries.Lean.System.IO (504ms)
✔ [1850/1860] Built Batteries.Data.List (679ms)
✔ [1851/1860] Built Batteries.Data.NameSet (666ms)
✔ [1852/1860] Built Batteries.Data.MLList.IO (509ms)
✔ [1853/1860] Built Batteries.Data.Nat.Bitwise.Lemmas (932ms)
✔ [1854/1860] Built Batteries.Data.Nat.Gcd (886ms)
✔ [1855/1862] Built Batteries.Data.MLList (753ms)
✔ [1856/1873] Built Batteries.Data.Nat.Bitwise (870ms)
✔ [1857/1875] Built Batteries.Data.Nat.Bisect (3.6s)
✔ [1859/1879] Built Batteries.Data.PairingHeap (2.8s)
✔ [1860/1880] Built Batteries.Data.Range.Lemmas (824ms)
✔ [1861/1880] Built Batteries.Lean.Float (754ms)
✔ [1862/1880] Built Batteries.Data.Random.MersenneTwister (2.4s)
✔ [1863/1881] Built Batteries.Data.RunningStats (537ms)
✔ [1864/1881] Built Batteries.Data.Rat.Float (605ms)
✔ [1865/1882] Built Batteries.Data.Random (481ms)
✔ [1866/1882] Built Batteries.Data.Stream (851ms)
✔ [1867/1883] Built Batteries.Data.Range (788ms)
✔ [1868/1884] Built Batteries.Data.String.AsciiCasing (451ms)
✔ [1869/1890] Built Batteries.Data.Rat (495ms)
✔ [1870/1891] Built Batteries.Data.String.Basic (602ms)
✔ [1871/1892] Built Batteries.Util.Panic (594ms)
✔ [1872/1892] Built BatteriesRecycling.RBTree.Basic (4.7s)
✔ [1873/1892] Built Batteries.Data.String.Matcher (688ms)
✔ [1874/1892] Built Batteries.Data.String.Legacy (1.7s)
✔ [1875/1895] Built Batteries.Data.RBMap.Basic (1.2s)
✔ [1876/1896] Built Batteries.Data.Vector.Basic (4.2s)
✔ [1878/1897] Built BatteriesRecycling.MonadSatisfying.Vector (1.4s)
✔ [1879/1897] Built Batteries.Data.UnionFind.Basic (6.5s)
✔ [1880/1898] Built Batteries.Lean.IO.Process (1.3s)
✔ [1881/1899] Built Batteries.Data.Vector.Monadic (734ms)
✔ [1883/1899] Built Batteries.Lean.Json (882ms)
✔ [1884/1900] Built Batteries.Lean.LawfulMonad (1.0s)
✔ [1885/1900] Built Batteries.Data.UnionFind.Lemmas (1.7s)
✔ [1886/1900] Built BatteriesRecycling.RBTree.WF (9.3s)
✔ [1887/1903] Built Batteries.Lean.LawfulMonadLift (1.2s)
✔ [1888/1903] Built Batteries.Data.UnionFind (784ms)
✔ [1889/1903] Built Batteries.Lean.Meta.Simp (1.2s)
✔ [1890/1903] Built Batteries.Data.RBMap.WF (855ms)
✔ [1891/1903] Built Batteries.Data.RBMap.Alter (850ms)
✔ [1892/1904] Built BatteriesRecycling.MonadSatisfying.Lean (781ms)
✔ [1893/1905] Built BatteriesRecycling.RBTree.Depth (1.4s)
✔ [1894/1905] Built Batteries.Data.String.Lemmas (10s)
✔ [1895/1906] Built Batteries.Lean.Util.EnvSearch (763ms)
✔ [1896/1906] Built Batteries.Lean.SatisfiesM (906ms)
✔ [1897/1907] Built Batteries.Data.RBMap.Depth (625ms)
✔ [1898/1907] Built BatteriesRecycling.RBTree.Alter (3.2s)
✔ [1899/1908] Built Batteries.Tactic.Instances (1.1s)
✔ [1900/1909] Built Batteries.Tactic.Lemma (979ms)
✔ [1901/1909] Built Batteries.Data.String (640ms)
✔ [1902/1910] Built Batteries.Tactic.NoMatch (1.1s)
✔ [1903/1911] Built Batteries.Tactic.PrintDependents (1.3s)
✔ [1904/1913] Built Batteries.Tactic.PrintOpaques (1.1s)
✔ [1905/1918] Built Batteries.Tactic.PrintPrefix (1.8s)
✔ [1906/1918] Built Batteries.Tactic.ShowUnused (1.5s)
✔ [1911/1963] Built Batteries.Util.Pickle (762ms)
✔ [2131/2155] Built Mathlib.Algebra.AddTorsor.Defs (1.1s)
✔ [2169/2183] Built Mathlib.Algebra.Notation.Lemmas (1.6s)
✔ [2171/2193] Built Mathlib.Algebra.Group.Pi.Units (2.0s)
✔ [2234/2301] Built Batteries.Tactic.SqueezeScope (4.9s)
✔ [2264/2301] Built Mathlib.Tactic.Polynomial.Core (1.5s)
✔ [2319/2350] Built Mathlib.Data.Nat.MaxPowDiv (2.1s)
✔ [2345/2484] Built Mathlib.CategoryTheory.ConcreteCategory.Bundled (1.1s)
✔ [2454/2486] Built BatteriesRecycling.RBTree.Lemmas (8.7s)
✔ [2456/2547] Built Mathlib.Tactic.SuppressCompilation (2.7s)
✔ [2592/2646] Built Batteries.Data.RBMap.Lemmas (726ms)
✔ [2593/2650] Built Mathlib.Tactic.CategoryTheory.Coherence.Datatypes (2.0s)
✔ [2595/2728] Built Batteries.Data.RBMap (702ms)
✔ [2597/2728] Built Mathlib.Algebra.Group.Ext (2.3s)
✔ [2622/2728] Built Mathlib.Tactic.BDSimp (1.2s)
✔ [3187/3334] Built Mathlib.Algebra.PEmptyInstances (882ms)
✔ [3242/3414] Built Mathlib.Algebra.Homology.ComplexShape (1.4s)
✔ [3332/3420] Built Mathlib.Tactic.Monotonicity.Basic (1.3s)
✔ [3339/3446] Built Mathlib.Algebra.Expr (912ms)
✔ [3365/3449] Built Mathlib.Algebra.Group.MinimalAxioms (1.2s)
✔ [3370/3450] Built Mathlib.Algebra.Group.Action.Option (1.3s)
✔ [3371/3474] Built Mathlib.Algebra.Group.Action.Sigma (1.3s)
✔ [3396/3487] Built Mathlib.Algebra.Group.Action.Sum (1.4s)
✔ [3409/3489] Built Mathlib.Algebra.GroupWithZero.Action.Faithful (861ms)
✔ [3410/3629] Built Mathlib.Algebra.HierarchyDesign (781ms)
✔ [3521/3664] Built Mathlib.Tactic.CategoryTheory.Coherence.Normalize (6.9s)
✔ [3555/3684] Built Mathlib.Algebra.Homology.HasNoLoop (1.1s)
✔ [4118/4242] Built Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence (7.6s)
✔ [4199/4289] Built Mathlib.Algebra.Homology.SpectralSequence.ComplexShape (1.2s)
✔ [4217/4450] Built Mathlib.Data.Nat.NthRoot.Defs (793ms)
✔ [4362/4575] Built Mathlib.LinearAlgebra.AffineSpace.Defs (1.0s)
✔ [4521/4683] Built Mathlib.Util.Superscript (2.8s)
✔ [4667/4745] Built Mathlib.Algebra.Order.Sum (921ms)
✔ [4668/4745] Built Mathlib.Logic.Function.Coequalizer (802ms)
✔ [4736/5042] Built Mathlib.Data.List.GetD (1.5s)
✔ [4740/5042] Built Mathlib.Algebra.Order.Group.Equiv (1.4s)
✔ [5794/5956] Built Mathlib.Order.SetIsMax (821ms)
✔ [5940/6176] Built Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note (780ms)
✔ [6332/6505] Built Mathlib.Combinatorics.Quiver.Cast (1.1s)
✔ [6521/6562] Built Mathlib.Data.TwoPointing (1.3s)
✔ [6523/6751] Built Mathlib.Combinatorics.Quiver.SingleObj (1.5s)
✔ [6742/6752] Built Mathlib.Data.List.Triplewise (2.6s)
✔ [6842/6854] Built Mathlib.Data.Matrix.DMatrix (1.9s)
✔ [6844/6953] Built Mathlib.GroupTheory.EckmannHilton (1.4s)
✔ [6938/6953] Built Mathlib.Combinatorics.Quiver.Subquiver (1.2s)
✔ [6941/6965] Built Mathlib.Data.Nat.Size (1.2s)
✔ [6950/6967] Built Mathlib.Data.Array.Defs (1.1s)
✔ [6952/6975] Built Mathlib.Data.Num.Basic (2.3s)
✔ [6967/6995] Built Mathlib.Combinatorics.Quiver.ConnectedComponent (1.7s)
✔ [6968/6995] Built Mathlib.Control.Traversable.Lemmas (1.8s)
✔ [6986/7020] Built Mathlib.Data.Bool.AllAny (821ms)
✔ [7010/7024] Built Mathlib.Data.Erased (1.3s)
✔ [7014/7025] Built Mathlib.Data.List.Lookmap (1.3s)
✔ [7016/7029] Built Mathlib.Control.Traversable.Equiv (1.7s)
✔ [7024/7036] Built Mathlib.Data.LawfulXor (1.6s)
✔ [7031/7071] Built Mathlib.Data.List.Fold (1.2s)
✔ [7067/7121] Built Mathlib.Data.List.Indexes (1.2s)
✔ [7116/7127] Built Mathlib.Data.List.SplitOn (468ms)
✔ [7122/7128] Built Mathlib.Data.List.ModifyLast (1.3s)
✔ [7123/7129] Built Mathlib.Data.Ordering.Lemmas (983ms)
✔ [7124/7141] Built Mathlib.Data.String.Lemmas (930ms)
✔ [7136/7384] Built Mathlib.Data.Tree.Get (912ms)
✔ [7381/7466] Built Mathlib.Data.Tree.RBMap (767ms)
✔ [7461/7467] Built Mathlib.Deprecated.Aliases (720ms)
✔ [7462/7468] Built Mathlib.Data.Tree.Traversable (1.1s)
✔ [7463/7468] Built Mathlib.Lean.Elab.Tactic.Basic (764ms)
✔ [7464/7471] Built Mathlib.Lean.CoreM (928ms)
✔ [7465/7473] Built Mathlib.Lean.EnvExtension (735ms)
✔ [7466/7473] Built Mathlib.Lean.Expr (473ms)
✔ [7467/7474] Built Mathlib.Lean.Exception (834ms)
✔ [7468/7475] Built Mathlib.Util.MemoFix (829ms)
✔ [7469/7476] Built Mathlib.Lean.Json (850ms)
✔ [7470/7476] Built Mathlib.Lean.LocalContext (778ms)
✔ [7471/7592] Built Mathlib.Lean.MessageData.ForExprs (1.1s)
✔ [7587/7672] Built Mathlib.Lean.Expr.ReplaceRec (758ms)
✔ [7588/7672] Built Mathlib.Lean.Meta.DiscrTree (1.0s)
✔ [7707/7712] Built Mathlib.Lean.Thunk (1.0s)
✔ [8048/8056] Built Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (407ms)
✔ [8051/8205] Built Mathlib.Logic.Equiv.Pairwise (889ms)
✔ [8052/8205] Built Mathlib.Logic.IsEmpty (816ms)
✔ [8432/8438] Built Mathlib.Order.Synonym (845ms)
✔ [8433/8438] Built Mathlib.Order.Std (1.7s)
✔ [8434/8449] Built Mathlib.Tactic.Change (1.2s)
✔ [8449/8454] Built Mathlib.Tactic.Clean (953ms)
✔ [8450/8457] Built Mathlib.Tactic.Cases (2.2s)
✔ [8451/8459] Built Mathlib.Tactic.Eval (883ms)
✔ [8452/8460] Built Mathlib.Tactic.Explode.Datatypes (1.1s)
✔ [8453/8460] Built Mathlib.Tactic.Ext (1.1s)
✔ [8454/8461] Built Mathlib.Tactic.DuplicateDecls (2.6s)
✔ [8455/8462] Built Mathlib.Tactic.Explode.Pretty (1.2s)
✔ [8456/8462] Built Mathlib.Tactic.FindSyntax (1.8s)
✔ [8457/8462] Built Mathlib.Tactic.Generalize (1.2s)
✔ [8458/8467] Built Mathlib.Tactic.DeriveTraversable (4.6s)
✔ [8462/8468] Built Mathlib.Tactic.Have (1.5s)
✔ [8463/8469] Built Mathlib.Tactic.Explode (1.7s)
✔ [8464/8469] Built Mathlib.Tactic.Linter.CommandStart (704ms)
✔ [8465/8471] Built Mathlib.Tactic.Linter.CommandRanges (1.2s)
✔ [8466/8488] Built Mathlib.Tactic.Linter.DeprecatedModule (783ms)
✔ [8481/8489] Built Mathlib.Tactic.Polyrith (1.1s)
✔ [8482/8489] Built Mathlib.Tactic.Linter.FindDeprecations (2.4s)
✔ [8483/8492] Built Mathlib.Tactic.ITauto (4.5s)
✔ [8484/8493] Built Mathlib.Tactic.Linter.TextBased.UnicodeLinter (3.1s)
✔ [8485/8493] Built Mathlib.Tactic.ProdAssoc (1.6s)
✔ [8486/8493] Built Mathlib.Tactic.ReduceModChar.Ext (796ms)
✔ [8488/8494] Built Mathlib.Tactic.Relation.Symm (879ms)
✔ [8489/8495] Built Mathlib.Tactic.Recall (1.8s)
✔ [8490/8501] Built Mathlib.Tactic.Replace (1.1s)
✔ [8491/8501] Built Mathlib.Tactic.RewriteSearch (1.0s)
✔ [8496/8501] Built Mathlib.Tactic.Linter.ValidatePRTitle (2.2s)
✔ [8497/8504] Built Mathlib.Tactic.StacksAttribute (974ms)
✔ [8498/8504] Built Mathlib.Tactic.TypeCheck (736ms)
✔ [8499/8505] Built ProofWidgets.Component.PenroseDiagram (1.5s)
✔ [8500/8509] Built Mathlib.Tactic.Linter.TextBased (4.2s)
✔ [8501/8510] Built ProofWidgets.Presentation.Expr (1.8s)
✔ [8503/8546] Built Mathlib.Tactic.Sat.FromLRAT (3.3s)
✔ [8538/8673] Built Mathlib.Tactic.Widget.GCongr (1.1s)
✔ [8539/8673] Built ProofWidgets.Component.HtmlDisplay (1.0s)
✔ [8663/8674] Built Mathlib.Tactic.WithoutCDot (1.1s)
✔ [8665/8675] Built Mathlib.Util.AliasIn (1.1s)
✔ [8668/8676] Built Mathlib.Util.AssertNoSorry (854ms)
✔ [8672/8809] Built Mathlib.Util.FormatTable (1.1s)
✔ [8673/8809] Built Mathlib.Util.GetAllModules (935ms)
✔ [8690/8809] Built Mathlib.Util.LongNames (1.1s)
✔ [8691/8809] Built Mathlib.Util.Simp (750ms)
✔ [8692/8809] Built Mathlib.Util.Export (2.5s)
✔ [8693/8809] Built Mathlib.Util.SleepHeartbeats (862ms)
✔ [8702/8809] Built PolyFun.Control.Monad.Indexed (888ms)
✔ [8703/8809] Built PolyFun.Logic.HEq (442ms)
✔ [8704/8809] Built PolyFun.Control.Monad.Iter (757ms)
✔ [8709/8809] Built PolyFun.Control.Trace (1.1s)
⚠ [8737/8809] Built PolyFun.Interaction.Basic.BundledMonad (795ms)
warning: PolyFun/Interaction/Basic/BundledMonad.lean:19:0: `BundledMonad`: universes `u`, `v` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.
Note: This linter can be disabled with `set_option linter.checkUnivs false`
✔ [8777/8809] Built PolyFun.Interaction.TwoParty.Role (568ms)
✔ [8803/8809] Built PolyFun.Interaction.UC.Leakage (284ms)
✔ [8804/8809] Built PolyFun.Interaction.UC.EnvAction (839ms)
Some required targets logged failures:
- Batteries.Data.Nat.Basic
- Aesop.Builder.Forward
- Plausible.Testable
- Batteries.Data.Array.Lemmas
error: build failed
Try
lake updateand then investigate why this update causes the lean build to fail.Files changed in update:
Build Output