search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
532 stars 77 forks source link

trace repository error #119

Closed yangky11 closed 7 months ago

yangky11 commented 7 months ago

Discussed in https://github.com/lean-dojo/LeanDojo/discussions/116

Originally posted by **Moyvbai** December 29, 2023 I used LeanDojo to trace lean4 project(repo = LeanGitRepo( "https://github.com/Moyvbai/lean4-example", "9ed7ebe5ecd3903dc59a49995da6514f39f50bfc", )), but the following error occurred ``` { "name": "FileNotFoundError", "message": "/home2/shuming/Lean/Tmp/tmpbq4ytl3q/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json does not exist", "stack": "--------------------------------------------------------------------------- FileNotFoundError Traceback (most recent call last) Cell In[5], line 2 1 # A few minutes if the traced repo is in the cache; many hours otherwise. ----> 2 traced_repo = trace(repo) File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:181, in trace(repo, dst_dir) 176 dst_dir = Path(dst_dir) 177 assert ( 178 not dst_dir.exists() 179 ), f\"The destination directory {dst_dir} already exists.\" --> 181 cached_path = get_traced_repo_path(repo) 182 logger.info(f\"Loading the traced repo from {cached_path}\") 183 traced_repo = TracedRepo.load_from_disk(cached_path) File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:154, in get_traced_repo_path(repo) 152 logger.debug(f\"Working in the temporary directory {tmp_dir}\") 153 _trace(repo) --> 154 traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name) 155 traced_repo.save_to_disk() 156 path = cache.store(tmp_dir) File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:1409, in TracedRepo.from_traced_files(cls, root_dir) 1399 traced_files = list( 1400 tqdm( 1401 pool.map_unordered( (...) 1405 ) 1406 ) 1408 dependencies = repo.get_dependencies(root_dir) -> 1409 traced_files_graph = _build_dependency_graph(traced_files, root_dir, repo) 1410 traced_repo = cls(repo, dependencies, root_dir, traced_files_graph) 1411 traced_repo._update_traced_files() File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:1240, in _build_dependency_graph(seed_files, root_dir, repo) 1238 if not G.has_node(dep_path_str): 1239 json_path = to_json_path(root_dir, dep_path, repo) -> 1240 tf_dep = TracedFile.from_traced_file(root_dir, json_path, repo) 1241 G.add_node(dep_path_str, traced_file=tf_dep) 1242 traced_files.append(tf_dep) File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:638, in TracedFile.from_traced_file(cls, root_dir, json_path, repo) 636 json_path = root_dir / json_path 637 if not json_path.exists(): --> 638 raise FileNotFoundError(f\"{json_path} does not exist\") 639 assert json_path.suffixes == [ 640 \".ast\", 641 \".json\", 642 ], f\"{json_path} is not a *.ast.json file\" 644 if repo.uses_lean3: FileNotFoundError: /home2/shuming/Lean/Tmp/tmpbq4ytl3q/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json does not exist" } ``` However, when I remove the sum_choose_eq_Ico theorem in Lean4Example.lean, it works.
yangky11 commented 7 months ago

@Moyvbai

I cannot reproduce the problem. What is the output in debug mode (VERBOSE=1)? Here is mine:

epo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-02 06:35:10.274 | DEBUG    | lean_dojo.container:run:183 - NUM_PROCS=32 python3 build_lean4_repo.py lean4-example
2024-01-02 06:35:10.541 | INFO     | __main__:main:146 - Building lean4-example
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to './.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
[0/2] Downloading proofwidgets cloud release
[0/16] Building Std.Lean.TagAttribute
[0/16] Building Std.Lean.Command
[0/22] Building Std.Tactic.Unreachable
[0/26] Building Std.Tactic.OpenPrivate
[0/28] Building Std.Tactic.ByCases
[0/30] Building Std.Util.TermUnsafe
[0/30] Building Std.Lean.Name
[0/30] Building Std.Tactic.SeqFocus
[0/31] Building Std.Lean.Position
[0/32] Building Std.Lean.Float
[0/36] Building Std.Lean.Parser
[0/36] Building Std.Lean.LocalContext
[0/49] Building Std.Lean.NameMapAttribute
[0/49] Building Std.Data.Array.Init.Basic
[0/49] Building Std.Classes.Dvd
[0/49] Building Std.Util.ProofWanted
[0/49] Building Std.Lean.Tactic
[0/54] Building Std.Data.Ord
[0/55] Building Std.Lean.InfoTree
[0/61] Building Std.Util.ExtendedBinder
[0/63] Building Std.Data.Option.Init.Lemmas
[0/65] Building Std.Data.Fin.Init.Lemmas
[0/65] Building Std.Tactic.HaveI
[0/77] Building Std.Lean.Expr
[0/77] Building Std.Lean.Meta.Expr
[0/83] Building Std.Lean.PersistentHashMap
[0/86] Building Std.Lean.Delaborator
[0/87] Building Std.Tactic.RCases
[0/90] Building Std.Util.LibraryNote
[1/105] Building Std.Control.ForInStep.Basic
[1/115] Building Std.Classes.BEq
[1/196] Building Std.Tactic.LabelAttr
[2/345] Building Aesop.Check
[2/357] Building Qq.Typ
[2/357] Building Std.Tactic.Omega.Config
[2/357] Building Std.Lean.CoreM
[2/357] Building Std.Tactic.Instances
[2/357] Building Std.Lean.Elab.Tactic
[2/357] Building Std.Tactic.Replace
[2/357] Building Std.Lean.Meta.Inaccessible
[2/357] Building Std.Lean.PersistentHashSet
[2/358] Building Std.Data.Prod.Lex
[2/358] Building Aesop.Percent
[2/358] Building Std.Data.MLList.Basic
[2/358] Building Aesop.Nanos
[2/358] Building Std.Tactic.LeftRight
[2/358] Building Std.Lean.MonadBacktrack
[2/358] Building Std.Tactic.Where
[2/358] Building Std.Lean.HashMap
[2/358] Building Std.Tactic.Exact
[2/358] Building Std.Lean.Util.Path
[2/358] Building Std.Tactic.Case
[2/358] Building Qq.ForLean.ToExpr
[2/358] Building Qq.ForLean.ReduceEval
[2/358] Building Aesop.Options.Public
[2/358] Building Std.WF
[2/358] Building Std.Data.DList
[2/358] Building Std.Tactic.Change
[5/375] Building Aesop.Frontend.Basic
[5/381] Building Aesop.Frontend.ElabM
[7/395] Unpacking proofwidgets cloud release
[32/409] Building Std.Data.Int.Basic
[33/409] Building Std.Lean.Json
[33/409] Building Std.Linter.UnreachableTactic
[33/409] Building Std.Control.ForInStep.Lemmas
[33/409] Building Std.Tactic.Relation.Rfl
[33/409] Building Std.Tactic.PrintDependents
[33/409] Building Std.Tactic.CoeExt
[33/416] Building Std.Util.Pickle
[33/416] Building Std.Data.Nat.Basic
[33/416] Building Aesop.Constants
[33/416] Building Std.Lean.AttributeExtra
[33/418] Building Std.Tactic.RunCmd
[33/418] Building Std.Lean.Meta.Basic
[33/418] Building Std.Tactic.GuardExpr
[33/418] Building Std.CodeAction.Attr
[34/419] Building Std.Tactic.Lint.Basic
[46/426] Building Mathlib.Util.AssertExists
[46/426] Building Mathlib.Tactic.PPWithUniv
[46/426] Building Mathlib.Util.Syntax
[46/426] Building Mathlib.Tactic.Spread
[46/426] Building Mathlib.Tactic.Substs
[46/426] Building Mathlib.Tactic.Monotonicity.Attr
[46/426] Building Mathlib.Tactic.Classical
[46/426] Building Mathlib.Lean.PrettyPrinter.Delaborator
[46/426] Building Mathlib.Init.Data.Nat.Notation
[46/426] Building Std.Test.Internal.DummyLabelAttr
[46/426] Building Mathlib.Tactic.ExtendDoc
[46/426] Building Mathlib.Mathport.Attributes
[46/426] Building Mathlib.Tactic.Attr.Register
[46/426] Building Mathlib.Tactic.SimpRw
[46/426] Building Mathlib.Lean.EnvExtension
[46/501] Building Mathlib.Tactic.Coe
[46/511] Building Qq.SortLocalDecls
[46/511] Building Mathlib.Util.WithWeakNamespace
[46/511] Building Mathlib.Tactic.RunCmd
[46/511] Building Mathlib.Tactic.ProjectionNotation
[46/511] Building Mathlib.Data.Array.Defs
[46/511] Building Mathlib.Lean.Elab.Term
[46/511] Building Qq.ForLean.Do
[46/511] Building Std.Data.Json
[46/511] Building Mathlib.Tactic.CasesM
[46/511] Building Mathlib.Mathport.Rename
[46/511] Building Mathlib.Util.MemoFix
[48/521] Building Mathlib.Lean.Meta.Basic
[48/524] Building Mathlib.Tactic.Clear!
[48/524] Building Mathlib.Tactic.ApplyWith
[48/524] Building Mathlib.Tactic.Clear_
[48/524] Building Mathlib.Tactic.Constructor
[48/524] Building Mathlib.Tactic.ClearExcept
[50/534] Building Mathlib.Tactic.ExtractGoal
[50/537] Building Mathlib.Tactic.InferParam
[51/538] Building Mathlib.Tactic.FailIfNoProgress
[51/538] Building Mathlib.Tactic.GuardHypNums
[51/538] Building Mathlib.Tactic.GuardGoalNums
[51/538] Building Mathlib.Lean.SMap
[60/567] Building Std.Control.ForInStep
[61/567] Building Mathlib.Tactic.Rename
[61/567] Building Mathlib.Tactic.Set
[61/567] Building Mathlib.Tactic.Trace
[61/567] Building Mathlib.Tactic.NthRewrite
[61/567] Building Mathlib.Tactic.SuccessIfFailWithMsg
[61/568] Building Std.Linter.UnnecessarySeqFocus
[61/568] Building Mathlib.Tactic.TypeCheck
[61/568] Building Mathlib.Tactic.UnsetOption
[62/569] Building ProofWidgets.Compat
[63/570] Building Mathlib.Tactic.SudoSetOption
[63/570] Building Mathlib.Tactic.SimpIntro
[64/571] Building Aesop.Options.Internal
[65/582] Building Mathlib.Util.WhatsNew
[65/583] Building Mathlib.Tactic.Widget.SelectInsertParamsClass
[66/594] Building Std.Lean.Format
[73/602] Building Std.Tactic.NoMatch
[82/617] Building Mathlib.Tactic.HaveI
[89/617] Building Mathlib.Tactic.HigherOrder
[102/627] Building Qq.Macro
[102/633] Building Mathlib.Tactic.ScopedNS
[102/639] Building Std.Tactic.Lint.TypeClass
[102/639] Building Std.Tactic.Lint.Frontend
[102/639] Building Mathlib.Tactic.ApplyAt
[102/639] Building Std.Classes.SetNotation
[102/639] Building Std.Tactic.NormCast.Ext
[102/639] Building Std.CodeAction.Basic
[102/639] Building Mathlib.Tactic.Have
[102/639] Building Std.Tactic.Lint.Misc
[102/640] Building Std.Classes.Cast
[102/640] Building Std.Tactic.Lint.Simp
[102/640] Building Mathlib.Util.CompileInductive
[102/644] Building Mathlib.Tactic.Conv
[113/664] Building Aesop.Options
[115/671] Building Mathlib.Util.AtomM
[115/671] Building ProofWidgets.Component.Basic
[115/672] Building Std.Data.MLList.Heartbeats
[115/672] Building Mathlib.Data.MLList.Basic
[115/673] Building Mathlib.Util.SynthesizeUsing
[115/687] Building Mathlib.Lean.Exception
[123/705] Building Mathlib.Init.Data.Fin.Basic
[123/722] Building Std.Tactic.TryThis
[126/793] Building Mathlib.Init.Quot
[126/801] Building Mathlib.Init.Data.Ordering.Basic
[126/808] Building Mathlib.Tactic.ToLevel
[126/810] Building Mathlib.Control.ULift
[131/903] Building Std.Tactic.FalseOrByContra
[131/903] Building Std.Lean.Meta.InstantiateMVars
[131/903] Building Std.Lean.Meta.SavedState
[131/903] Building Std.Tactic.Relation.Symm
[131/903] Building Std.Lean.Meta.AssertHypotheses
[131/903] Building Std.Lean.Meta.Clear
[137/903] Building Std.Linter
[140/903] Building ProofWidgets.Component.MakeEditLink
[140/903] Building ProofWidgets.Data.Html
[144/903] Building Mathlib.Tactic.Replace
[150/903] Building Mathlib.Tactic.DeriveToExpr
[151/903] Building Aesop.Util.EqualUpToIds
[155/903] Building Std.Tactic.NormCast.Lemmas
[161/903] Building Mathlib.Tactic.ApplyCongr
[164/903] Building Std.CodeAction.Deprecated
[164/903] Building Std.CodeAction.Misc
[164/903] Building Std.Tactic.GuardMsgs
[165/903] Building Std.Lean.HashSet
[165/903] Building Mathlib.Util.Delaborators
[165/903] Building Mathlib.Init.Set
[166/903] Building Mathlib.Tactic.Variable
[166/903] Building Mathlib.Tactic.TryThis
[166/903] Building Mathlib.Util.CountHeartbeats
[166/903] Building Std.Tactic.ShowTerm
[166/903] Building Std.Tactic.SimpTrace
[166/903] Building Std.Tactic.Simpa
[167/903] Building Std.Lean.Util.EnvSearch
[168/903] Building Std.Tactic.Lint
[171/903] Building Mathlib.Tactic.Lint
[171/903] Building Mathlib.Tactic.Simps.NotationClass
[171/903] Building Mathlib.Data.Nondet.Basic
[172/903] Building Std.Tactic.PrintPrefix
[177/903] Building Std.Tactic.Alias
[184/903] Building ProofWidgets.Component.OfRpcMethod
[185/903] Building Mathlib.Tactic.Hint
[187/903] Building Std.CodeAction
[190/903] Building Mathlib.Tactic.ToExpr
[191/903] Building Std.Data.Char
[191/903] Building Mathlib.Tactic.Recover
[192/903] Building Std.Data.Bool
[193/903] Building Std.Tactic.SqueezeScope
[193/903] Building Std.Tactic.Basic
[197/903] Building Std.Classes.Order
[198/903] Building Mathlib.Tactic.FBinop
[200/903] Building Mathlib.Init.Data.Bool.Basic
[205/903] Building Mathlib.Tactic.GCongr.ForwardAttr
[205/903] Building Std.Logic
[207/903] Building Mathlib.Data.SProd
[209/903] Building Std.Data.Nat.Init.Lemmas
[209/903] Building Std.Tactic.Omega.Logic
[209/903] Building Std.Classes.LawfulMonad
[209/903] Building Std.Data.Fin.Iterate
[209/903] Building Mathlib.Tactic.Attr.Core
[209/903] Building Std.Data.PairingHeap
[209/903] Building Std.Data.Sum.Basic
[209/903] Building Mathlib.Tactic.Use
[209/903] Building Std.Data.RBMap.Basic
[209/903] Building Std.Data.List.Init.Lemmas
[212/903] Building Std.Data.Fin.Basic
[212/903] Building Mathlib.Tactic.Widget.SelectPanelUtils
[212/903] Building Std.Data.Nat.Lemmas
[215/903] Building Qq.Delab
[218/903] Building Std.Data.Option.Basic
[222/903] Building Std.Data.List.Init.Attach
[222/903] Building Mathlib.Init.Control.Combinators
[222/903] Building Std.Data.Array.Init.Lemmas
[223/903] Building Qq.MetaM
[224/903] Building Std.Data.Array.Basic
[227/903] Building Qq.AssertInstancesCommute
[227/903] Building Qq.Match
[228/903] Building Mathlib.Lean.Data.NameMap
[228/903] Building Std.Data.RBMap.WF
[231/903] Building Std.Data.Array.Merge
[231/903] Building Std.Data.Nat.Gcd
[231/903] Building Std.Data.Nat.Bitwise
[231/903] Building Std.Data.BinomialHeap.Basic
[231/903] Building Std.Data.Int.Lemmas
[232/903] Building Std.Data.List.Basic
[234/903] Building Std.Data.BitVec.Basic
[235/903] Building Aesop.Util.UnorderedArraySet
[235/903] Building Std.Lean.Meta.DiscrTree
[237/903] Building Std.Data.BitVec
[237/903] Building Std.Data.BitVec.Lemmas
[238/903] Building Std.Lean.Meta.Simp
[238/903] Building Std.Tactic.Ext.Attr
[238/903] Building Std.Util.Cache
[240/903] Building Std.Data.BitVec.Folds
[241/903] Building Mathlib.Tactic.Find
[242/903] Building Mathlib.Lean.Meta.Simp
[242/903] Building Std.Tactic.NormCast
[243/903] Building Std.Data.BitVec.Bitblast
[244/903] Building Qq
[245/903] Building Std.Tactic.Ext
[245/903] Building Std.Data.Option.Lemmas
[246/903] Building Std.Tactic.Omega.Int
[247/903] Building Std.Data.Int.DivMod
[247/903] Building Mathlib.Util.Qq
[254/903] Building Std.Control.Lemmas
[254/903] Building Std.Tactic.Congr
[254/903] Building Std.Data.Sum.Lemmas
[254/903] Building Std.Data.Fin.Lemmas
[257/903] Building Std.Data.BinomialHeap.Lemmas
[258/903] Building Std.Data.Sum
[260/903] Building Std.Data.BinomialHeap
[263/903] Building Std.Tactic.PermuteGoals
[263/903] Building Std.Data.AssocList
[263/903] Building Mathlib.Data.String.Defs
[263/903] Building Mathlib.Init.Data.List.Basic
[263/903] Building Mathlib.Lean.Expr.Basic
[264/903] Building Std.Data.List.Lemmas
[265/903] Building Std.Data.Rat.Basic
[266/903] Building Mathlib.Tactic.Widget.Calc
[266/903] Building Mathlib.Tactic.Widget.Conv
[269/903] Building Mathlib.Data.Rat.Init
[269/903] Building Std.Classes.RatCast
[269/903] Building Std.Data.Rat.Lemmas
[270/903] Building Std.Data.RBMap
[270/903] Building Std.Data.RBMap.Alter
[273/903] Building Std.Data.HashMap.Basic
[276/903] Building Mathlib.Tactic.Cases
[276/903] Building Mathlib.Lean.Expr.Traverse
[276/903] Building Mathlib.Tactic.HelpCmd
[276/903] Building Mathlib.Tactic.GeneralizeProofs
[276/903] Building Mathlib.Util.Tactic
[276/903] Building Mathlib.Util.Imports
[278/903] Building Mathlib.Tactic.SwapVar
[278/903] Building Mathlib.Tactic.RenameBVar
[279/903] Building Mathlib.Lean.Expr.ReplaceRec
[279/903] Building Mathlib.Lean.Meta.DiscrTree
[280/903] Building Mathlib.Lean.Expr
[285/903] Building Mathlib.Data.MLList.Dedup
[285/903] Building Std.Data.HashMap.Lemmas
[285/903] Building Mathlib.Lean.Name
[285/903] Building Aesop.Util.UnionFind
[286/903] Building Mathlib.Tactic.Eqns
[286/903] Building Mathlib.Tactic.Core
[286/903] Building Mathlib.Mathport.Notation
[289/903] Building Std.Data.Rat
[292/903] Building Aesop.Util.Basic
[296/903] Building Mathlib.Tactic.WLOG
[296/903] Building Mathlib.Tactic.SplitIfs
[297/903] Building Aesop.Tracing
[297/903] Building Aesop.Index.Basic
[297/903] Building Aesop.Rule.Name
[297/903] Building Aesop.Util.Tactic
[302/903] Building Aesop.Index
[303/903] Building Aesop.Script
[307/903] Building Aesop.RuleTac.Basic
[308/903] Building Aesop.RuleTac.Apply
[308/903] Building Aesop.RuleTac.Preprocess
[308/903] Building Aesop.Rule.Basic
[308/903] Building Aesop.RuleTac.Cases
[308/903] Building Aesop.RuleTac.Tactic
[310/903] Building Aesop.Search.Expansion.Basic
[310/903] Building Aesop.Rule
[315/903] Building Aesop.Builder.Basic
[315/903] Building Aesop.Tree.UnsafeQueue
[316/903] Building Aesop.Tree.Data
[317/903] Building Aesop.Builder.Tactic
[317/903] Building Aesop.Builder.NormSimp
[317/903] Building Aesop.Builder.Apply
[317/903] Building Aesop.Builder.Unfold
[317/903] Building Aesop.Builder.Cases
[317/903] Building Aesop.Builder.Forward
[319/903] Building Aesop.Builder.Constructors
[324/903] Building Aesop.Builder.Default
[326/903] Building Aesop.Builder
[327/903] Building Aesop.Tree.Traversal
[327/903] Building Aesop.Tree.RunMetaM
[327/903] Building Aesop.Profiling
[328/903] Building Aesop.RuleSet
[329/903] Building Std.Data.List.Count
[329/903] Building Std.Lean.System.IO
[329/903] Building Std.Data.Range.Lemmas
[329/903] Building Std.Tactic.Omega.MinNatAbs
[329/903] Building Std.Data.RBMap.Lemmas
[329/903] Building Std.Tactic.Omega.IntList
[329/903] Building Std.Data.Array.Lemmas
[330/903] Building Aesop.Tree.TreeM
[330/903] Building Aesop.Tree.Tracing
[331/903] Building Aesop.Tree.State
[332/903] Building Std.Data.MLList.IO
[336/903] Building Aesop.Tree.ExtractScript
[336/903] Building Aesop.Tree.Free
[336/903] Building Aesop.Tree.AddRapp
[337/903] Building Mathlib.Lean.Meta
[337/903] Building Std.Data.List.Pairwise
[339/903] Building Aesop.Tree.Check
[341/903] Building Aesop.Tree.ExtractProof
[343/903] Building Mathlib.Tactic.Backtrack
[343/903] Building Mathlib.Lean.Elab.Tactic.Basic
[343/903] Building Mathlib.Lean.Meta.CongrTheorems
[343/903] Building Mathlib.Tactic.Relation.Rfl
[343/903] Building Mathlib.Tactic.Relation.Symm
[344/903] Building Std.Data.List.Perm
[345/903] Building Std.Tactic.Omega.Coeffs.IntList
[350/903] Building Aesop.Frontend.Extension.Init
[350/903] Building Aesop.Search.Expansion.Simp
[350/903] Building Aesop.Frontend.RuleExpr
[352/903] Building Std.Tactic.Omega.LinearCombo
[352/903] Building Mathlib.Tactic.Relation.Trans
[353/903] Building Aesop.Tree
[354/903] Building Mathlib.Tactic.SolveByElim
[355/903] Building Aesop.Frontend.Extension
[356/903] Building Aesop.Search.Queue.Class
[357/903] Building Aesop.Search.Queue
[358/903] Building Mathlib.Tactic.Congr!
[359/903] Building Std.Tactic.Omega.OmegaM
[360/903] Building Aesop.Search.SearchM
[363/903] Building Aesop.Search.RuleSelection
[364/903] Building Mathlib.Tactic.Propose
[364/903] Building Mathlib.Tactic.LibrarySearch
[365/903] Building Std.Tactic.Omega.Constraint
[368/903] Building Std.Data.Array.Match
[368/903] Building Std.Data.HashMap.WF
[370/903] Building Mathlib.Init.Core
[371/903] Building Std.Data.String.Basic
[374/903] Building Aesop.Frontend.Attribute
[375/903] Building Mathlib.Tactic.Observe
[377/903] Building Std.Lean.Meta.UnusedNames
[377/903] Building Std.Data.String.Lemmas
[377/903] Building Mathlib.Tactic.Says
[377/903] Building Mathlib.Tactic.Simps.Basic
[378/903] Building Mathlib.Tactic.Convert
[379/903] Building Aesop.BuiltinRules.ApplyHyps
[379/903] Building Aesop.BuiltinRules.Subst
[379/903] Building Aesop.Frontend.Tactic
[379/903] Building Aesop.BuiltinRules.Ext
[379/903] Building Aesop.BuiltinRules.Split
[379/903] Building Aesop.BuiltinRules.Assumption
[379/903] Building Aesop.Frontend.Command
[379/903] Building Aesop.BuiltinRules.Intros
[379/903] Building Aesop.BuiltinRules.DestructProducts
[380/903] Building Aesop.RuleTac.Forward
[392/903] Building Aesop.Frontend
[393/903] Building Aesop.RuleTac
[394/903] Building Aesop.BuiltinRules
[395/903] Building Aesop.Search.Expansion.Norm
[397/903] Building Std.Data.HashMap
[398/903] Building Std.Tactic.Omega.Core
[399/903] Building Aesop.Search.Expansion
[400/903] Building Std.Tactic.Omega.Frontend
[401/903] Building Mathlib.Tactic.ToAdditive
[402/903] Building Aesop.Search.ExpandSafePrefix
[403/903] Building Std.Data.String
[405/903] Building Aesop.Search.Main
[406/903] Building Mathlib.Init.ZeroOne
[407/903] Building Std.Tactic.Omega
[408/903] Building Std
[409/903] Building Mathlib.Init.Data.Nat.Basic
[409/903] Building Mathlib.Init.Data.Int.Basic
[410/903] Building Mathlib.Tactic.Basic
[413/903] Building Mathlib.Tactic.Existsi
[413/903] Building Mathlib.Tactic.ExtractLets
[413/903] Building Mathlib.Tactic.MkIffOfInductiveProp
[413/903] Building Mathlib.Tactic.Inhabit
[413/903] Building Mathlib.Tactic.RSuffices
[413/903] Building Mathlib.Algebra.Abs
[413/903] Building Mathlib.Tactic.DefEqTransformations
[413/903] Building Mathlib.Init.Logic
[421/903] Building Mathlib.Init.Data.Sigma.Basic
[421/903] Building Mathlib.Init.CCLemmas
[421/903] Building Mathlib.Init.Data.Quot
[421/903] Building Mathlib.Init.Propext
[421/903] Building Mathlib.Init.Data.Bool.Lemmas
[421/903] Building Mathlib.Init.Algebra.Classes
[421/903] Building Mathlib.Init.Function
[421/903] Building Mathlib.Init.Align
[422/903] Building Aesop.Main
[427/903] Building Mathlib.Data.HashMap
[429/903] Building Mathlib.Logic.Nontrivial.Defs
[429/903] Building Mathlib.Control.Basic
[430/903] Building Aesop
[431/903] Building Mathlib.Data.Option.Defs
[431/903] Building Mathlib.Init.Order.Defs
[431/903] Building Mathlib.Logic.Basic
[433/903] Building Mathlib.Tactic.SetLike
[437/903] Building Mathlib.Tactic.Rewrites
[437/903] Building Mathlib.Control.Functor
[438/903] Building Mathlib.Init.Data.Int.Order
[438/903] Building Mathlib.Init.Order.LinearOrder
[438/903] Building Mathlib.Tactic.GCongr.Core
[440/903] Building Mathlib.Init.Data.Nat.Lemmas
[441/903] Building Mathlib.Logic.Relator
[441/903] Building Mathlib.Data.Prod.PProd
[441/903] Building Mathlib.Algebra.NeZero
[441/903] Building Mathlib.Logic.Nonempty
[441/903] Building Mathlib.Tactic.PushNeg
[441/903] Building Mathlib.Tactic.Tauto
[441/903] Building Mathlib.Data.List.Defs
[441/903] Building Mathlib.Tactic.TermCongr
[442/903] Building Mathlib.Tactic.Lift
[445/903] Building Mathlib.Logic.Function.Basic
[447/903] Building Mathlib.Init.Data.List.Lemmas
[447/903] Building Mathlib.Data.Bool.Basic
[449/903] Building Mathlib.Control.Traversable.Basic
[451/903] Building Mathlib.Init.Data.List.Instances
[455/903] Building Mathlib.Init.Data.Nat.Bitwise
[457/903] Building Mathlib.Tactic.Contrapose
[457/903] Building Mathlib.Tactic.ByContra
[458/903] Building Mathlib.Data.Subtype
[458/903] Building Mathlib.Tactic.Choose
[458/903] Building Mathlib.Logic.IsEmpty
[458/903] Building Mathlib.Data.Sum.Basic
[458/903] Building Mathlib.Logic.Relation
[458/903] Building Mathlib.Data.Sigma.Basic
[458/903] Building Mathlib.Data.Prod.Basic
[458/903] Building Mathlib.Data.FunLike.Basic
[458/903] Building Mathlib.Algebra.Group.Defs
[458/903] Building Mathlib.Logic.Function.Conjugate
[461/903] Building Mathlib.Logic.Unique
[461/903] Building Mathlib.Data.Option.Basic
[462/903] Building Mathlib.Init.Data.Int.Bitwise
[462/903] Building Mathlib.Data.Num.Basic
[464/903] Building Mathlib.Data.FunLike.Embedding
[464/903] Building Mathlib.Logic.Function.Iterate
[465/903] Building Mathlib.Tactic.Congrm
[466/903] Building Mathlib.Tactic.IrreducibleDef
[468/903] Building Mathlib.Data.FunLike.Equiv
[472/903] Building Mathlib.Order.Basic
[473/903] Building Mathlib.Logic.Nontrivial.Basic
[473/903] Building Mathlib.Data.Quot
[474/903] Building Mathlib.Tactic.Widget.Congrm
[479/903] Building Mathlib.Tactic.Nontriviality.Core
[480/903] Building Mathlib.Data.Option.NAry
[481/903] Building Mathlib.Init.Classical
[482/903] Building Mathlib.Tactic.Common
[484/903] Building Mathlib.Logic.Pairwise
[485/903] Building Mathlib.Tactic.Nontriviality
[486/903] Building Mathlib.Logic.Equiv.Defs
[490/903] Building Mathlib.Algebra.Invertible.Defs
[490/903] Building Mathlib.Algebra.Group.Semiconj.Defs
[490/903] Building Mathlib.Data.List.BigOperators.Defs
[490/903] Building Mathlib.Data.Nat.Cast.Defs
[490/903] Building Mathlib.Algebra.GroupWithZero.Defs
[490/903] Building Mathlib.Control.Applicative
[490/903] Building Mathlib.Data.Pi.Algebra
[490/903] Building Mathlib.Algebra.Group.Basic
[492/903] Building Mathlib.Algebra.Group.Commute.Defs
[493/903] Building Mathlib.Algebra.GroupWithZero.NeZero
[493/903] Building Mathlib.Algebra.Group.Hom.Defs
[494/903] Building Mathlib.Data.Int.Cast.Defs
[494/903] Building Mathlib.Data.Nat.Cast.NeZero
[498/903] Building Mathlib.Algebra.Invertible.GroupWithZero
[500/903] Building Mathlib.Algebra.CharZero.Defs
[500/903] Building Mathlib.Algebra.Ring.Defs
[502/903] Building Mathlib.Order.ULift
[502/903] Building Mathlib.Data.Tree
[502/903] Building Mathlib.Algebra.Order.ZeroLEOne
[502/903] Building Mathlib.Data.PNat.Defs
[502/903] Building Mathlib.Order.RelClasses
[504/903] Building Mathlib.Control.EquivFunctor
[504/903] Building Mathlib.Logic.Small.Defs
[504/903] Building Mathlib.Algebra.Opposites
[504/903] Building Mathlib.Order.Synonym
[504/903] Building Mathlib.Logic.Equiv.Basic
[510/903] Building Mathlib.Logic.Equiv.Option
[512/903] Building Mathlib.Order.Max
[512/903] Building Mathlib.Order.Compare
[512/903] Building Mathlib.Algebra.Group.OrderSynonym
[514/903] Building Mathlib.Algebra.Ring.Semiconj
[514/903] Building Mathlib.Algebra.Field.Defs
[514/903] Building Mathlib.Data.Nat.Basic
[517/903] Building Mathlib.Order.Monotone.Basic
[518/903] Building Mathlib.Algebra.Ring.OrderSynonym
[520/903] Building Mathlib.Algebra.Field.IsField
[522/903] Building Mathlib.Data.Int.Cast.Basic
[522/903] Building Mathlib.Algebra.Group.Units
[522/903] Building Mathlib.Algebra.GroupWithZero.Basic
[525/903] Building Mathlib.Tactic.Zify
[525/903] Building Mathlib.Algebra.Group.InjSurj
[528/903] Building Mathlib.Order.Iterate
[528/903] Building Mathlib.Algebra.CovariantAndContravariant
[528/903] Building Mathlib.Order.Lattice
[530/903] Building Mathlib.Algebra.Group.Commute.Hom
[530/903] Building Mathlib.Algebra.Divisibility.Basic
[530/903] Building Mathlib.Algebra.Group.Hom.Basic
[530/903] Building Mathlib.Algebra.Ring.Basic
[531/903] Building Mathlib.Algebra.Order.Ring.Lemmas
[532/903] Building Mathlib.Data.Finite.Defs
[532/903] Building Mathlib.Data.ULift
[532/903] Building Mathlib.Logic.Embedding.Basic
[534/903] Building Mathlib.Algebra.Group.Semiconj.Units
[534/903] Building Mathlib.Algebra.GroupWithZero.Units.Basic
[534/903] Building Mathlib.Algebra.Group.Units.Hom
[535/903] Building Mathlib.Data.Countable.Defs
[535/903] Building Mathlib.Algebra.Group.TypeTags
[536/903] Building Mathlib.Algebra.Divisibility.Units
[538/903] Building Mathlib.Data.Int.Basic
[538/903] Building Mathlib.Algebra.Ring.Hom.Defs
[539/903] Building Mathlib.Algebra.GroupWithZero.InjSurj
[540/903] Building Mathlib.Algebra.Group.Commute.Units
[542/903] Building Mathlib.Algebra.GroupWithZero.Divisibility
[543/903] Building Mathlib.Algebra.GroupWithZero.Semiconj
[544/903] Building Mathlib.Algebra.Group.Embedding
[544/903] Building Mathlib.Order.RelIso.Basic
[545/903] Building Mathlib.Algebra.Group.Equiv.Basic
[548/903] Building Mathlib.Order.MinMax
[548/903] Building Mathlib.Order.BoundedOrder
[550/903] Building Mathlib.Algebra.GroupWithZero.Commute
[552/903] Building Mathlib.Algebra.Ring.InjSurj
[553/903] Building Mathlib.Algebra.GroupPower.Basic
[553/903] Building Mathlib.GroupTheory.GroupAction.Defs
[557/903] Building Mathlib.Algebra.Order.Monoid.Lemmas
[559/903] Building Mathlib.Order.Disjoint
[559/903] Building Mathlib.Order.WithBot
[560/903] Building Mathlib.Algebra.Group.Hom.Instances
[561/903] Building Mathlib.Data.Nat.Bits
[561/903] Building Mathlib.Data.Nat.Units
[561/903] Building Mathlib.Tactic.NormNum.Result
[563/903] Building Mathlib.Algebra.Ring.Units
[563/903] Building Mathlib.Data.Nat.Cast.Basic
[564/903] Building Mathlib.Algebra.Ring.Divisibility.Basic
[564/903] Building Mathlib.Algebra.Group.Units.Equiv
[564/903] Building Mathlib.Algebra.Group.Opposite
[568/903] Building Mathlib.GroupTheory.GroupAction.Units
[571/903] Building Mathlib.Algebra.GroupWithZero.Units.Equiv
[572/903] Building Mathlib.Data.Int.Units
[572/903] Building Mathlib.Algebra.Ring.Commute
[574/903] Building Mathlib.Tactic.NormNum.Core
[575/903] Building Mathlib.Algebra.Order.Monoid.MinMax
[575/903] Building Mathlib.Algebra.Order.Monoid.Defs
[575/903] Building Mathlib.Algebra.Order.Monoid.NatCast
[575/903] Building Mathlib.Algebra.Order.Sub.Defs
[575/903] Building Mathlib.Algebra.Regular.Basic
[576/903] Building Mathlib.Data.Nat.Cast.Commute
[577/903] Building Mathlib.Algebra.GroupWithZero.Units.Lemmas
[582/903] Building Mathlib.Algebra.Order.Monoid.Canonical.Defs
[582/903] Building Mathlib.Algebra.Order.Monoid.OrderDual
[584/903] Building Mathlib.Order.PropInstances
[584/903] Building Mathlib.Algebra.Group.WithOne.Defs
[584/903] Building Mathlib.Order.Hom.Basic
[585/903] Building Mathlib.Algebra.Ring.Regular
[587/903] Building Mathlib.Order.Heyting.Basic
[588/903] Building Mathlib.Algebra.GroupPower.CovariantClass
[589/903] Building Mathlib.Algebra.Invertible.Basic
[589/903] Building Mathlib.Algebra.Field.Basic
[592/903] Building Mathlib.GroupTheory.GroupAction.Opposite
[592/903] Building Mathlib.Algebra.Group.Prod
[592/903] Building Mathlib.Algebra.Ring.Opposite
[594/903] Building Mathlib.Algebra.Order.Monoid.WithZero.Defs
[594/903] Building Mathlib.Algebra.Order.Monoid.TypeTags
[594/903] Building Mathlib.Algebra.Order.Sub.Canonical
[596/903] Building Mathlib.Tactic.NormNum.Basic
[598/903] Building Mathlib.Algebra.Order.Monoid.WithZero.Basic
[599/903] Building Mathlib.Algebra.Order.Monoid.WithTop
[604/903] Building Mathlib.Algebra.Order.Monoid.Basic
[604/903] Building Mathlib.Tactic.ApplyFun
[604/903] Building Mathlib.Algebra.Order.Group.Defs
[604/903] Building Mathlib.Algebra.Order.Monoid.Units
[604/903] Building Mathlib.Order.Hom.Bounded
[604/903] Building Mathlib.Order.Antisymmetrization
[608/903] Building Mathlib.GroupTheory.GroupAction.Prod
[610/903] Building Mathlib.Algebra.Order.Sub.WithTop
[611/903] Building Mathlib.Order.BooleanAlgebra
[614/903] Building Mathlib.Algebra.SMulWithZero
[616/903] Building Mathlib.Algebra.Regular.SMul
[617/903] Building Mathlib.Algebra.Order.Group.OrderIso
[617/903] Building Mathlib.Algebra.Order.Group.Instances
[617/903] Building Mathlib.Algebra.Order.Group.Units
[617/903] Building Mathlib.Algebra.Order.Ring.Defs
[620/903] Building Mathlib.Algebra.Order.WithZero
[621/903] Building Mathlib.Algebra.Order.Group.Abs
[622/903] Building Mathlib.Order.SymmDiff
[624/903] Building Mathlib.Algebra.Order.Group.MinMax
[626/903] Building Mathlib.Order.Hom.Lattice
[626/903] Building Mathlib.Data.Set.Basic
[627/903] Building Mathlib.Algebra.Order.Field.Defs
[627/903] Building Mathlib.Algebra.Order.Ring.CharZero
[627/903] Building Mathlib.Algebra.Order.Ring.Abs
[627/903] Building Mathlib.Algebra.Order.Ring.Canonical
[627/903] Building Mathlib.Algebra.Order.Positive.Ring
[628/903] Building Mathlib.Data.Int.Order.Basic
[631/903] Building Mathlib.Algebra.Order.Ring.WithTop
[631/903] Building Mathlib.Data.Nat.Order.Basic
[633/903] Building Mathlib.Data.Int.Order.Lemmas
[633/903] Building Mathlib.Data.Rat.Defs
[636/903] Building Mathlib.Data.SetLike.Basic
[636/903] Building Mathlib.Data.Set.Image
[636/903] Building Mathlib.Data.Part
[637/903] Building Mathlib.Data.Rat.Basic
[638/903] Building Mathlib.Data.Nat.Cast.Order
[638/903] Building Mathlib.Data.PNat.Basic
[638/903] Building Mathlib.Algebra.GroupPower.Ring
[638/903] Building Mathlib.Data.Nat.Order.Lemmas
[638/903] Building Mathlib.Data.Vector
[638/903] Building Mathlib.Data.List.Basic
[643/903] Building Mathlib.Data.Nat.GCD.Basic
[645/903] Building Mathlib.Data.Int.Dvd.Basic
[645/903] Building Mathlib.Algebra.Order.Invertible
[647/903] Building Mathlib.Data.Int.Div
[652/903] Building Mathlib.Algebra.Ring.Hom.Basic
[652/903] Building Mathlib.Data.Nat.Set
[652/903] Building Mathlib.Logic.Embedding.Set
[652/903] Building Mathlib.Data.Bool.Set
[652/903] Building Mathlib.Order.Directed
[652/903] Building Mathlib.Order.WellFounded
[652/903] Building Mathlib.Data.Set.Prod
[652/903] Building Mathlib.Data.Set.Sigma
[654/903] Building Mathlib.Data.Int.Cast.Lemmas
[656/903] Building Mathlib.Order.RelIso.Set
[661/903] Building Mathlib.Data.Rat.Order
[661/903] Building Mathlib.Algebra.Field.Opposite
[661/903] Building Mathlib.Tactic.Positivity.Core
[661/903] Building Mathlib.Data.Int.Cast.Field
[661/903] Building Mathlib.Data.Rat.Lemmas
[664/903] Building Mathlib.Data.Set.NAry
[664/903] Building Mathlib.Data.Set.Intervals.Basic
[664/903] Building Mathlib.Data.Set.Function
[666/903] Building Mathlib.Data.Rat.Cast.Defs
[669/903] Building Mathlib.Tactic.NormNum.OfScientific
[671/903] Building Mathlib.Data.List.Lex
[671/903] Building Mathlib.Data.List.MinMax
[671/903] Building Mathlib.Data.List.Infix
[672/903] Building Mathlib.Data.Set.Pairwise.Basic
[672/903] Building Mathlib.Algebra.Group.Pi
[672/903] Building Mathlib.Logic.Equiv.Set
[674/903] Building Mathlib.Data.List.Forall2
[676/903] Building Mathlib.Data.Set.Intervals.Monoid
[676/903] Building Mathlib.Data.Set.Intervals.Image
[676/903] Building Mathlib.Algebra.GroupPower.Order
[676/903] Building Mathlib.Order.Bounds.Basic
[677/903] Building Mathlib.Logic.Small.Basic
[677/903] Building Mathlib.Order.Hom.Set
[677/903] Building Mathlib.Algebra.Ring.Equiv
[680/903] Building Mathlib.Data.Fin.Basic
[682/903] Building Mathlib.Algebra.Ring.Pi
[682/903] Building Mathlib.GroupTheory.GroupAction.Pi
[682/903] Building Mathlib.Data.Pi.Lex
[683/903] Building Mathlib.Data.List.BigOperators.Basic
[687/903] Building Mathlib.Tactic.Linarith.Lemmas
[687/903] Building Mathlib.Data.Nat.Pow
[689/903] Building Mathlib.Order.Bounds.OrderIso
[689/903] Building Mathlib.Order.Antichain
[689/903] Building Mathlib.Data.Set.Intervals.UnorderedInterval
[689/903] Building Mathlib.Order.CompleteLattice
[691/903] Building Mathlib.Algebra.Order.Field.Basic
[692/903] Building Mathlib.Data.Nat.Size
[692/903] Building Mathlib.Algebra.GroupPower.Lemmas
[692/903] Building Mathlib.Data.Nat.Factorial.Basic
[693/903] Building Mathlib.Algebra.Ring.CompTypeclasses
[695/903] Building Mathlib.Data.Nat.ForSqrt
[695/903] Building Mathlib.Data.Nat.Bitwise
[697/903] Building Mathlib.Data.Nat.Choose.Basic
[699/903] Building Mathlib.Data.Set.List
[699/903] Building Mathlib.Data.Fin.Tuple.Basic
[700/903] Building Mathlib.Data.List.Join
[700/903] Building Mathlib.Data.List.Zip
[700/903] Building Mathlib.Data.List.Count
[700/903] Building Mathlib.Algebra.FreeMonoid.Basic
[700/903] Building Mathlib.Data.List.BigOperators.Lemmas
[702/903] Building Mathlib.Data.List.Lattice
[702/903] Building Mathlib.Data.List.Pairwise
[704/903] Building Mathlib.Data.List.Permutation
[705/903] Building Mathlib.Data.Int.Bitwise
[708/903] Building Mathlib.Data.List.Chain
[709/903] Building Mathlib.Data.List.Nodup
[715/903] Building Mathlib.Order.CompleteBooleanAlgebra
[715/903] Building Mathlib.Order.GaloisConnection
[716/903] Building Mathlib.Data.List.Dedup
[716/903] Building Mathlib.Data.List.Duplicate
[716/903] Building Mathlib.Data.List.Range
[717/903] Building Mathlib.Tactic.CancelDenoms.Core
[717/903] Building Mathlib.Data.Nat.Cast.Field
[718/903] Building Mathlib.Algebra.GroupWithZero.Power
[718/903] Building Mathlib.Tactic.NormNum.Pow
[718/903] Building Mathlib.Algebra.Parity
[718/903] Building Mathlib.Data.Int.GCD
[718/903] Building Mathlib.Algebra.GroupPower.IterateHom
[719/903] Building Mathlib.Data.List.OfFn
[722/903] Building Mathlib.Data.List.NatAntidiagonal
[722/903] Building Mathlib.Data.List.Perm
[722/903] Building Mathlib.Data.Fin.VecNotation
[725/903] Building Mathlib.GroupTheory.Perm.Basic
[729/903] Building Mathlib.Data.Setoid.Basic
[729/903] Building Mathlib.Order.Hom.Order
[730/903] Building Mathlib.Algebra.Associated
[730/903] Building Mathlib.Data.Nat.Sqrt
[733/903] Building Mathlib.Logic.Equiv.Fin
[734/903] Building Mathlib.Data.Vector.Basic
[736/903] Building Mathlib.Data.List.Sort
[736/903] Building Mathlib.Data.List.FinRange
[736/903] Building Mathlib.Data.List.Sublists
[736/903] Building Mathlib.Data.Multiset.Basic
[737/903] Building Mathlib.Data.Set.Lattice
[740/903] Building Mathlib.Dynamics.FixedPoints.Basic
[740/903] Building Mathlib.Algebra.Group.Aut
[742/903] Building Mathlib.Order.FixedPoints
[745/903] Building Mathlib.Data.List.NodupEquivFin
[746/903] Building Mathlib.GroupTheory.GroupAction.Group
[749/903] Building Mathlib.Data.Nat.Prime
[750/903] Building Mathlib.Algebra.GroupRingAction.Basic
[751/903] Building Mathlib.Algebra.Ring.Aut
[752/903] Building Mathlib.Data.Set.Intervals.OrdConnected
[752/903] Building Mathlib.Data.Set.Pairwise.Lattice
[752/903] Building Mathlib.Data.Nat.Pairing
[752/903] Building Mathlib.Order.Chain
[752/903] Building Mathlib.Data.Set.Functor
[752/903] Building Mathlib.Order.ConditionallyCompleteLattice.Basic
[752/903] Building Mathlib.Data.Set.Pointwise.Basic
[752/903] Building Mathlib.GroupTheory.Subsemigroup.Basic
[755/903] Building Mathlib.Order.Cover
[757/903] Building Mathlib.Order.Zorn
[759/903] Building Mathlib.Logic.Equiv.Nat
[760/903] Building Mathlib.GroupTheory.Subsemigroup.Operations
[760/903] Building Mathlib.GroupTheory.Submonoid.Basic
[761/903] Building Mathlib.SetTheory.Cardinal.SchroederBernstein
[762/903] Building Mathlib.Data.Countable.Basic
[762/903] Building Mathlib.Logic.Encodable.Basic
[764/903] Building Mathlib.Order.SuccPred.Basic
[764/903] Building Mathlib.Algebra.Function.Support
[767/903] Building Mathlib.Data.Multiset.Sort
[767/903] Building Mathlib.Data.Multiset.Range
[767/903] Building Mathlib.Algebra.BigOperators.Multiset.Basic
[767/903] Building Mathlib.Data.Sym.Basic
[769/903] Building Mathlib.Data.Int.CharZero
[769/903] Building Mathlib.Algebra.CharZero.Lemmas
[769/903] Building Mathlib.Algebra.Function.Indicator
[772/903] Building Mathlib.Data.Rat.Cast.CharZero
[774/903] Building Mathlib.Data.Set.Pointwise.ListOfFn
[774/903] Building Mathlib.Algebra.Bounds
[775/903] Building Mathlib.Algebra.Order.Field.Power
[776/903] Building Mathlib.Data.Nat.SuccPred
[776/903] Building Mathlib.Order.SuccPred.Limit
[777/903] Building Mathlib.GroupTheory.Submonoid.Operations
[778/903] Building Mathlib.Data.Rat.Cast.Order
[778/903] Building Mathlib.Tactic.NormNum.Inv
[778/903] Building Mathlib.Algebra.Star.Basic
[781/903] Building Mathlib.Data.ENat.Basic
[783/903] Building Mathlib.Order.SuccPred.CompleteLinearOrder
[785/903] Building Mathlib.Tactic.Positivity.Basic
[786/903] Building Mathlib.Algebra.BigOperators.Multiset.Lemmas
[786/903] Building Mathlib.Data.Multiset.Bind
[791/903] Building Mathlib.Tactic.NormNum.Eq
[791/903] Building Mathlib.Tactic.Ring.Basic
[793/903] Building Mathlib.Tactic.NormNum.Ineq
[794/903] Building Mathlib.Data.Multiset.Nodup
[795/903] Building Mathlib.Data.Multiset.Powerset
[795/903] Building Mathlib.Data.Multiset.NatAntidiagonal
[795/903] Building Mathlib.Data.Multiset.Sum
[795/903] Building Mathlib.Data.Multiset.Dedup
[795/903] Building Mathlib.Data.Multiset.Pi
[798/903] Building Mathlib.Data.Multiset.Fold
[798/903] Building Mathlib.Data.Multiset.FinsetOps
[802/903] Building Mathlib.Data.Multiset.Lattice
[802/903] Building Mathlib.Data.Finset.Basic
[804/903] Building Mathlib.Tactic.NormNum.DivMod
[805/903] Building Mathlib.Algebra.Order.Hom.Basic
[805/903] Building Mathlib.Tactic.Positivity
[807/903] Building Mathlib.Tactic.GCongr
[807/903] Building Mathlib.Algebra.Order.Pi
[808/903] Building Mathlib.Tactic.NormNum
[810/903] Building Mathlib.Data.Nat.ModEq
[810/903] Building Mathlib.Tactic.Abel
[812/903] Building Mathlib.Algebra.Order.AbsoluteValue
[813/903] Building Mathlib.Data.Nat.Parity
[816/903] Building Mathlib.Algebra.Module.Basic
[817/903] Building Mathlib.Tactic.Ring.RingNF
[817/903] Building Mathlib.Tactic.Ring.PNat
[817/903] Building Mathlib.Tactic.Linarith.Datatypes
[819/903] Building Mathlib.Tactic.Linarith.Parsing
[819/903] Building Mathlib.Tactic.Linarith.Elimination
[819/903] Building Mathlib.Tactic.Linarith.Preprocessing
[820/903] Building Mathlib.Tactic.Ring
[822/903] Building Mathlib.Data.Real.CauSeq
[823/903] Building Mathlib.Tactic.Linarith.Verification
[824/903] Building Mathlib.Data.Finset.Image
[826/903] Building Mathlib.Tactic.Linarith.Frontend
[827/903] Building Mathlib.GroupTheory.GroupAction.Hom
[827/903] Building Mathlib.Algebra.Order.Module.Synonym
[827/903] Building Mathlib.Data.Set.Pointwise.SMul
[828/903] Building Mathlib.Algebra.Order.Module.Defs
[829/903] Building Mathlib.Tactic.Linarith
[831/903] Building Mathlib.Data.Finset.Pi
[831/903] Building Mathlib.Data.Finset.Fold
[831/903] Building Mathlib.Data.Finset.Card
[831/903] Building Mathlib.Data.Fintype.Basic
[834/903] Building Mathlib.Data.Finset.Sum
[834/903] Building Mathlib.Data.Finset.Option
[834/903] Building Mathlib.Data.Finset.Prod
[839/903] Building Mathlib.Data.Real.CauSeqCompletion
[840/903] Building Mathlib.Data.Fintype.Pi
[840/903] Building Mathlib.Data.Fintype.Card
[841/903] Building Mathlib.Data.Fintype.Vector
[842/903] Building Mathlib.Data.Finset.Lattice
[844/903] Building Mathlib.Data.Fintype.Prod
[844/903] Building Mathlib.Data.Fintype.Sum
[844/903] Building Mathlib.Data.Fintype.Option
[845/903] Building Mathlib.Data.Real.Basic
[851/903] Building Mathlib.Data.Fintype.Lattice
[851/903] Building Mathlib.Data.Finset.Sigma
[851/903] Building Mathlib.Data.Finset.Powerset
[852/903] Building Mathlib.Data.Finset.Sort
[852/903] Building Mathlib.Data.ZMod.Defs
[852/903] Building Mathlib.Logic.Denumerable
[853/903] Building Mathlib.Data.Fintype.Sigma
[855/903] Building Mathlib.Data.Fintype.Powerset
[855/903] Building Mathlib.Algebra.BigOperators.Basic
[856/903] Building Mathlib.Data.Finite.Basic
[858/903] Building Mathlib.Logic.Equiv.List
[860/903] Building Mathlib.Data.Set.Finite
[862/903] Building Mathlib.Data.Set.Pointwise.Finite
[862/903] Building Mathlib.Order.ConditionallyCompleteLattice.Finset
[862/903] Building Mathlib.Data.Finset.NAry
[862/903] Building Mathlib.Data.Set.Countable
[867/903] Building Mathlib.Data.Rat.BigOperators
[867/903] Building Mathlib.Algebra.BigOperators.Option
[867/903] Building Mathlib.Data.Finset.Preimage
[867/903] Building Mathlib.Algebra.BigOperators.Ring
[867/903] Building Mathlib.Data.Finset.NoncommProd
[867/903] Building Mathlib.Algebra.BigOperators.Pi
[867/903] Building Mathlib.Data.Finsupp.Defs
[867/903] Building Mathlib.Algebra.BigOperators.Order
[870/903] Building Mathlib.Order.LocallyFinite
[872/903] Building Mathlib.Data.Fintype.BigOperators
[873/903] Building Mathlib.GroupTheory.Submonoid.Membership
[876/903] Building Mathlib.Data.Finset.LocallyFinite
[877/903] Building Mathlib.Data.Finsupp.Fin
[877/903] Building Mathlib.Data.Finsupp.Notation
[877/903] Building Mathlib.Data.Finsupp.Indicator
[882/903] Building Mathlib.Data.Nat.Interval
[883/903] Building Mathlib.Data.Fin.Interval
[883/903] Building Mathlib.Algebra.BigOperators.Intervals
[883/903] Building Mathlib.Data.Nat.Lattice
[884/903] Building Mathlib.Data.Fintype.Fin
[885/903] Building Mathlib.Data.ENat.Lattice
[886/903] Building Mathlib.Data.Nat.PartENat
[887/903] Building Mathlib.Algebra.BigOperators.Fin
[889/903] Building Mathlib.SetTheory.Cardinal.Basic
[890/903] Building Mathlib.Algebra.BigOperators.Finsupp
[891/903] Building Mathlib.SetTheory.Cardinal.Finite
[892/903] Building Mathlib.Data.Finsupp.Basic
[893/903] Building Mathlib.Data.Finset.Pointwise
[894/903] Building Mathlib.Data.Finsupp.Order
[896/903] Building Mathlib.Data.Finset.Finsupp
[897/903] Building Mathlib.Data.Finsupp.Interval
[898/903] Building Mathlib.Data.Finset.Antidiagonal
[899/903] Building Mathlib.Data.Finset.NatAntidiagonal
[900/903] Building Mathlib.Algebra.BigOperators.NatAntidiagonal
[901/903] Building Mathlib.Data.Nat.Choose.Sum
[902/903] Building Lean4Example
2024-01-02 06:40:50.279 | INFO     | __main__:main:160 - Tracing lean4-example
 94%|██████████████████████████████████████████████████████████▉    | 1541/1648 [09:20<08:44,  4.90s/it]2024-01-02 06:55:44.413 | DEBUG    | lean_dojo.data_extraction.traced_data:from_traced_files:1388 - Parsing 1542 *.ast.json files in /raid/kaiyu/tmp/tmpbvwbi6fe/lean4-example with 31 workers
2024-01-02 06:55:46,321 INFO worker.py:1715 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
  0%|                                                                          | 0/1542 [00:00<?, ?it/s](pid=2753089) 2024-01-02 06:55:47.944 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
100%|███████████████████████████████████████████████████████████████| 1542/1542 [01:37<00:00, 15.82it/s]
(pid=2753114) 2024-01-02 06:55:48.132 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication [repeated 30x across cluster] (Ray deduplicates logs by default. Set RAY_DEDUP_LOGS=0 to disable log deduplication, or see https://docs.ray.io/en/master/ray-observability/ray-logging.html#log-deduplication for more options.)
2024-01-02 06:57:26.251 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:529 - Querying the dependencies of LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-02 06:57:28.291 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for doc-gen4 main
2024-01-02 06:57:29.150 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4 v4.3.0-rc2
2024-01-02 06:57:32.333 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for std4 main
2024-01-02 06:57:33.888 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for quote4 master
2024-01-02 06:57:34.808 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4 v4.0.0
2024-01-02 06:57:37.930 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for aesop master
2024-01-02 06:57:39.032 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for ProofWidgets4 v0.0.24
2024-01-02 06:57:40.509 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-cli main
2024-01-02 06:57:42.070 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for CMark.lean main
2024-01-02 06:57:42.892 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2023-07-29
2024-01-02 06:57:45.132 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-unicode-basic main
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2024-01-02 06:57:46.402 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-cli nightly
2024-01-02 06:57:47.293 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2023-08-23
2024-01-02 06:57:49.679 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for LeanInk doc-gen
2024-01-02 06:57:50.594 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2022-12-16
2024-01-02 06:58:03.367 | DEBUG    | lean_dojo.data_extraction.traced_data:save_to_disk:1435 - Saving 1542 traced XML files to /raid/kaiyu/tmp/tmpbvwbi6fe/lean4-example with 31 workers
2024-01-02 06:58:06,347 INFO worker.py:1715 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
  0%|                                                                          | 0/1542 [00:00<?, ?it/s](pid=2779727) 2024-01-02 06:58:07.870 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
100%|███████████████████████████████████████████████████████████████| 1542/1542 [00:38<00:00, 40.48it/s]
(pid=2779768) 2024-01-02 06:58:08.011 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication [repeated 30x across cluster]
2024-01-02 06:58:52.187 | INFO     | lean_dojo.data_extraction.trace:trace:182 - Loading the traced repo from /home/kaiyu/.cache/lean_dojo/Moyvbai-lean4-example-9ed7ebe5ecd3903dc59a49995da6514f39f50bfc/lean4-example
2024-01-02 06:58:52.246 | DEBUG    | lean_dojo.data_extraction.traced_data:load_from_disk:1462 - Loading 1542 traced XML files from /raid/kaiyu/.cache/lean_dojo/Moyvbai-lean4-example-9ed7ebe5ecd3903dc59a49995da6514f39f50bfc/lean4-example with 31 workers
2024-01-02 06:58:55,223 INFO worker.py:1715 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
  0%|                                                                          | 0/1542 [00:00<?, ?it/s](pid=2799959) 2024-01-02 06:58:56.822 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
100%|███████████████████████████████████████████████████████████████| 1542/1542 [02:22<00:00, 10.80it/s]
(pid=2799977) 2024-01-02 06:58:56.871 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication [repeated 30x across cluster]
2024-01-02 07:01:20.589 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:529 - Querying the dependencies of LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-02 07:01:27.350 | DEBUG    | lean_dojo.data_extraction.traced_data:check_sanity:1328 - Checking the sanity of TracedRepo(repo=LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc'), dependencies={'lean4': LeanGitRepo(url='https://github.com/leanprover/lean4', commit='ec941735c80dc54c53948e30c428905b6600f95a'), 'mathlib': LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='089e95fb3b3ae586e821f77cd172c1bc01f70acd'), '«doc-gen4»': LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='eab9173b56295c3dadf46e104ab342060cbe2af8'), 'CMark': LeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77'), '«UnicodeBasic»': LeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='8603bb1d0d5edae780e3a85a0398fd83dbbb80a3'), 'Cli': LeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa'), 'leanInk': LeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1'), 'std': LeanGitRepo(url='https://github.com/leanprover/std4', commit='03a0f24da542fcf3fd60d9a9de9db6c5af0391f7'), 'Qq': LeanGitRepo(url='https://github.com/leanprover-community/quote4', commit='1c88406514a636d241903e2e288d21dc6d861e01'), 'aesop': LeanGitRepo(url='https://github.com/leanprover-community/aesop', commit='69404390bdc1de946bf0a2e51b1a69f308e56d7a'), 'proofwidgets': LeanGitRepo(url='https://github.com/leanprover-community/ProofWidgets4', commit='31d41415d5782a196999d4fd8eeaef3cae386a5f')}, root_dir=PosixPath('/raid/kaiyu/.cache/lean_dojo/Moyvbai-lean4-example-9ed7ebe5ecd3903dc59a49995da6514f39f50bfc/lean4-example'))
Moyvbai commented 7 months ago

@yangky11 Thank you for your reply. The environment as follows:

OS: 22.04.1-Ubuntu
python version: 3.10.13
LeanDojo version:  1.4.4

python code:

from lean_dojo import *
repo = LeanGitRepo(
    "https://github.com/Moyvbai/lean4-example",
    "9ed7ebe5ecd3903dc59a49995da6514f39f50bfc",
)
traced_repo = trace(repo)

debug mode logs:

2024-01-03 17:58:00.943 | DEBUG    | lean_dojo.constants:<module>:70 - Using GitHub personal access token for authentication
2024-01-03 17:58:05.302 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4 v4.5.0-rc1
2024-01-03 17:58:11.053 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:150 - Tracing LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-03 17:58:11.054 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:152 - Working in the temporary directory /home2/shuming/Lean/Tmp/tmpr_u61kps
2024-01-03 17:58:11.903 | DEBUG    | lean_dojo.data_extraction.lean:clone_and_checkout:483 - Cloning LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-03 17:58:13.329 | DEBUG    | lean_dojo.data_extraction.trace:_trace_lean4:109 - Tracing LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-03 17:58:13.337 | DEBUG    | lean_dojo.container:run:183 - NUM_PROCS=32 python3 build_lean4_repo.py lean4-example
2024-01-03 17:58:13.835 | INFO     | __main__:main:146 - Building lean4-example
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to './.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
[0/2] Downloading proofwidgets cloud release
[0/20] Building Std.Tactic.Unreachable
[0/21] Building Std.Lean.Command
[0/21] Building Std.Lean.TagAttribute
[0/27] Building Std.Tactic.OpenPrivate
[0/29] Building Std.Util.TermUnsafe
[0/30] Building Std.Tactic.ByCases
[0/30] Building Std.Lean.Name
[0/30] Building Std.Tactic.SeqFocus
[0/30] Building Std.Lean.Position
[0/32] Building Std.Lean.Float
[0/40] Building Std.Lean.Tactic
[0/40] Building Std.Lean.LocalContext
[0/40] Building Std.Util.ProofWanted
[0/40] Building Std.Lean.Parser
[0/41] Building Std.Lean.InfoTree
[0/44] Building Std.Lean.NameMapAttribute
[0/45] Building Std.Data.Array.Init.Basic
[0/48] Building Std.Classes.Dvd
[1/155] Building Std.Data.DList
[1/155] Building Std.Data.Option.Init.Lemmas
[1/155] Building Std.Lean.Delaborator
[1/343] Building Std.Lean.Elab.Tactic
[1/343] Building Std.Data.Fin.Init.Lemmas
[1/427] Building Std.Util.LibraryNote
[1/438] Building Std.Lean.PersistentHashMap
[1/438] Building Std.Tactic.Change
[1/449] Building Std.WF
[1/459] Building Std.Data.Ord
[1/485] Building Std.Tactic.RCases
[1/495] Building Std.Lean.Meta.Expr
[1/495] Building Std.Lean.Expr
[1/495] Building Std.Tactic.HaveI
[1/495] Building Std.Tactic.Case
[1/511] Building Std.Control.ForInStep.Basic
[1/509] Building Std.Classes.BEq
[1/525] Building Std.Lean.Meta.Inaccessible
[1/525] Building Std.Tactic.Instances
[1/529] Building Std.Tactic.LeftRight
[1/544] Building Std.Lean.MonadBacktrack
[1/555] Building Std.Lean.HashMap
[1/570] Building Std.Util.ExtendedBinder
[1/580] Building Std.Data.Prod.Lex
[1/580] Building Std.Data.MLList.Basic
[1/903] Building Std.Lean.Util.Path
[2/903] Building Std.Tactic.Replace
[2/903] Building Std.Tactic.Exact
[3/903] Building Std.Tactic.Omega.Config
[3/903] Building Std.Lean.PersistentHashSet
[3/903] Building Std.Lean.CoreM
[4/903] Building Std.Tactic.Where
[5/903] Building Std.Tactic.LabelAttr
[7/903] Building Qq.ForLean.ReduceEval
[7/903] Building Qq.ForLean.ToExpr
[8/903] Building Qq.Typ
[10/903] Building Aesop.Check
[10/903] Building Aesop.Nanos
[10/903] Building Aesop.Options.Public
[12/903] Building Aesop.Frontend.Basic
[12/903] Building Aesop.Percent
[15/903] Building Aesop.Frontend.ElabM
[16/903] Building Qq.ForLean.Do
[19/903] Building Std.Data.Nat.Basic
[19/903] Building Std.Tactic.Relation.Rfl
[19/903] Building Std.Lean.Json
[19/903] Building Qq.SortLocalDecls
[20/903] Building Std.Util.Pickle
[21/903] Building Std.Tactic.RunCmd
[22/903] Building Std.CodeAction.Attr
[24/903] Building Std.Data.Int.Basic
[24/903] Building Std.Lean.Meta.Basic
[26/903] Building Std.Tactic.Lint.Basic
[27/903] Building Std.Lean.AttributeExtra
[29/903] Building Std.Control.ForInStep.Lemmas
[31/903] Building Std.Linter.UnreachableTactic
[31/903] Building Std.Tactic.GuardExpr
[35/903] Building Std.Tactic.CoeExt
[36/903] Building Aesop.Constants
[39/903] Building Std.Tactic.PrintDependents
[39/903] Building Std.Lean.Format
[44/903] Building Std.Tactic.NoMatch
[53/903] Building Std.Data.Json
[53/903] Building Std.Test.Internal.DummyLabelAttr
[53/903] Building Aesop.Options.Internal
[58/903] Building Qq.Macro
[60/903] Building Std.Control.ForInStep
[63/903] Building Std.Linter.UnnecessarySeqFocus
[64/903] Unpacking proofwidgets cloud release
[66/903] Building Aesop.Options
[70/903] Building Mathlib.Tactic.SudoSetOption
[70/903] Building Mathlib.Util.SynthesizeUsing
[70/903] Building Mathlib.Tactic.HaveI
[70/903] Building Mathlib.Tactic.ExtendDoc
[70/903] Building Mathlib.Tactic.Classical
[70/903] Building Mathlib.Tactic.Rename
[70/903] Building Mathlib.Lean.PrettyPrinter.Delaborator
[70/903] Building Mathlib.Tactic.Set
[70/903] Building Mathlib.Tactic.TypeCheck
[70/903] Building Mathlib.Util.MemoFix
[70/903] Building Mathlib.Tactic.Attr.Register
[70/903] Building Mathlib.Tactic.UnsetOption
[70/903] Building Mathlib.Tactic.SuccessIfFailWithMsg
[70/903] Building Mathlib.Tactic.Coe
[70/903] Building Mathlib.Tactic.Clear!
[70/903] Building Mathlib.Util.AtomM
[70/903] Building Mathlib.Tactic.RunCmd
[70/903] Building Mathlib.Lean.Exception
[70/903] Building Mathlib.Tactic.ApplyWith
[70/903] Building Mathlib.Tactic.Substs
[70/903] Building Mathlib.Mathport.Attributes
[71/903] Building Mathlib.Lean.Meta.Basic
[71/903] Building ProofWidgets.Compat
[71/903] Building Mathlib.Tactic.NthRewrite
[71/903] Building Mathlib.Lean.SMap
[71/903] Building Mathlib.Tactic.FailIfNoProgress
[71/903] Building Mathlib.Tactic.SimpRw
[71/903] Building Mathlib.Util.WhatsNew
[71/903] Building Mathlib.Tactic.Clear_
[71/903] Building Mathlib.Tactic.Trace
[71/903] Building Mathlib.Tactic.InferParam
[72/903] Building Mathlib.Tactic.GuardGoalNums
[73/903] Building Mathlib.Tactic.Spread
[77/903] Building Mathlib.Lean.EnvExtension
[77/903] Building Mathlib.Tactic.Monotonicity.Attr
[77/903] Building Mathlib.Lean.Elab.Term
[78/903] Building Mathlib.Tactic.PPWithUniv
[79/903] Building Mathlib.Data.Array.Defs
[81/903] Building Mathlib.Tactic.GuardHypNums
[81/903] Building Mathlib.Tactic.ClearExcept
[81/903] Building Mathlib.Util.AssertExists
[83/903] Building Mathlib.Tactic.SimpIntro
[84/903] Building Mathlib.Init.Data.Nat.Notation
[85/903] Building Mathlib.Tactic.Widget.SelectInsertParamsClass
[87/903] Building Mathlib.Util.WithWeakNamespace
[87/903] Building Mathlib.Tactic.CasesM
[88/903] Building Mathlib.Tactic.ExtractGoal
[88/903] Building Mathlib.Util.Syntax
[90/903] Building Mathlib.Tactic.ProjectionNotation
[91/903] Building Mathlib.Tactic.Constructor
[95/903] Building Mathlib.Mathport.Rename
[95/903] Building Mathlib.Data.MLList.Basic
[97/903] Building Std.Tactic.NormCast.Ext
[97/903] Building Std.Tactic.Lint.Frontend
[98/903] Building Std.CodeAction.Basic
[99/903] Building Std.Classes.SetNotation
[99/903] Building Mathlib.Tactic.HigherOrder
[99/903] Building Std.Data.MLList.Heartbeats
[100/903] Building Std.Tactic.Lint.TypeClass
[101/903] Building Std.Classes.Cast
[102/903] Building Std.Tactic.TryThis
[103/903] Building Std.Tactic.Lint.Simp
[104/903] Building Std.Tactic.Lint.Misc
[105/903] Building Mathlib.Tactic.ApplyAt
[106/903] Building Std.Linter
[106/903] Building ProofWidgets.Component.Basic
[109/903] Building Std.Tactic.FalseOrByContra
[109/903] Building Std.Lean.Meta.Clear
[110/903] Building Std.Tactic.Relation.Symm
[110/903] Building Std.Lean.Meta.AssertHypotheses
[111/903] Building Std.Lean.Meta.SavedState
[112/903] Building Std.Lean.Meta.InstantiateMVars
[113/903] Building Mathlib.Util.CompileInductive
[114/903] Building Mathlib.Tactic.Conv
[115/903] Building Mathlib.Init.Data.Fin.Basic
[127/903] Building Mathlib.Tactic.Have
[129/903] Building Mathlib.Tactic.ScopedNS
[142/903] Building ProofWidgets.Data.Html
[144/903] Building ProofWidgets.Component.MakeEditLink
[146/903] Building Aesop.Util.EqualUpToIds
[148/903] Building Std.Tactic.NormCast.Lemmas
[151/903] Building Mathlib.Tactic.ToLevel
[151/903] Building Mathlib.Init.Quot
[151/903] Building Mathlib.Control.ULift
[151/903] Building Mathlib.Init.Data.Ordering.Basic
[156/903] Building Std.Tactic.GuardMsgs
[156/903] Building Std.CodeAction.Deprecated
[156/903] Building Std.CodeAction.Misc
[157/903] Building Std.Lean.HashSet
[157/903] Building Mathlib.Init.Set
[157/903] Building Mathlib.Util.Delaborators
[159/903] Building Mathlib.Tactic.DeriveToExpr
[160/903] Building Mathlib.Tactic.Replace
[164/903] Building Mathlib.Util.CountHeartbeats
[164/903] Building Std.Tactic.Simpa
[164/903] Building Mathlib.Tactic.Variable
[164/903] Building Std.Tactic.ShowTerm
[164/903] Building Std.Tactic.SimpTrace
[164/903] Building Mathlib.Tactic.TryThis
[166/903] Building Mathlib.Tactic.ApplyCongr
[167/903] Building Std.Lean.Util.EnvSearch
[167/903] Building Std.Tactic.Lint
[169/903] Building Mathlib.Data.Nondet.Basic
[169/903] Building Mathlib.Tactic.Simps.NotationClass
[169/903] Building Mathlib.Tactic.Lint
[170/903] Building Std.Tactic.PrintPrefix
[175/903] Building Std.Tactic.Alias
[183/903] Building Std.Data.Char
[183/903] Building Mathlib.Tactic.Recover
[185/903] Building ProofWidgets.Component.OfRpcMethod
[186/903] Building Mathlib.Tactic.Hint
[188/903] Building Std.CodeAction
[192/903] Building Std.Tactic.SqueezeScope
[192/903] Building Std.Tactic.Basic
[194/903] Building Std.Data.Bool
[196/903] Building Std.Classes.Order
[198/903] Building Mathlib.Tactic.ToExpr
[200/903] Building Mathlib.Init.Data.Bool.Basic
[203/903] Building Mathlib.Tactic.GCongr.ForwardAttr
[203/903] Building Std.Logic
[205/903] Building Mathlib.Tactic.FBinop
[207/903] Building Std.Data.Nat.Init.Lemmas
[207/903] Building Std.Data.Sum.Basic
[207/903] Building Std.Data.Fin.Iterate
[207/903] Building Std.Tactic.Omega.Logic
[207/903] Building Mathlib.Tactic.Attr.Core
[207/903] Building Mathlib.Tactic.Use
[207/903] Building Std.Data.List.Init.Lemmas
[207/903] Building Std.Classes.LawfulMonad
[207/903] Building Std.Data.PairingHeap
[207/903] Building Std.Data.RBMap.Basic
[208/903] Building Mathlib.Data.SProd
[211/903] Building Std.Data.Fin.Basic
[211/903] Building Std.Data.Nat.Lemmas
[211/903] Building Mathlib.Tactic.Widget.SelectPanelUtils
[214/903] Building Qq.Delab
[217/903] Building Std.Data.Option.Basic
[221/903] Building Std.Data.List.Init.Attach
[221/903] Building Std.Data.Array.Init.Lemmas
[221/903] Building Mathlib.Init.Control.Combinators
[223/903] Building Qq.MetaM
[224/903] Building Std.Data.Array.Basic
[227/903] Building Qq.AssertInstancesCommute
[227/903] Building Qq.Match
[228/903] Building Mathlib.Lean.Data.NameMap
[228/903] Building Std.Data.RBMap.WF
[231/903] Building Std.Data.Array.Merge
[231/903] Building Std.Data.Nat.Bitwise
[231/903] Building Std.Data.Int.Lemmas
[231/903] Building Std.Data.Nat.Gcd
[231/903] Building Std.Data.BinomialHeap.Basic
[232/903] Building Std.Data.List.Basic
[234/903] Building Std.Data.BitVec.Basic
[235/903] Building Aesop.Util.UnorderedArraySet
[235/903] Building Std.Lean.Meta.DiscrTree
[237/903] Building Std.Data.BitVec
[237/903] Building Std.Data.BitVec.Lemmas
[238/903] Building Std.Lean.Meta.Simp
[238/903] Building Std.Util.Cache
[238/903] Building Std.Tactic.Ext.Attr
[240/903] Building Std.Data.BitVec.Folds
[241/903] Building Mathlib.Tactic.Find
[242/903] Building Mathlib.Lean.Meta.Simp
[242/903] Building Std.Tactic.NormCast
[243/903] Building Std.Tactic.Ext
[243/903] Building Std.Data.Option.Lemmas
[244/903] Building Std.Data.BitVec.Bitblast
[245/903] Building Std.Tactic.Omega.Int
[245/903] Building Std.Data.Int.DivMod
[246/903] Building Qq
[248/903] Building Mathlib.Util.Qq
[254/903] Building Std.Control.Lemmas
[254/903] Building Std.Data.Sum.Lemmas
[254/903] Building Std.Tactic.Congr
[254/903] Building Std.Data.Fin.Lemmas
[255/903] Building Std.Data.BinomialHeap.Lemmas
[258/903] Building Std.Data.BinomialHeap
[259/903] Building Std.Data.Sum
[263/903] Building Mathlib.Init.Data.List.Basic
[263/903] Building Mathlib.Data.String.Defs
[263/903] Building Std.Tactic.PermuteGoals
[263/903] Building Std.Data.AssocList
[263/903] Building Mathlib.Lean.Expr.Basic
[264/903] Building Mathlib.Tactic.Widget.Conv
[264/903] Building Mathlib.Tactic.Widget.Calc
[267/903] Building Std.Data.List.Lemmas
[268/903] Building Std.Data.Rat.Basic
[269/903] Building Std.Data.RBMap
[269/903] Building Std.Data.RBMap.Alter
[270/903] Building Std.Data.HashMap.Basic
[274/903] Building Mathlib.Tactic.GeneralizeProofs
[274/903] Building Mathlib.Tactic.Cases
[274/903] Building Mathlib.Lean.Expr.Traverse
[274/903] Building Mathlib.Util.Tactic
[274/903] Building Mathlib.Tactic.HelpCmd
[274/903] Building Mathlib.Util.Imports
[275/903] Building Std.Classes.RatCast
[275/903] Building Mathlib.Data.Rat.Init
[275/903] Building Std.Data.Rat.Lemmas
[276/903] Building Mathlib.Tactic.SwapVar
[276/903] Building Mathlib.Tactic.RenameBVar
[277/903] Building Mathlib.Lean.Meta.DiscrTree
[277/903] Building Mathlib.Lean.Expr.ReplaceRec
[282/903] Building Mathlib.Lean.Expr
[283/903] Building Std.Data.HashMap.Lemmas
[283/903] Building Mathlib.Data.MLList.Dedup
[283/903] Building Mathlib.Lean.Name
[283/903] Building Aesop.Util.UnionFind
[287/903] Building Mathlib.Tactic.Core
[287/903] Building Mathlib.Tactic.Eqns
[287/903] Building Mathlib.Mathport.Notation
[290/903] Building Aesop.Util.Basic
[294/903] Building Std.Data.Rat
[296/903] Building Mathlib.Tactic.SplitIfs
[296/903] Building Mathlib.Tactic.WLOG
[297/903] Building Aesop.Rule.Name
[297/903] Building Aesop.Index.Basic
[297/903] Building Aesop.Util.Tactic
[297/903] Building Aesop.Tracing
[301/903] Building Aesop.Index
[302/903] Building Aesop.Script
[307/903] Building Aesop.RuleTac.Basic
[308/903] Building Aesop.Rule.Basic
[308/903] Building Aesop.RuleTac.Preprocess
[308/903] Building Aesop.RuleTac.Tactic
[308/903] Building Aesop.RuleTac.Cases
[308/903] Building Aesop.RuleTac.Apply
[310/903] Building Aesop.Search.Expansion.Basic
[310/903] Building Aesop.Rule
[315/903] Building Aesop.Builder.Basic
[315/903] Building Aesop.Tree.UnsafeQueue
[316/903] Building Aesop.Tree.Data
[317/903] Building Aesop.Builder.Unfold
[317/903] Building Aesop.Builder.NormSimp
[317/903] Building Aesop.Builder.Apply
[317/903] Building Aesop.Builder.Forward
[317/903] Building Aesop.Builder.Tactic
[317/903] Building Aesop.Builder.Cases
[319/903] Building Aesop.Builder.Constructors
[324/903] Building Aesop.Builder.Default
[325/903] Building Aesop.Builder
[326/903] Building Aesop.Tree.RunMetaM
[326/903] Building Aesop.Tree.Traversal
[326/903] Building Aesop.Profiling
[327/903] Building Std.Lean.System.IO
[327/903] Building Std.Data.RBMap.Lemmas
[327/903] Building Std.Data.List.Count
[327/903] Building Std.Tactic.Omega.MinNatAbs
[327/903] Building Std.Tactic.Omega.IntList
[327/903] Building Std.Data.Range.Lemmas
[327/903] Building Std.Data.Array.Lemmas
[329/903] Building Aesop.RuleSet
[330/903] Building Std.Data.MLList.IO
[331/903] Building Aesop.Tree.Tracing
[331/903] Building Aesop.Tree.TreeM
[332/903] Building Aesop.Tree.State
[336/903] Building Mathlib.Lean.Meta
[336/903] Building Std.Data.List.Pairwise
[338/903] Building Aesop.Tree.Free
[338/903] Building Aesop.Tree.ExtractScript
[338/903] Building Aesop.Tree.AddRapp
[339/903] Building Aesop.Tree.Check
[341/903] Building Aesop.Tree.ExtractProof
[343/903] Building Mathlib.Lean.Elab.Tactic.Basic
[343/903] Building Mathlib.Tactic.Backtrack
[343/903] Building Mathlib.Tactic.Relation.Rfl
[343/903] Building Mathlib.Lean.Meta.CongrTheorems
[343/903] Building Mathlib.Tactic.Relation.Symm
[344/903] Building Std.Tactic.Omega.Coeffs.IntList
[345/903] Building Std.Data.List.Perm
[346/903] Building Std.Tactic.Omega.LinearCombo
[350/903] Building Mathlib.Tactic.Relation.Trans
[352/903] Building Aesop.Frontend.Extension.Init
[352/903] Building Aesop.Search.Expansion.Simp
[352/903] Building Aesop.Frontend.RuleExpr
[353/903] Building Mathlib.Tactic.SolveByElim
[354/903] Building Aesop.Tree
[355/903] Building Aesop.Frontend.Extension
[356/903] Building Std.Tactic.Omega.OmegaM
[357/903] Building Mathlib.Tactic.Congr!
[358/903] Building Aesop.Search.Queue.Class
[361/903] Building Aesop.Search.Queue
[361/903] Building Aesop.Search.SearchM
[364/903] Building Std.Tactic.Omega.Constraint
[365/903] Building Std.Data.Array.Match
[365/903] Building Std.Data.HashMap.WF
[366/903] Building Mathlib.Tactic.Propose
[366/903] Building Mathlib.Tactic.LibrarySearch
[367/903] Building Aesop.Search.RuleSelection
[369/903] Building Std.Data.String.Basic
[371/903] Building Mathlib.Init.Core
[374/903] Building Std.Lean.Meta.UnusedNames
[374/903] Building Mathlib.Tactic.Says
[374/903] Building Std.Data.String.Lemmas
[374/903] Building Mathlib.Tactic.Simps.Basic
[376/903] Building Aesop.Frontend.Attribute
[377/903] Building Mathlib.Tactic.Observe
[378/903] Building Mathlib.Tactic.Convert
[379/903] Building Aesop.RuleTac.Forward
[380/903] Building Aesop.BuiltinRules.Intros
[380/903] Building Aesop.BuiltinRules.Assumption
[380/903] Building Aesop.Frontend.Command
[380/903] Building Aesop.BuiltinRules.Ext
[380/903] Building Aesop.BuiltinRules.Subst
[380/903] Building Aesop.BuiltinRules.DestructProducts
[380/903] Building Aesop.BuiltinRules.Split
[380/903] Building Aesop.BuiltinRules.ApplyHyps
[380/903] Building Aesop.Frontend.Tactic
[387/903] Building Aesop.RuleTac
[393/903] Building Aesop.Search.Expansion.Norm
[394/903] Building Aesop.Frontend
[395/903] Building Std.Data.HashMap
[396/903] Building Aesop.BuiltinRules
[397/903] Building Std.Tactic.Omega.Core
[399/903] Building Aesop.Search.Expansion
[400/903] Building Std.Tactic.Omega.Frontend
[401/903] Building Mathlib.Tactic.ToAdditive
[402/903] Building Std.Data.String
[404/903] Building Aesop.Search.ExpandSafePrefix
[405/903] Building Aesop.Search.Main
[406/903] Building Mathlib.Init.ZeroOne
[407/903] Building Std.Tactic.Omega
[408/903] Building Mathlib.Init.Data.Nat.Basic
[408/903] Building Mathlib.Init.Data.Int.Basic
[409/903] Building Std
[411/903] Building Mathlib.Tactic.Basic
[413/903] Building Mathlib.Tactic.RSuffices
[413/903] Building Mathlib.Tactic.Existsi
[413/903] Building Mathlib.Tactic.ExtractLets
[413/903] Building Mathlib.Tactic.MkIffOfInductiveProp
[413/903] Building Mathlib.Tactic.DefEqTransformations
[413/903] Building Mathlib.Algebra.Abs
[413/903] Building Mathlib.Tactic.Inhabit
[413/903] Building Mathlib.Init.Logic
[420/903] Building Mathlib.Init.CCLemmas
[420/903] Building Mathlib.Init.Data.Bool.Lemmas
[420/903] Building Mathlib.Init.Data.Quot
[420/903] Building Mathlib.Init.Data.Sigma.Basic
[420/903] Building Mathlib.Init.Align
[420/903] Building Mathlib.Init.Function
[420/903] Building Mathlib.Init.Propext
[420/903] Building Mathlib.Init.Algebra.Classes
[422/903] Building Aesop.Main
[427/903] Building Mathlib.Data.HashMap
[429/903] Building Aesop
[430/903] Building Mathlib.Logic.Nontrivial.Defs
[430/903] Building Mathlib.Control.Basic
[431/903] Building Mathlib.Data.Option.Defs
[431/903] Building Mathlib.Init.Order.Defs
[431/903] Building Mathlib.Logic.Basic
[433/903] Building Mathlib.Tactic.SetLike
[437/903] Building Mathlib.Control.Functor
[437/903] Building Mathlib.Tactic.Rewrites
[438/903] Building Mathlib.Init.Data.Int.Order
[438/903] Building Mathlib.Init.Order.LinearOrder
[438/903] Building Mathlib.Tactic.GCongr.Core
[440/903] Building Mathlib.Init.Data.Nat.Lemmas
[441/903] Building Mathlib.Tactic.Lift
[442/903] Building Mathlib.Logic.Nonempty
[442/903] Building Mathlib.Data.Prod.PProd
[442/903] Building Mathlib.Logic.Relator
[442/903] Building Mathlib.Algebra.NeZero
[442/903] Building Mathlib.Tactic.PushNeg
[442/903] Building Mathlib.Data.List.Defs
[442/903] Building Mathlib.Tactic.TermCongr
[442/903] Building Mathlib.Tactic.Tauto
[445/903] Building Mathlib.Logic.Function.Basic
[447/903] Building Mathlib.Init.Data.List.Lemmas
[447/903] Building Mathlib.Data.Bool.Basic
[448/903] Building Mathlib.Control.Traversable.Basic
[451/903] Building Mathlib.Init.Data.List.Instances
[455/903] Building Mathlib.Init.Data.Nat.Bitwise
[457/903] Building Mathlib.Logic.Function.Conjugate
[457/903] Building Mathlib.Data.Subtype
[457/903] Building Mathlib.Tactic.Choose
[457/903] Building Mathlib.Logic.IsEmpty
[457/903] Building Mathlib.Data.FunLike.Basic
[457/903] Building Mathlib.Data.Sum.Basic
[457/903] Building Mathlib.Data.Prod.Basic
[457/903] Building Mathlib.Algebra.Group.Defs
[457/903] Building Mathlib.Data.Sigma.Basic
[457/903] Building Mathlib.Logic.Relation
[458/903] Building Mathlib.Tactic.ByContra
[458/903] Building Mathlib.Tactic.Contrapose
[459/903] Building Mathlib.Logic.Function.Iterate
[460/903] Building Mathlib.Init.Data.Int.Bitwise
[460/903] Building Mathlib.Data.Num.Basic
[461/903] Building Mathlib.Data.FunLike.Embedding
[462/903] Building Mathlib.Tactic.Congrm
[463/903] Building Mathlib.Logic.Unique
[463/903] Building Mathlib.Data.Option.Basic
[464/903] Building Mathlib.Tactic.IrreducibleDef
[468/903] Building Mathlib.Data.FunLike.Equiv
[471/903] Building Mathlib.Tactic.Widget.Congrm
[473/903] Building Mathlib.Order.Basic
[475/903] Building Mathlib.Logic.Nontrivial.Basic
[475/903] Building Mathlib.Data.Quot
[479/903] Building Mathlib.Data.Option.NAry
[480/903] Building Mathlib.Tactic.Nontriviality.Core
[482/903] Building Mathlib.Init.Classical
[482/903] Building Mathlib.Tactic.Common
[484/903] Building Mathlib.Logic.Pairwise
[485/903] Building Mathlib.Logic.Equiv.Defs
[486/903] Building Mathlib.Tactic.Nontriviality
[488/903] Building Mathlib.Data.List.BigOperators.Defs
[488/903] Building Mathlib.Algebra.Invertible.Defs
[488/903] Building Mathlib.Control.Applicative
[488/903] Building Mathlib.Data.Nat.Cast.Defs
[488/903] Building Mathlib.Algebra.GroupWithZero.Defs
[488/903] Building Mathlib.Algebra.Group.Semiconj.Defs
[488/903] Building Mathlib.Algebra.Group.Basic
[488/903] Building Mathlib.Data.Pi.Algebra
[492/903] Building Mathlib.Algebra.Group.Commute.Defs
[493/903] Building Mathlib.Data.Nat.Cast.NeZero
[493/903] Building Mathlib.Data.Int.Cast.Defs
[494/903] Building Mathlib.Algebra.GroupWithZero.NeZero
[494/903] Building Mathlib.Algebra.Group.Hom.Defs
[498/903] Building Mathlib.Algebra.CharZero.Defs
[498/903] Building Mathlib.Algebra.Ring.Defs
[499/903] Building Mathlib.Algebra.Invertible.GroupWithZero
[502/903] Building Mathlib.Order.ULift
[502/903] Building Mathlib.Algebra.Order.ZeroLEOne
[502/903] Building Mathlib.Data.Tree
[502/903] Building Mathlib.Data.PNat.Defs
[502/903] Building Mathlib.Order.RelClasses
[504/903] Building Mathlib.Algebra.Opposites
[504/903] Building Mathlib.Order.Synonym
[504/903] Building Mathlib.Logic.Small.Defs
[504/903] Building Mathlib.Control.EquivFunctor
[504/903] Building Mathlib.Logic.Equiv.Basic
[510/903] Building Mathlib.Logic.Equiv.Option
[511/903] Building Mathlib.Order.Compare
[511/903] Building Mathlib.Order.Max
[511/903] Building Mathlib.Algebra.Group.OrderSynonym
[513/903] Building Mathlib.Algebra.Ring.Semiconj
[513/903] Building Mathlib.Data.Nat.Basic
[513/903] Building Mathlib.Algebra.Field.Defs
[517/903] Building Mathlib.Algebra.Field.IsField
[519/903] Building Mathlib.Order.Monotone.Basic
[520/903] Building Mathlib.Algebra.Ring.OrderSynonym
[521/903] Building Mathlib.Data.Int.Cast.Basic
[521/903] Building Mathlib.Algebra.GroupWithZero.Basic
[521/903] Building Mathlib.Algebra.Group.Units
[525/903] Building Mathlib.Tactic.Zify
[525/903] Building Mathlib.Algebra.Group.InjSurj
[528/903] Building Mathlib.Order.Iterate
[528/903] Building Mathlib.Algebra.CovariantAndContravariant
[528/903] Building Mathlib.Order.Lattice
[529/903] Building Mathlib.Algebra.Group.Hom.Basic
[529/903] Building Mathlib.Algebra.Group.Commute.Hom
[529/903] Building Mathlib.Algebra.Divisibility.Basic
[529/903] Building Mathlib.Algebra.Ring.Basic
[531/903] Building Mathlib.Algebra.Order.Ring.Lemmas
[532/903] Building Mathlib.Algebra.Group.Units.Hom
[532/903] Building Mathlib.Algebra.Group.Semiconj.Units
[532/903] Building Mathlib.Algebra.GroupWithZero.Units.Basic
[533/903] Building Mathlib.Data.Finite.Defs
[533/903] Building Mathlib.Data.ULift
[533/903] Building Mathlib.Logic.Embedding.Basic
[535/903] Building Mathlib.Algebra.Group.TypeTags
[535/903] Building Mathlib.Data.Countable.Defs
[537/903] Building Mathlib.Algebra.Divisibility.Units
[538/903] Building Mathlib.Algebra.Group.Commute.Units
[539/903] Building Mathlib.Algebra.GroupWithZero.InjSurj
[540/903] Building Mathlib.Algebra.Ring.Hom.Defs
[540/903] Building Mathlib.Data.Int.Basic
[541/903] Building Mathlib.Algebra.GroupWithZero.Semiconj
[543/903] Building Mathlib.Algebra.GroupWithZero.Divisibility
[544/903] Building Mathlib.Algebra.Group.Embedding
[544/903] Building Mathlib.Order.RelIso.Basic
[546/903] Building Mathlib.Algebra.Group.Equiv.Basic
[547/903] Building Mathlib.Algebra.GroupWithZero.Commute
[549/903] Building Mathlib.Algebra.Ring.InjSurj
[550/903] Building Mathlib.Order.MinMax
[550/903] Building Mathlib.Order.BoundedOrder
[555/903] Building Mathlib.Algebra.GroupPower.Basic
[555/903] Building Mathlib.GroupTheory.GroupAction.Defs
[557/903] Building Mathlib.Algebra.Order.Monoid.Lemmas
[559/903] Building Mathlib.Data.Nat.Bits
[559/903] Building Mathlib.Data.Nat.Units
[559/903] Building Mathlib.Tactic.NormNum.Result
[560/903] Building Mathlib.Order.Disjoint
[560/903] Building Mathlib.Order.WithBot
[561/903] Building Mathlib.Algebra.Group.Hom.Instances
[564/903] Building Mathlib.Algebra.Ring.Units
[564/903] Building Mathlib.Data.Nat.Cast.Basic
[566/903] Building Mathlib.Algebra.Ring.Divisibility.Basic
[566/903] Building Mathlib.Algebra.Group.Units.Equiv
[566/903] Building Mathlib.Algebra.Group.Opposite
[570/903] Building Mathlib.Tactic.NormNum.Core
[571/903] Building Mathlib.GroupTheory.GroupAction.Units
[572/903] Building Mathlib.Algebra.Ring.Commute
[572/903] Building Mathlib.Data.Int.Units
[573/903] Building Mathlib.Algebra.GroupWithZero.Units.Equiv
[575/903] Building Mathlib.Algebra.Order.Monoid.MinMax
[575/903] Building Mathlib.Algebra.Order.Monoid.Defs
[575/903] Building Mathlib.Algebra.Order.Monoid.NatCast
[575/903] Building Mathlib.Algebra.Order.Sub.Defs
[575/903] Building Mathlib.Algebra.Regular.Basic
[576/903] Building Mathlib.Data.Nat.Cast.Commute
[578/903] Building Mathlib.Algebra.GroupWithZero.Units.Lemmas
[581/903] Building Mathlib.Algebra.Group.WithOne.Defs
[581/903] Building Mathlib.Order.PropInstances
[581/903] Building Mathlib.Order.Hom.Basic
[585/903] Building Mathlib.Algebra.Order.Monoid.OrderDual
[585/903] Building Mathlib.Algebra.Order.Monoid.Canonical.Defs
[586/903] Building Mathlib.Algebra.Ring.Regular
[588/903] Building Mathlib.Order.Heyting.Basic
[589/903] Building Mathlib.GroupTheory.GroupAction.Opposite
[589/903] Building Mathlib.Algebra.Ring.Opposite
[589/903] Building Mathlib.Algebra.Group.Prod
[590/903] Building Mathlib.Algebra.Invertible.Basic
[590/903] Building Mathlib.Algebra.Field.Basic
[591/903] Building Mathlib.Algebra.GroupPower.CovariantClass
[594/903] Building Mathlib.Algebra.Order.Monoid.WithZero.Defs
[594/903] Building Mathlib.Algebra.Order.Monoid.TypeTags
[594/903] Building Mathlib.Algebra.Order.Sub.Canonical
[596/903] Building Mathlib.Tactic.NormNum.Basic
[598/903] Building Mathlib.Algebra.Order.Monoid.WithZero.Basic
[601/903] Building Mathlib.Algebra.Order.Monoid.WithTop
[604/903] Building Mathlib.Algebra.Order.Monoid.Basic
[604/903] Building Mathlib.Order.Hom.Bounded
[604/903] Building Mathlib.Algebra.Order.Monoid.Units
[604/903] Building Mathlib.Algebra.Order.Group.Defs
[604/903] Building Mathlib.Order.Antisymmetrization
[604/903] Building Mathlib.Tactic.ApplyFun
[608/903] Building Mathlib.GroupTheory.GroupAction.Prod
[610/903] Building Mathlib.Algebra.Order.Sub.WithTop
[611/903] Building Mathlib.Order.BooleanAlgebra
[614/903] Building Mathlib.Algebra.SMulWithZero
[615/903] Building Mathlib.Algebra.Regular.SMul
[617/903] Building Mathlib.Algebra.Order.Group.Units
[617/903] Building Mathlib.Algebra.Order.Group.Instances
[617/903] Building Mathlib.Algebra.Order.Group.OrderIso
[617/903] Building Mathlib.Algebra.Order.Ring.Defs
[620/903] Building Mathlib.Algebra.Order.WithZero
[621/903] Building Mathlib.Algebra.Order.Group.Abs
[622/903] Building Mathlib.Order.SymmDiff
[624/903] Building Mathlib.Algebra.Order.Group.MinMax
[626/903] Building Mathlib.Order.Hom.Lattice
[626/903] Building Mathlib.Data.Set.Basic
[627/903] Building Mathlib.Algebra.Order.Ring.CharZero
[627/903] Building Mathlib.Algebra.Order.Positive.Ring
[627/903] Building Mathlib.Algebra.Order.Field.Defs
[627/903] Building Mathlib.Algebra.Order.Ring.Canonical
[627/903] Building Mathlib.Algebra.Order.Ring.Abs
[628/903] Building Mathlib.Data.Int.Order.Basic
[631/903] Building Mathlib.Algebra.Order.Ring.WithTop
[631/903] Building Mathlib.Data.Nat.Order.Basic
[633/903] Building Mathlib.Data.Int.Order.Lemmas
[633/903] Building Mathlib.Data.Rat.Defs
[636/903] Building Mathlib.Data.Nat.Cast.Order
[636/903] Building Mathlib.Algebra.GroupPower.Ring
[636/903] Building Mathlib.Data.Vector
[636/903] Building Mathlib.Data.List.Basic
[637/903] Building Mathlib.Data.Rat.Basic
[638/903] Building Mathlib.Data.PNat.Basic
[638/903] Building Mathlib.Data.Nat.Order.Lemmas
[638/903] Building Mathlib.Data.Set.Image
[638/903] Building Mathlib.Data.Part
[638/903] Building Mathlib.Data.SetLike.Basic
[643/903] Building Mathlib.Data.Int.Dvd.Basic
[643/903] Building Mathlib.Algebra.Order.Invertible
[645/903] Building Mathlib.Data.Nat.GCD.Basic
[647/903] Building Mathlib.Data.Int.Div
[652/903] Building Mathlib.Data.Nat.Set
[652/903] Building Mathlib.Data.Set.Sigma
[652/903] Building Mathlib.Data.Bool.Set
[652/903] Building Mathlib.Order.Directed
[652/903] Building Mathlib.Order.WellFounded
[652/903] Building Mathlib.Logic.Embedding.Set
[652/903] Building Mathlib.Algebra.Ring.Hom.Basic
[652/903] Building Mathlib.Data.Set.Prod
[655/903] Building Mathlib.Data.Int.Cast.Lemmas
[657/903] Building Mathlib.Order.RelIso.Set
[661/903] Building Mathlib.Data.Rat.Order
[661/903] Building Mathlib.Algebra.Field.Opposite
[661/903] Building Mathlib.Tactic.Positivity.Core
[661/903] Building Mathlib.Data.Rat.Lemmas
[661/903] Building Mathlib.Data.Int.Cast.Field
[664/903] Building Mathlib.Data.Set.NAry
[664/903] Building Mathlib.Data.Set.Intervals.Basic
[664/903] Building Mathlib.Data.Set.Function
[666/903] Building Mathlib.Data.Rat.Cast.Defs
[669/903] Building Mathlib.Tactic.NormNum.OfScientific
[670/903] Building Mathlib.Data.List.Lex
[670/903] Building Mathlib.Data.List.MinMax
[670/903] Building Mathlib.Data.List.Infix
[673/903] Building Mathlib.Data.Set.Pairwise.Basic
[673/903] Building Mathlib.Algebra.Group.Pi
[673/903] Building Mathlib.Logic.Equiv.Set
[674/903] Building Mathlib.Data.List.Forall2
[677/903] Building Mathlib.Data.Set.Intervals.Monoid
[677/903] Building Mathlib.Algebra.GroupPower.Order
[677/903] Building Mathlib.Data.Set.Intervals.Image
[677/903] Building Mathlib.Order.Bounds.Basic
[678/903] Building Mathlib.Data.List.BigOperators.Basic
[679/903] Building Mathlib.Order.Hom.Set
[679/903] Building Mathlib.Logic.Small.Basic
[679/903] Building Mathlib.Algebra.Ring.Equiv
[683/903] Building Mathlib.Data.Fin.Basic
[684/903] Building Mathlib.Algebra.Ring.Pi
[684/903] Building Mathlib.GroupTheory.GroupAction.Pi
[684/903] Building Mathlib.Data.Pi.Lex
[685/903] Building Mathlib.Tactic.Linarith.Lemmas
[685/903] Building Mathlib.Data.Nat.Pow
[688/903] Building Mathlib.Order.Bounds.OrderIso
[688/903] Building Mathlib.Data.Set.Intervals.UnorderedInterval
[688/903] Building Mathlib.Order.Antichain
[688/903] Building Mathlib.Order.CompleteLattice
[690/903] Building Mathlib.Data.Nat.Size
[690/903] Building Mathlib.Data.Nat.Factorial.Basic
[691/903] Building Mathlib.Algebra.GroupPower.Lemmas
[692/903] Building Mathlib.Algebra.Order.Field.Basic
[694/903] Building Mathlib.Algebra.Ring.CompTypeclasses
[695/903] Building Mathlib.Data.Nat.ForSqrt
[695/903] Building Mathlib.Data.Nat.Bitwise
[696/903] Building Mathlib.Data.List.Join
[696/903] Building Mathlib.Data.List.Count
[696/903] Building Mathlib.Algebra.FreeMonoid.Basic
[696/903] Building Mathlib.Data.List.Zip
[696/903] Building Mathlib.Data.List.BigOperators.Lemmas
[698/903] Building Mathlib.Data.Nat.Choose.Basic
[700/903] Building Mathlib.Data.List.Pairwise
[700/903] Building Mathlib.Data.List.Lattice
[701/903] Building Mathlib.Data.List.Permutation
[703/903] Building Mathlib.Data.Set.List
[703/903] Building Mathlib.Data.Fin.Tuple.Basic
[705/903] Building Mathlib.Data.List.Chain
[708/903] Building Mathlib.Data.List.Nodup
[709/903] Building Mathlib.Data.Int.Bitwise
[714/903] Building Mathlib.Data.List.Dedup
[714/903] Building Mathlib.Data.List.Duplicate
[714/903] Building Mathlib.Data.List.Range
[716/903] Building Mathlib.Data.Nat.Cast.Field
[716/903] Building Mathlib.Tactic.CancelDenoms.Core
[717/903] Building Mathlib.Order.CompleteBooleanAlgebra
[717/903] Building Mathlib.Order.GaloisConnection
[719/903] Building Mathlib.Tactic.NormNum.Pow
[719/903] Building Mathlib.Algebra.Parity
[719/903] Building Mathlib.Data.Int.GCD
[719/903] Building Mathlib.Algebra.GroupWithZero.Power
[719/903] Building Mathlib.Algebra.GroupPower.IterateHom
[720/903] Building Mathlib.Data.List.NatAntidiagonal
[721/903] Building Mathlib.Data.List.Perm
[723/903] Building Mathlib.Data.List.OfFn
[723/903] Building Mathlib.Data.Fin.VecNotation
[726/903] Building Mathlib.GroupTheory.Perm.Basic
[729/903] Building Mathlib.Algebra.Associated
[729/903] Building Mathlib.Data.Nat.Sqrt
[730/903] Building Mathlib.Data.Setoid.Basic
[730/903] Building Mathlib.Order.Hom.Order
[731/903] Building Mathlib.Logic.Equiv.Fin
[734/903] Building Mathlib.Data.List.Sublists
[734/903] Building Mathlib.Data.Multiset.Basic
[736/903] Building Mathlib.Data.List.FinRange
[736/903] Building Mathlib.Data.Vector.Basic
[736/903] Building Mathlib.Data.List.Sort
[737/903] Building Mathlib.Data.Set.Lattice
[739/903] Building Mathlib.Dynamics.FixedPoints.Basic
[739/903] Building Mathlib.Algebra.Group.Aut
[742/903] Building Mathlib.Order.FixedPoints
[744/903] Building Mathlib.Data.List.NodupEquivFin
[746/903] Building Mathlib.GroupTheory.GroupAction.Group
[749/903] Building Mathlib.Data.Nat.Prime
[750/903] Building Mathlib.Algebra.GroupRingAction.Basic
[751/903] Building Mathlib.Algebra.Ring.Aut
[753/903] Building Mathlib.Data.Set.Functor
[753/903] Building Mathlib.Data.Set.Pairwise.Lattice
[753/903] Building Mathlib.Data.Nat.Pairing
[753/903] Building Mathlib.Order.Chain
[753/903] Building Mathlib.Data.Set.Intervals.OrdConnected
[753/903] Building Mathlib.GroupTheory.Subsemigroup.Basic
[753/903] Building Mathlib.Order.ConditionallyCompleteLattice.Basic
[753/903] Building Mathlib.Data.Set.Pointwise.Basic
[755/903] Building Mathlib.Order.Cover
[758/903] Building Mathlib.Order.Zorn
[759/903] Building Mathlib.Logic.Equiv.Nat
[760/903] Building Mathlib.GroupTheory.Submonoid.Basic
[760/903] Building Mathlib.GroupTheory.Subsemigroup.Operations
[761/903] Building Mathlib.SetTheory.Cardinal.SchroederBernstein
[762/903] Building Mathlib.Data.Countable.Basic
[762/903] Building Mathlib.Logic.Encodable.Basic
[763/903] Building Mathlib.Data.Multiset.Sort
[763/903] Building Mathlib.Data.Multiset.Range
[763/903] Building Mathlib.Algebra.BigOperators.Multiset.Basic
[763/903] Building Mathlib.Data.Sym.Basic
[765/903] Building Mathlib.Algebra.Function.Support
[765/903] Building Mathlib.Order.SuccPred.Basic
[771/903] Building Mathlib.Data.Int.CharZero
[771/903] Building Mathlib.Algebra.CharZero.Lemmas
[771/903] Building Mathlib.Algebra.Function.Indicator
[773/903] Building Mathlib.Data.Set.Pointwise.ListOfFn
[774/903] Building Mathlib.Algebra.Bounds
[775/903] Building Mathlib.Data.Rat.Cast.CharZero
[776/903] Building Mathlib.GroupTheory.Submonoid.Operations
[777/903] Building Mathlib.Algebra.Order.Field.Power
[779/903] Building Mathlib.Algebra.BigOperators.Multiset.Lemmas
[779/903] Building Mathlib.Data.Multiset.Bind
[780/903] Building Mathlib.Data.Nat.SuccPred
[780/903] Building Mathlib.Order.SuccPred.Limit
[781/903] Building Mathlib.Data.Rat.Cast.Order
[781/903] Building Mathlib.Tactic.NormNum.Inv
[781/903] Building Mathlib.Algebra.Star.Basic
[784/903] Building Mathlib.Data.ENat.Basic
[785/903] Building Mathlib.Order.SuccPred.CompleteLinearOrder
[788/903] Building Mathlib.Tactic.Positivity.Basic
[791/903] Building Mathlib.Data.Multiset.Nodup
[792/903] Building Mathlib.Tactic.NormNum.Eq
[792/903] Building Mathlib.Tactic.Ring.Basic
[794/903] Building Mathlib.Data.Multiset.Sum
[794/903] Building Mathlib.Data.Multiset.Pi
[794/903] Building Mathlib.Data.Multiset.NatAntidiagonal
[794/903] Building Mathlib.Data.Multiset.Powerset
[794/903] Building Mathlib.Data.Multiset.Dedup
[795/903] Building Mathlib.Tactic.NormNum.Ineq
[798/903] Building Mathlib.Data.Multiset.Fold
[798/903] Building Mathlib.Data.Multiset.FinsetOps
[802/903] Building Mathlib.Data.Multiset.Lattice
[802/903] Building Mathlib.Data.Finset.Basic
[805/903] Building Mathlib.Tactic.NormNum.DivMod
[806/903] Building Mathlib.Tactic.Positivity
[806/903] Building Mathlib.Algebra.Order.Hom.Basic
[807/903] Building Mathlib.Algebra.Order.Pi
[807/903] Building Mathlib.Tactic.GCongr
[809/903] Building Mathlib.Tactic.NormNum
[810/903] Building Mathlib.Algebra.Order.AbsoluteValue
[812/903] Building Mathlib.Data.Nat.ModEq
[812/903] Building Mathlib.Tactic.Abel
[814/903] Building Mathlib.Data.Nat.Parity
[815/903] Building Mathlib.Algebra.Module.Basic
[817/903] Building Mathlib.Data.Finset.Image
[818/903] Building Mathlib.Tactic.Ring.PNat
[818/903] Building Mathlib.Tactic.Linarith.Datatypes
[818/903] Building Mathlib.Tactic.Ring.RingNF
[820/903] Building Mathlib.Tactic.Linarith.Parsing
[820/903] Building Mathlib.Tactic.Linarith.Elimination
[820/903] Building Mathlib.Tactic.Linarith.Preprocessing
[821/903] Building Mathlib.Tactic.Ring
[823/903] Building Mathlib.Algebra.Order.Module.Synonym
[823/903] Building Mathlib.GroupTheory.GroupAction.Hom
[823/903] Building Mathlib.Data.Set.Pointwise.SMul
[824/903] Building Mathlib.Data.Real.CauSeq
[825/903] Building Mathlib.Tactic.Linarith.Verification
[826/903] Building Mathlib.Data.Finset.Fold
[826/903] Building Mathlib.Data.Finset.Pi
[826/903] Building Mathlib.Data.Fintype.Basic
[826/903] Building Mathlib.Data.Finset.Card
[827/903] Building Mathlib.Algebra.Order.Module.Defs
[830/903] Building Mathlib.Tactic.Linarith.Frontend
[832/903] Building Mathlib.Tactic.Linarith
[833/903] Building Mathlib.Data.Finset.Sum
[833/903] Building Mathlib.Data.Finset.Option
[833/903] Building Mathlib.Data.Finset.Prod
[836/903] Building Mathlib.Data.Fintype.Pi
[836/903] Building Mathlib.Data.Fintype.Card
[839/903] Building Mathlib.Data.Fintype.Vector
[842/903] Building Mathlib.Data.Finset.Lattice
[843/903] Building Mathlib.Data.Fintype.Prod
[843/903] Building Mathlib.Data.Fintype.Option
[843/903] Building Mathlib.Data.Fintype.Sum
[847/903] Building Mathlib.Data.Real.CauSeqCompletion
[849/903] Building Mathlib.Data.Real.Basic
[850/903] Building Mathlib.Data.Fintype.Lattice
[850/903] Building Mathlib.Data.Finset.Sigma
[850/903] Building Mathlib.Data.Finset.Powerset
[851/903] Building Mathlib.Data.ZMod.Defs
[851/903] Building Mathlib.Data.Finset.Sort
[851/903] Building Mathlib.Logic.Denumerable
[852/903] Building Mathlib.Data.Fintype.Sigma
[854/903] Building Mathlib.Data.Fintype.Powerset
[854/903] Building Mathlib.Algebra.BigOperators.Basic
[857/903] Building Mathlib.Data.Finite.Basic
[858/903] Building Mathlib.Logic.Equiv.List
[860/903] Building Mathlib.Data.Set.Finite
[862/903] Building Mathlib.Order.ConditionallyCompleteLattice.Finset
[862/903] Building Mathlib.Data.Set.Pointwise.Finite
[862/903] Building Mathlib.Data.Set.Countable
[862/903] Building Mathlib.Data.Finset.NAry
[867/903] Building Mathlib.Data.Rat.BigOperators
[867/903] Building Mathlib.Algebra.BigOperators.Pi
[867/903] Building Mathlib.Data.Finset.Preimage
[867/903] Building Mathlib.Algebra.BigOperators.Option
[867/903] Building Mathlib.Data.Finset.NoncommProd
[867/903] Building Mathlib.Algebra.BigOperators.Ring
[867/903] Building Mathlib.Data.Finsupp.Defs
[867/903] Building Mathlib.Algebra.BigOperators.Order
[870/903] Building Mathlib.Order.LocallyFinite
[872/903] Building Mathlib.Data.Fintype.BigOperators
[873/903] Building Mathlib.GroupTheory.Submonoid.Membership
[876/903] Building Mathlib.Data.Finset.LocallyFinite
[877/903] Building Mathlib.Data.Finsupp.Fin
[877/903] Building Mathlib.Data.Finsupp.Indicator
[877/903] Building Mathlib.Data.Finsupp.Notation
[882/903] Building Mathlib.Data.Nat.Interval
[883/903] Building Mathlib.Data.Fin.Interval
[883/903] Building Mathlib.Data.Nat.Lattice
[883/903] Building Mathlib.Algebra.BigOperators.Intervals
[884/903] Building Mathlib.Data.Fintype.Fin
[885/903] Building Mathlib.Data.ENat.Lattice
[886/903] Building Mathlib.Data.Nat.PartENat
[887/903] Building Mathlib.Algebra.BigOperators.Fin
[889/903] Building Mathlib.SetTheory.Cardinal.Basic
[890/903] Building Mathlib.Algebra.BigOperators.Finsupp
[891/903] Building Mathlib.SetTheory.Cardinal.Finite
[892/903] Building Mathlib.Data.Finsupp.Basic
[893/903] Building Mathlib.Data.Finset.Pointwise
[894/903] Building Mathlib.Data.Finsupp.Order
[896/903] Building Mathlib.Data.Finset.Finsupp
[897/903] Building Mathlib.Data.Finsupp.Interval
[898/903] Building Mathlib.Data.Finset.Antidiagonal
[899/903] Building Mathlib.Data.Finset.NatAntidiagonal
[900/903] Building Mathlib.Algebra.BigOperators.NatAntidiagonal
[901/903] Building Mathlib.Data.Nat.Choose.Sum
[902/903] Building Lean4Example
2024-01-03 18:08:22.505 | INFO     | __main__:main:160 - Tracing lean4-example

  0%|          | 0/1648 [00:00<?, ?it/s]
  0%|          | 0/1648 [00:05<?, ?it/s]
  0%|          | 0/1648 [00:10<?, ?it/s]
  0%|          | 0/1648 [00:15<?, ?it/s]
  1%|          | 16/1648 [00:20<08:30,  3.20it/s]
  2%|▏         | 25/1648 [00:25<11:23,  2.37it/s]
  2%|▏         | 32/1648 [00:30<13:57,  1.93it/s]
  2%|▏         | 35/1648 [00:35<19:08,  1.40it/s]
  3%|▎         | 43/1648 [00:40<18:08,  1.47it/s]
  3%|▎         | 50/1648 [00:45<18:23,  1.45it/s]
  3%|▎         | 54/1648 [00:50<21:29,  1.24it/s]
  4%|▍         | 63/1648 [00:55<18:39,  1.42it/s]
  4%|▍         | 71/1648 [01:00<17:51,  1.47it/s]
  5%|▍         | 75/1648 [01:05<20:43,  1.26it/s]
  5%|▌         | 83/1648 [01:10<19:04,  1.37it/s]
  5%|▌         | 89/1648 [01:15<19:44,  1.32it/s]
  6%|▌         | 96/1648 [01:20<19:17,  1.34it/s]
  6%|▌         | 102/1648 [01:25<19:51,  1.30it/s]
  7%|▋         | 112/1648 [01:30<16:58,  1.51it/s]
  7%|▋         | 117/1648 [01:35<18:49,  1.36it/s]
  8%|▊         | 127/1648 [01:40<16:22,  1.55it/s]
  8%|▊         | 132/1648 [01:45<18:15,  1.38it/s]
  8%|▊         | 140/1648 [01:50<17:21,  1.45it/s]
  9%|▉         | 147/1648 [01:55<17:27,  1.43it/s]
  9%|▉         | 149/1648 [02:00<22:14,  1.12it/s]
  9%|▉         | 152/1648 [02:05<25:48,  1.04s/it]
  9%|▉         | 156/1648 [02:10<27:08,  1.09s/it]
 10%|▉         | 160/1648 [02:15<28:08,  1.14s/it]
 10%|▉         | 162/1648 [02:20<33:37,  1.36s/it]
 10%|█         | 167/1648 [02:25<30:16,  1.23s/it]
 10%|█         | 170/1648 [02:30<32:49,  1.33s/it]
 10%|█         | 173/1648 [02:35<34:51,  1.42s/it]
 11%|█         | 176/1648 [02:40<36:25,  1.48s/it]
 11%|█         | 180/1648 [02:45<34:24,  1.41s/it]
 11%|█         | 184/1648 [02:50<33:04,  1.36s/it]
 11%|█▏        | 186/1648 [02:55<38:17,  1.57s/it]
 12%|█▏        | 190/1648 [03:00<35:27,  1.46s/it]
 12%|█▏        | 194/1648 [03:05<33:41,  1.39s/it]
 12%|█▏        | 201/1648 [03:10<26:07,  1.08s/it]
 13%|█▎        | 207/1648 [03:15<23:52,  1.01it/s]
 13%|█▎        | 216/1648 [03:20<19:11,  1.24it/s]
 13%|█▎        | 220/1648 [03:25<21:26,  1.11it/s]
 14%|█▍        | 229/1648 [03:30<17:57,  1.32it/s]
 14%|█▍        | 231/1648 [03:35<22:40,  1.04it/s]
 14%|█▍        | 235/1648 [03:40<24:18,  1.03s/it]
 14%|█▍        | 238/1648 [03:45<27:23,  1.17s/it]
 15%|█▍        | 242/1648 [03:50<27:53,  1.19s/it]
 15%|█▍        | 247/1648 [03:55<26:17,  1.13s/it]
 15%|█▌        | 252/1648 [04:00<25:15,  1.09s/it]
 16%|█▌        | 257/1648 [04:05<24:32,  1.06s/it]
 16%|█▌        | 262/1648 [04:10<24:02,  1.04s/it]
 16%|█▌        | 265/1648 [04:15<27:02,  1.17s/it]
 16%|█▋        | 268/1648 [04:20<29:36,  1.29s/it]
 16%|█▋        | 271/1648 [04:25<31:43,  1.38s/it]
 17%|█▋        | 275/1648 [04:30<30:39,  1.34s/it]
 17%|█▋        | 278/1648 [04:35<32:30,  1.42s/it]
 17%|█▋        | 279/1648 [04:40<41:22,  1.81s/it]
 17%|█▋        | 285/1648 [04:45<30:27,  1.34s/it]
 17%|█▋        | 287/1648 [04:50<35:20,  1.56s/it]
 18%|█▊        | 293/1648 [04:55<27:54,  1.24s/it]
 18%|█▊        | 299/1648 [05:00<24:16,  1.08s/it]
 18%|█▊        | 301/1648 [05:05<29:13,  1.30s/it]
 19%|█▊        | 306/1648 [05:10<26:42,  1.19s/it]
 19%|█▊        | 308/1648 [05:15<31:37,  1.42s/it]
 19%|█▉        | 313/1648 [05:20<28:01,  1.26s/it]
 19%|█▉        | 319/1648 [05:25<24:12,  1.09s/it]
 20%|█▉        | 327/1648 [05:30<19:39,  1.12it/s]
 20%|█▉        | 329/1648 [05:35<24:18,  1.11s/it]
 20%|██        | 333/1648 [05:40<25:06,  1.15s/it]
 20%|██        | 337/1648 [05:45<25:41,  1.18s/it]
 21%|██        | 342/1648 [05:50<24:18,  1.12s/it]
 21%|██        | 346/1648 [05:55<25:02,  1.15s/it]
 21%|██▏       | 353/1648 [06:00<21:02,  1.03it/s]
 22%|██▏       | 355/1648 [06:05<25:42,  1.19s/it]
 22%|██▏       | 359/1648 [06:10<25:59,  1.21s/it]
 22%|██▏       | 362/1648 [06:15<28:15,  1.32s/it]
 22%|██▏       | 369/1648 [06:20<22:25,  1.05s/it]
 22%|██▏       | 370/1648 [06:25<29:21,  1.38s/it]
 23%|██▎       | 375/1648 [06:30<26:16,  1.24s/it]
 23%|██▎       | 380/1648 [06:35<24:25,  1.16s/it]
 23%|██▎       | 383/1648 [06:40<26:50,  1.27s/it]
 24%|██▎       | 389/1648 [06:45<23:04,  1.10s/it]
 24%|██▎       | 391/1648 [06:50<27:41,  1.32s/it]
 24%|██▍       | 392/1648 [06:55<35:30,  1.70s/it]
 24%|██▍       | 397/1648 [07:00<29:15,  1.40s/it]
 24%|██▍       | 402/1648 [07:05<26:01,  1.25s/it]
 25%|██▍       | 407/1648 [07:10<24:05,  1.16s/it]
 25%|██▍       | 409/1648 [07:15<28:38,  1.39s/it]
 25%|██▌       | 414/1648 [07:20<25:34,  1.24s/it]
 25%|██▌       | 419/1648 [07:25<23:44,  1.16s/it]
 26%|██▌       | 423/1648 [07:30<24:11,  1.19s/it]
 26%|██▌       | 431/1648 [07:35<18:57,  1.07it/s]
 27%|██▋       | 437/1648 [07:40<18:12,  1.11it/s]
 27%|██▋       | 442/1648 [07:45<18:40,  1.08it/s]
 27%|██▋       | 444/1648 [07:50<22:59,  1.15s/it]
 27%|██▋       | 446/1648 [07:55<27:24,  1.37s/it]
 27%|██▋       | 452/1648 [08:00<22:52,  1.15s/it]
 28%|██▊       | 455/1648 [08:05<25:10,  1.27s/it]
 28%|██▊       | 461/1648 [08:10<21:40,  1.10s/it]
 28%|██▊       | 468/1648 [08:15<18:34,  1.06it/s]
 29%|██▉       | 479/1648 [08:20<13:54,  1.40it/s]
 29%|██▉       | 483/1648 [08:25<15:54,  1.22it/s]
 30%|██▉       | 493/1648 [08:30<13:14,  1.45it/s]
 30%|███       | 500/1648 [08:35<13:18,  1.44it/s]
 31%|███       | 507/1648 [08:40<13:20,  1.42it/s]
 31%|███▏      | 515/1648 [08:45<12:47,  1.48it/s]
 32%|███▏      | 527/1648 [08:50<10:39,  1.75it/s]
 32%|███▏      | 532/1648 [08:55<12:10,  1.53it/s]
 33%|███▎      | 539/1648 [09:00<12:24,  1.49it/s]
 33%|███▎      | 544/1648 [09:05<13:42,  1.34it/s]
 33%|███▎      | 548/1648 [09:10<15:33,  1.18it/s]
 34%|███▎      | 554/1648 [09:15<15:23,  1.18it/s]
 34%|███▍      | 562/1648 [09:20<13:49,  1.31it/s]
 34%|███▍      | 567/1648 [09:25<14:49,  1.22it/s]
 35%|███▍      | 572/1648 [09:30<15:35,  1.15it/s]
 35%|███▌      | 577/1648 [09:35<16:09,  1.11it/s]
 35%|███▌      | 583/1648 [09:40<15:39,  1.13it/s]
 36%|███▌      | 586/1648 [09:45<18:11,  1.03s/it]
 36%|███▌      | 595/1648 [09:50<14:22,  1.22it/s]
 36%|███▋      | 601/1648 [09:55<14:22,  1.21it/s]
 37%|███▋      | 608/1648 [10:00<13:39,  1.27it/s]
 38%|███▊      | 620/1648 [10:05<10:39,  1.61it/s]
 38%|███▊      | 630/1648 [10:10<09:50,  1.72it/s]
 39%|███▉      | 643/1648 [10:15<08:25,  1.99it/s]
 39%|███▉      | 650/1648 [10:20<09:11,  1.81it/s]
 40%|████      | 661/1648 [10:25<08:32,  1.93it/s]
 41%|████      | 676/1648 [10:30<07:12,  2.25it/s]
 42%|████▏     | 686/1648 [10:35<07:22,  2.17it/s]
 42%|████▏     | 695/1648 [10:40<07:42,  2.06it/s]
 43%|████▎     | 703/1648 [10:45<08:11,  1.92it/s]
 43%|████▎     | 712/1648 [10:50<08:16,  1.88it/s]
 44%|████▎     | 718/1648 [10:55<09:13,  1.68it/s]
 44%|████▍     | 721/1648 [11:00<11:24,  1.36it/s]
 44%|████▍     | 727/1648 [11:05<11:43,  1.31it/s]
 44%|████▍     | 729/1648 [11:10<14:47,  1.04it/s]
 44%|████▍     | 733/1648 [11:15<15:48,  1.04s/it]
 45%|████▍     | 740/1648 [11:20<13:49,  1.10it/s]
 45%|████▌     | 745/1648 [11:25<14:06,  1.07it/s]
 46%|████▌     | 754/1648 [11:30<11:35,  1.29it/s]
 46%|████▌     | 756/1648 [11:35<14:34,  1.02it/s]
 46%|████▋     | 763/1648 [11:40<13:00,  1.13it/s]
 47%|████▋     | 767/1648 [11:45<14:12,  1.03it/s]
 47%|████▋     | 774/1648 [11:50<12:44,  1.14it/s]
 47%|████▋     | 777/1648 [11:55<14:48,  1.02s/it]
 47%|████▋     | 781/1648 [12:00<15:36,  1.08s/it]
 48%|████▊     | 790/1648 [12:05<12:02,  1.19it/s]
 49%|████▊     | 803/1648 [12:10<08:44,  1.61it/s]
 49%|████▉     | 812/1648 [12:15<08:21,  1.67it/s]
 50%|████▉     | 819/1648 [12:20<08:42,  1.59it/s]
 51%|█████     | 836/1648 [12:25<06:21,  2.13it/s]
 51%|█████     | 840/1648 [12:30<07:46,  1.73it/s]
 52%|█████▏    | 855/1648 [12:35<06:15,  2.11it/s]
 52%|█████▏    | 861/1648 [12:40<07:08,  1.84it/s]
 53%|█████▎    | 872/1648 [12:45<06:38,  1.95it/s]
 54%|█████▎    | 883/1648 [12:50<06:18,  2.02it/s]
 54%|█████▍    | 892/1648 [12:55<06:26,  1.95it/s]
 55%|█████▌    | 910/1648 [13:00<05:01,  2.45it/s]
 56%|█████▌    | 920/1648 [13:05<05:14,  2.31it/s]
 57%|█████▋    | 937/1648 [13:10<04:29,  2.64it/s]
 58%|█████▊    | 948/1648 [13:15<04:39,  2.51it/s]
 58%|█████▊    | 955/1648 [13:20<05:18,  2.17it/s]
 59%|█████▊    | 965/1648 [13:25<05:21,  2.12it/s]
 59%|█████▉    | 975/1648 [13:30<05:22,  2.08it/s]
 60%|██████    | 989/1648 [13:35<04:46,  2.30it/s]
 60%|██████    | 997/1648 [13:40<05:11,  2.09it/s]
 61%|██████    | 1002/1648 [13:45<06:06,  1.76it/s]
 61%|██████▏   | 1012/1648 [13:50<05:47,  1.83it/s]
 62%|██████▏   | 1024/1648 [13:55<05:11,  2.00it/s]
 63%|██████▎   | 1034/1648 [14:00<05:06,  2.00it/s]
 63%|██████▎   | 1043/1648 [14:05<05:11,  1.94it/s]
 64%|██████▍   | 1051/1648 [14:10<05:24,  1.84it/s]
 64%|██████▍   | 1061/1648 [14:15<05:11,  1.89it/s]
 65%|██████▍   | 1071/1648 [14:20<05:00,  1.92it/s]
 66%|██████▌   | 1084/1648 [14:25<04:25,  2.12it/s]
 67%|██████▋   | 1097/1648 [14:30<04:03,  2.27it/s]
 67%|██████▋   | 1105/1648 [14:35<04:22,  2.07it/s]
 68%|██████▊   | 1115/1648 [14:40<04:20,  2.05it/s]
 68%|██████▊   | 1123/1648 [14:45<04:34,  1.91it/s]
 69%|██████▊   | 1129/1648 [14:50<05:05,  1.70it/s]
 69%|██████▊   | 1131/1648 [14:55<06:35,  1.31it/s]
 69%|██████▉   | 1140/1648 [15:00<05:49,  1.46it/s]
 70%|██████▉   | 1147/1648 [15:05<05:48,  1.44it/s]
 70%|███████   | 1154/1648 [15:10<05:46,  1.43it/s]
 71%|███████   | 1164/1648 [15:15<05:02,  1.60it/s]
 71%|███████   | 1170/1648 [15:20<05:23,  1.48it/s]
 72%|███████▏  | 1179/1648 [15:25<04:57,  1.57it/s]
 72%|███████▏  | 1190/1648 [15:30<04:20,  1.76it/s]
 73%|███████▎  | 1198/1648 [15:35<04:22,  1.71it/s]
 73%|███████▎  | 1209/1648 [15:40<03:56,  1.86it/s]
 74%|███████▍  | 1216/1648 [15:45<04:11,  1.72it/s]
 74%|███████▍  | 1224/1648 [15:50<04:11,  1.68it/s]
 75%|███████▍  | 1231/1648 [15:55<04:20,  1.60it/s]
 75%|███████▌  | 1240/1648 [16:00<04:06,  1.66it/s]
 76%|███████▌  | 1250/1648 [16:05<03:46,  1.76it/s]
 77%|███████▋  | 1263/1648 [16:10<03:11,  2.01it/s]
 77%|███████▋  | 1275/1648 [16:15<02:55,  2.13it/s]
 78%|███████▊  | 1286/1648 [16:20<02:48,  2.15it/s]
 79%|███████▉  | 1299/1648 [16:25<02:32,  2.28it/s]
 79%|███████▉  | 1305/1648 [16:30<02:55,  1.96it/s]
 80%|████████  | 1321/1648 [16:35<02:20,  2.33it/s]
 81%|████████  | 1332/1648 [16:40<02:17,  2.29it/s]
 82%|████████▏ | 1345/1648 [16:45<02:07,  2.38it/s]
 82%|████████▏ | 1356/1648 [16:50<02:05,  2.33it/s]
 83%|████████▎ | 1370/1648 [16:55<01:52,  2.47it/s]
 84%|████████▍ | 1384/1648 [17:00<01:42,  2.57it/s]
 84%|████████▍ | 1392/1648 [17:05<01:52,  2.28it/s]
 85%|████████▌ | 1407/1648 [17:10<01:36,  2.49it/s]
 86%|████████▌ | 1421/1648 [17:15<01:27,  2.58it/s]
 87%|████████▋ | 1435/1648 [17:20<01:20,  2.65it/s]
 88%|████████▊ | 1453/1648 [17:25<01:06,  2.93it/s]
 89%|████████▉ | 1467/1648 [17:30<01:02,  2.89it/s]
 90%|████████▉ | 1480/1648 [17:35<00:59,  2.80it/s]
 91%|█████████ | 1497/1648 [17:40<00:50,  2.98it/s]
 91%|█████████▏| 1504/1648 [17:45<00:57,  2.51it/s]
 92%|█████████▏| 1519/1648 [17:50<00:48,  2.65it/s]
 93%|█████████▎| 1532/1648 [17:55<00:43,  2.64it/s]
 93%|█████████▎| 1534/1648 [18:01<00:57,  1.97it/s]
 93%|█████████▎| 1535/1648 [18:06<01:18,  1.44it/s]
 93%|█████████▎| 1538/1648 [18:11<01:32,  1.19it/s]
 93%|█████████▎| 1539/1648 [18:36<04:29,  2.47s/it]
 93%|█████████▎| 1540/1648 [18:46<05:38,  3.14s/it]
 94%|█████████▎| 1541/1648 [19:01<07:57,  4.46s/it]2024-01-03 18:34:43.199 | WARNING  | __main__:check_files:120 - Missing /home2/shuming/Lean/Tmp/tmpr_u61kps/workspace/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json
2024-01-03 18:34:43.204 | WARNING  | __main__:check_files:120 - Missing /home2/shuming/Lean/Tmp/tmpr_u61kps/workspace/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.dep_paths
2024-01-03 18:34:44.589 | DEBUG    | lean_dojo.data_extraction.traced_data:from_traced_files:1388 - Parsing 1541 *.ast.json files in /home2/shuming/Lean/Tmp/tmpr_u61kps/lean4-example with 31 workers
2024-01-03 18:34:48,561 INFO worker.py:1664 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 

  0%|          | 0/1541 [00:00<?, ?it/s](pid=374655) 2024-01-03 18:34:52.129 | DEBUG    | lean_dojo.constants:<module>:70 - Using GitHub personal access token for authentication

  0%|          | 1/1541 [00:05<2:18:19,  5.39s/it]
  1%|          | 15/1541 [00:05<06:42,  3.79it/s] 
  1%|▏         | 23/1541 [00:05<04:08,  6.10it/s]
  2%|▏         | 29/1541 [00:06<03:11,  7.88it/s]
  2%|▏         | 34/1541 [00:06<02:50,  8.83it/s]
  2%|▏         | 38/1541 [00:06<02:51,  8.75it/s]
  3%|▎         | 41/1541 [00:07<03:07,  8.00it/s]
  3%|▎         | 48/1541 [00:08<02:41,  9.26it/s]
  3%|▎         | 53/1541 [00:08<02:02, 12.15it/s]
  4%|▎         | 56/1541 [00:08<02:41,  9.17it/s]
  4%|▍         | 61/1541 [00:08<01:59, 12.40it/s]
  4%|▍         | 64/1541 [00:09<02:40,  9.19it/s]
  4%|▍         | 67/1541 [00:09<02:15, 10.89it/s]
  5%|▍         | 71/1541 [00:10<03:05,  7.93it/s]
  5%|▌         | 81/1541 [00:10<01:35, 15.27it/s]
  6%|▌         | 86/1541 [00:10<01:18, 18.56it/s]
  6%|▌         | 92/1541 [00:11<02:12, 10.97it/s]
  6%|▋         | 98/1541 [00:11<01:44, 13.80it/s]
  7%|▋         | 102/1541 [00:13<03:20,  7.19it/s]
  7%|▋         | 106/1541 [00:13<02:48,  8.51it/s]
  7%|▋         | 111/1541 [00:13<02:10, 10.97it/s]
  7%|▋         | 114/1541 [00:15<04:16,  5.56it/s]
  8%|▊         | 116/1541 [00:15<03:51,  6.16it/s]
  8%|▊         | 120/1541 [00:15<02:48,  8.42it/s]
  8%|▊         | 123/1541 [00:15<02:25,  9.73it/s]
  8%|▊         | 126/1541 [00:17<05:10,  4.56it/s]
  9%|▊         | 134/1541 [00:17<02:44,  8.57it/s]
  9%|▉         | 138/1541 [00:17<02:10, 10.79it/s]
  9%|▉         | 142/1541 [00:17<02:08, 10.92it/s]
  9%|▉         | 145/1541 [00:19<05:08,  4.53it/s]
 10%|▉         | 150/1541 [00:19<03:30,  6.59it/s]
 10%|█         | 159/1541 [00:20<02:00, 11.49it/s]
 11%|█         | 167/1541 [00:20<01:22, 16.71it/s]
 11%|█         | 172/1541 [00:20<01:16, 17.84it/s]
 12%|█▏        | 179/1541 [00:20<00:57, 23.76it/s]
 12%|█▏        | 184/1541 [00:20<00:51, 26.54it/s]
 12%|█▏        | 189/1541 [00:23<03:46,  5.96it/s]
 13%|█▎        | 193/1541 [00:23<03:02,  7.40it/s]
 13%|█▎        | 197/1541 [00:23<02:25,  9.24it/s]
 13%|█▎        | 205/1541 [00:23<01:35, 13.97it/s]
 14%|█▎        | 211/1541 [00:23<01:13, 18.19it/s]
 14%|█▍        | 216/1541 [00:23<01:05, 20.29it/s]
 14%|█▍        | 221/1541 [00:24<00:55, 23.82it/s]
 15%|█▍        | 228/1541 [00:24<00:42, 30.70it/s]
 15%|█▌        | 235/1541 [00:24<00:34, 37.61it/s]
 16%|█▌        | 241/1541 [00:27<03:50,  5.63it/s]
 16%|█▌        | 247/1541 [00:27<02:48,  7.67it/s]
 16%|█▋        | 253/1541 [00:27<02:05, 10.28it/s]
 17%|█▋        | 258/1541 [00:27<01:43, 12.37it/s]
 17%|█▋        | 264/1541 [00:28<01:20, 15.80it/s]
 17%|█▋        | 269/1541 [00:28<01:08, 18.44it/s]
 18%|█▊        | 274/1541 [00:28<00:57, 22.07it/s]
 18%|█▊        | 279/1541 [00:28<00:48, 26.15it/s]
 18%|█▊        | 284/1541 [00:32<05:18,  3.95it/s]
 19%|█▉        | 290/1541 [00:32<03:43,  5.60it/s]
 19%|█▉        | 294/1541 [00:32<03:00,  6.90it/s]
 19%|█▉        | 300/1541 [00:32<02:08,  9.63it/s]
 20%|█▉        | 304/1541 [00:32<01:48, 11.38it/s]
 20%|██        | 311/1541 [00:33<01:15, 16.27it/s]
 21%|██        | 323/1541 [00:33<00:43, 27.72it/s]
 21%|██▏       | 330/1541 [00:33<00:39, 30.28it/s]
 22%|██▏       | 340/1541 [00:33<00:30, 39.93it/s]
 23%|██▎       | 347/1541 [00:33<00:26, 44.69it/s]
 23%|██▎       | 354/1541 [00:33<00:26, 45.13it/s]
 23%|██▎       | 360/1541 [00:38<04:22,  4.50it/s]
 24%|██▍       | 366/1541 [00:38<03:20,  5.86it/s]
 24%|██▍       | 370/1541 [00:39<02:54,  6.71it/s]
 24%|██▍       | 374/1541 [00:39<02:26,  7.99it/s]
 25%|██▍       | 379/1541 [00:39<01:51, 10.45it/s]
 25%|██▌       | 387/1541 [00:39<01:31, 12.67it/s]
 26%|██▌       | 394/1541 [00:39<01:07, 17.08it/s]
 26%|██▌       | 398/1541 [00:46<07:07,  2.67it/s]
 26%|██▌       | 402/1541 [00:46<05:36,  3.39it/s]
 27%|██▋       | 411/1541 [00:46<03:18,  5.68it/s]
 27%|██▋       | 417/1541 [00:46<02:26,  7.68it/s]
 28%|██▊       | 427/1541 [00:46<01:30, 12.31it/s]
 28%|██▊       | 434/1541 [00:46<01:11, 15.54it/s]
 29%|██▉       | 444/1541 [00:46<00:48, 22.44it/s]
 30%|██▉       | 458/1541 [00:46<00:31, 34.89it/s]
 30%|███       | 467/1541 [00:47<00:26, 40.31it/s]
 31%|███       | 476/1541 [00:47<00:23, 45.43it/s]
 32%|███▏      | 487/1541 [00:47<00:19, 54.91it/s]
 32%|███▏      | 496/1541 [00:47<00:17, 58.72it/s]
 33%|███▎      | 506/1541 [00:47<00:15, 65.50it/s]
 33%|███▎      | 515/1541 [00:47<00:18, 54.84it/s]
 34%|███▍      | 522/1541 [00:47<00:19, 52.58it/s]
 34%|███▍      | 529/1541 [00:48<00:21, 46.73it/s]
 35%|███▍      | 535/1541 [00:55<05:16,  3.18it/s]
 35%|███▌      | 541/1541 [00:55<04:02,  4.12it/s]
 35%|███▌      | 545/1541 [00:55<03:22,  4.92it/s]
 36%|███▌      | 549/1541 [00:56<02:45,  6.01it/s]
 36%|███▌      | 553/1541 [00:56<02:14,  7.35it/s]
 36%|███▌      | 557/1541 [00:56<01:54,  8.60it/s]
 37%|███▋      | 563/1541 [00:56<01:19, 12.29it/s]
 37%|███▋      | 569/1541 [00:56<01:02, 15.61it/s]
 37%|███▋      | 573/1541 [00:56<00:53, 18.08it/s]
 37%|███▋      | 577/1541 [00:57<00:49, 19.62it/s]
 38%|███▊      | 584/1541 [00:57<00:35, 26.99it/s]
 38%|███▊      | 590/1541 [00:57<00:29, 32.23it/s]
 39%|███▊      | 595/1541 [00:57<00:30, 30.98it/s]
 39%|███▉      | 601/1541 [00:57<00:25, 36.62it/s]
 39%|███▉      | 608/1541 [00:57<00:22, 41.15it/s]
 40%|███▉      | 614/1541 [00:57<00:21, 43.96it/s]
 40%|████      | 619/1541 [01:06<07:33,  2.03it/s]
 40%|████      | 623/1541 [01:07<05:59,  2.56it/s]
 41%|████      | 627/1541 [01:07<04:41,  3.24it/s]
 41%|████      | 635/1541 [01:07<02:49,  5.36it/s]
 42%|████▏     | 640/1541 [01:07<02:09,  6.95it/s]
 42%|████▏     | 645/1541 [01:07<01:39,  9.04it/s]
 42%|████▏     | 649/1541 [01:07<01:22, 10.84it/s]
 42%|████▏     | 654/1541 [01:07<01:02, 14.18it/s]
 43%|████▎     | 659/1541 [01:07<00:49, 17.66it/s]
 43%|████▎     | 666/1541 [01:08<00:35, 24.44it/s]
 44%|████▎     | 671/1541 [01:08<00:31, 27.98it/s]
 44%|████▍     | 676/1541 [01:08<00:29, 29.57it/s]
 44%|████▍     | 683/1541 [01:08<00:23, 37.07it/s]
 45%|████▍     | 689/1541 [01:08<00:21, 39.60it/s]
 45%|████▌     | 698/1541 [01:08<00:17, 47.10it/s]
 46%|████▌     | 704/1541 [01:08<00:20, 40.32it/s]
 46%|████▌     | 710/1541 [01:09<00:19, 43.65it/s]
 46%|████▋     | 716/1541 [01:09<00:18, 44.90it/s]
 47%|████▋     | 721/1541 [01:09<00:19, 42.30it/s]
 47%|████▋     | 726/1541 [01:09<00:21, 38.23it/s]
 47%|████▋     | 731/1541 [01:09<00:22, 35.69it/s]
 48%|████▊     | 737/1541 [01:09<00:19, 40.23it/s]
 48%|████▊     | 737/1541 [01:20<00:19, 40.23it/s]
 48%|████▊     | 741/1541 [01:20<08:44,  1.53it/s]
 48%|████▊     | 744/1541 [01:20<07:04,  1.88it/s]
 49%|████▊     | 748/1541 [01:20<05:16,  2.51it/s]
 49%|████▉     | 754/1541 [01:21<03:30,  3.75it/s]
 49%|████▉     | 757/1541 [01:21<02:52,  4.56it/s]
 50%|████▉     | 763/1541 [01:21<01:52,  6.93it/s]
 50%|████▉     | 769/1541 [01:21<01:20,  9.55it/s]
 50%|█████     | 775/1541 [01:21<00:58, 13.15it/s]
 51%|█████     | 781/1541 [01:21<00:43, 17.54it/s]
 51%|█████▏    | 791/1541 [01:21<00:27, 27.13it/s]
 52%|█████▏    | 800/1541 [01:22<00:20, 36.04it/s]
 52%|█████▏    | 807/1541 [01:22<00:18, 38.88it/s]
 53%|█████▎    | 814/1541 [01:22<00:18, 39.19it/s]
 53%|█████▎    | 820/1541 [01:22<00:19, 37.79it/s]
 54%|█████▎    | 825/1541 [01:22<00:18, 38.81it/s]
 54%|█████▍    | 831/1541 [01:22<00:16, 43.10it/s]
 54%|█████▍    | 837/1541 [01:22<00:17, 40.42it/s]
 55%|█████▍    | 842/1541 [01:23<00:20, 33.53it/s]
 55%|█████▍    | 846/1541 [01:23<00:20, 33.21it/s]
 55%|█████▌    | 853/1541 [01:23<00:16, 40.97it/s]
 56%|█████▌    | 860/1541 [01:23<00:15, 45.20it/s]
 56%|█████▌    | 865/1541 [01:23<00:17, 39.20it/s]
 57%|█████▋    | 872/1541 [01:23<00:16, 41.74it/s]
 57%|█████▋    | 879/1541 [01:23<00:15, 43.70it/s]
 57%|█████▋    | 884/1541 [01:24<00:18, 36.32it/s]
 58%|█████▊    | 888/1541 [01:24<00:18, 35.75it/s]
 58%|█████▊    | 893/1541 [01:24<00:17, 36.92it/s]
 58%|█████▊    | 893/1541 [01:38<00:17, 36.92it/s]
 58%|█████▊    | 899/1541 [01:38<08:13,  1.30it/s]
 58%|█████▊    | 900/1541 [01:38<07:42,  1.39it/s]
 59%|█████▊    | 903/1541 [01:38<06:06,  1.74it/s]
 59%|█████▉    | 906/1541 [01:38<04:53,  2.16it/s]
 59%|█████▉    | 908/1541 [01:39<04:04,  2.59it/s]
 59%|█████▉    | 910/1541 [01:39<03:21,  3.13it/s]
 59%|█████▉    | 913/1541 [01:39<02:40,  3.91it/s]
 60%|█████▉    | 917/1541 [01:39<01:56,  5.34it/s]
 60%|█████▉    | 919/1541 [01:40<01:48,  5.71it/s]
 60%|█████▉    | 921/1541 [01:40<01:35,  6.48it/s]
 60%|█████▉    | 923/1541 [01:40<01:42,  6.05it/s]
 60%|██████    | 926/1541 [01:40<01:16,  8.09it/s]
 60%|██████    | 929/1541 [01:40<00:57, 10.61it/s]
 60%|██████    | 931/1541 [01:41<00:51, 11.94it/s]
 61%|██████    | 935/1541 [01:41<00:37, 16.15it/s]
 61%|██████    | 943/1541 [01:41<00:21, 28.15it/s]
 62%|██████▏   | 949/1541 [01:41<00:18, 31.38it/s]
 62%|██████▏   | 954/1541 [01:41<00:16, 35.34it/s]
 62%|██████▏   | 960/1541 [01:41<00:14, 39.87it/s]
 63%|██████▎   | 965/1541 [01:42<00:21, 27.33it/s]
 63%|██████▎   | 971/1541 [01:42<00:18, 31.36it/s]
 63%|██████▎   | 971/1541 [01:58<00:18, 31.36it/s]
 63%|██████▎   | 975/1541 [01:58<09:33,  1.01s/it]
 63%|██████▎   | 976/1541 [01:58<08:55,  1.05it/s]
 64%|██████▍   | 983/1541 [01:58<05:01,  1.85it/s]
 64%|██████▍   | 987/1541 [01:59<03:46,  2.45it/s]
 64%|██████▍   | 991/1541 [01:59<02:48,  3.26it/s]
 65%|██████▍   | 994/1541 [01:59<02:24,  3.79it/s]
 65%|██████▍   | 998/1541 [01:59<01:44,  5.20it/s]
 65%|██████▌   | 1004/1541 [01:59<01:06,  8.08it/s]
 65%|██████▌   | 1008/1541 [01:59<00:51, 10.28it/s]
 66%|██████▌   | 1014/1541 [02:00<00:36, 14.62it/s]
 66%|██████▌   | 1019/1541 [02:00<00:30, 17.15it/s]
 67%|██████▋   | 1027/1541 [02:00<00:20, 24.96it/s]
 67%|██████▋   | 1032/1541 [02:00<00:18, 27.16it/s]
 67%|██████▋   | 1037/1541 [02:00<00:18, 27.73it/s]
 68%|██████▊   | 1042/1541 [02:00<00:15, 31.40it/s]
 68%|██████▊   | 1049/1541 [02:00<00:13, 36.63it/s]
 68%|██████▊   | 1055/1541 [02:01<00:12, 40.49it/s]
 69%|██████▉   | 1061/1541 [02:01<00:10, 43.76it/s]
 70%|██████▉   | 1076/1541 [02:01<00:06, 66.93it/s]
 70%|███████   | 1084/1541 [02:01<00:08, 55.77it/s]
 71%|███████   | 1092/1541 [02:01<00:07, 61.00it/s]
 71%|███████▏  | 1099/1541 [02:01<00:07, 57.23it/s]
 72%|███████▏  | 1106/1541 [02:01<00:07, 58.83it/s]
 72%|███████▏  | 1113/1541 [02:02<00:09, 44.10it/s]
 73%|███████▎  | 1119/1541 [02:02<00:09, 44.98it/s]
 73%|███████▎  | 1125/1541 [02:02<00:11, 37.69it/s]
 73%|███████▎  | 1130/1541 [02:02<00:13, 31.41it/s]
 74%|███████▎  | 1134/1541 [02:02<00:12, 32.76it/s]
 74%|███████▍  | 1138/1541 [02:02<00:12, 32.84it/s]
 74%|███████▍  | 1142/1541 [02:03<00:12, 32.83it/s]
 74%|███████▍  | 1146/1541 [02:03<00:12, 32.83it/s]
 75%|███████▍  | 1152/1541 [02:03<00:11, 33.96it/s]
 75%|███████▌  | 1158/1541 [02:03<00:09, 38.98it/s]
 76%|███████▌  | 1164/1541 [02:03<00:08, 43.61it/s]
 76%|███████▌  | 1173/1541 [02:03<00:06, 54.58it/s]
 77%|███████▋  | 1179/1541 [02:03<00:09, 40.13it/s]
 77%|███████▋  | 1184/1541 [02:04<00:10, 32.68it/s]
 77%|███████▋  | 1189/1541 [02:04<00:10, 35.07it/s]
 77%|███████▋  | 1194/1541 [02:04<00:09, 37.55it/s]
 78%|███████▊  | 1200/1541 [02:04<00:08, 40.66it/s]
 78%|███████▊  | 1200/1541 [02:27<00:08, 40.66it/s]
 78%|███████▊  | 1205/1541 [02:27<07:04,  1.26s/it]
 78%|███████▊  | 1207/1541 [02:27<06:10,  1.11s/it]
 79%|███████▊  | 1211/1541 [02:27<04:28,  1.23it/s]
 79%|███████▉  | 1214/1541 [02:27<03:30,  1.55it/s]
 79%|███████▉  | 1218/1541 [02:27<02:28,  2.18it/s]
 79%|███████▉  | 1221/1541 [02:28<01:56,  2.74it/s]
 79%|███████▉  | 1225/1541 [02:28<01:22,  3.85it/s]
 80%|███████▉  | 1228/1541 [02:28<01:05,  4.77it/s]
 80%|███████▉  | 1231/1541 [02:28<00:51,  5.98it/s]
 80%|████████  | 1237/1541 [02:28<00:31,  9.77it/s]
 81%|████████  | 1241/1541 [02:28<00:24, 12.02it/s]
 81%|████████  | 1248/1541 [02:29<00:16, 18.31it/s]
 81%|████████▏ | 1254/1541 [02:29<00:12, 22.58it/s]
 82%|████████▏ | 1262/1541 [02:29<00:08, 31.20it/s]
 82%|████████▏ | 1268/1541 [02:29<00:08, 33.19it/s]
 83%|████████▎ | 1275/1541 [02:29<00:08, 32.20it/s]
 83%|████████▎ | 1280/1541 [02:29<00:08, 31.06it/s]
 84%|████████▍ | 1292/1541 [02:29<00:05, 45.65it/s]
 85%|████████▍ | 1304/1541 [02:30<00:03, 60.18it/s]
 85%|████████▌ | 1312/1541 [02:30<00:04, 53.05it/s]
 86%|████████▌ | 1319/1541 [02:30<00:04, 48.74it/s]
 86%|████████▌ | 1325/1541 [02:30<00:05, 41.88it/s]
 86%|████████▋ | 1330/1541 [02:30<00:05, 35.27it/s]
 87%|████████▋ | 1336/1541 [02:30<00:05, 39.02it/s]
 87%|████████▋ | 1344/1541 [02:31<00:04, 46.70it/s]
 88%|████████▊ | 1350/1541 [02:31<00:04, 45.71it/s]
 88%|████████▊ | 1356/1541 [02:31<00:04, 42.59it/s]
 89%|████████▉ | 1372/1541 [02:31<00:02, 58.46it/s]
 89%|████████▉ | 1379/1541 [02:31<00:02, 57.58it/s]
 90%|████████▉ | 1386/1541 [02:31<00:02, 59.32it/s]
 90%|█████████ | 1393/1541 [02:32<00:03, 46.42it/s]
 91%|█████████ | 1399/1541 [02:32<00:03, 44.71it/s]
 91%|█████████ | 1404/1541 [02:32<00:03, 44.87it/s]
 92%|█████████▏| 1414/1541 [02:32<00:02, 57.21it/s]
 92%|█████████▏| 1421/1541 [02:32<00:02, 53.07it/s]
 93%|█████████▎| 1429/1541 [02:32<00:01, 58.61it/s]
 93%|█████████▎| 1437/1541 [02:32<00:01, 62.97it/s]
 94%|█████████▍| 1445/1541 [02:32<00:01, 60.54it/s]
 94%|█████████▍| 1452/1541 [02:33<00:01, 54.36it/s]
 95%|█████████▍| 1458/1541 [02:33<00:01, 48.85it/s]
 95%|█████████▌| 1464/1541 [02:33<00:02, 33.39it/s]
 95%|█████████▌| 1464/1541 [02:58<00:02, 33.39it/s]
 95%|█████████▌| 1468/1541 [02:58<01:32,  1.27s/it]
 96%|█████████▌| 1472/1541 [02:58<01:09,  1.01s/it]
 96%|█████████▌| 1476/1541 [02:58<00:51,  1.27it/s]
 96%|█████████▌| 1479/1541 [02:59<00:39,  1.55it/s]
 96%|█████████▌| 1482/1541 [02:59<00:29,  1.97it/s]
 96%|█████████▋| 1485/1541 [02:59<00:21,  2.56it/s]
 97%|█████████▋| 1488/1541 [02:59<00:16,  3.24it/s]
 97%|█████████▋| 1491/1541 [02:59<00:12,  4.13it/s]
 97%|█████████▋| 1494/1541 [03:00<00:09,  4.85it/s]
 97%|█████████▋| 1498/1541 [03:00<00:06,  6.62it/s]
 97%|█████████▋| 1500/1541 [03:00<00:05,  7.14it/s]
 98%|█████████▊| 1509/1541 [03:00<00:02, 14.71it/s]
 98%|█████████▊| 1513/1541 [03:00<00:01, 17.32it/s]
 99%|█████████▊| 1518/1541 [03:00<00:01, 21.72it/s]
 99%|█████████▉| 1524/1541 [03:01<00:00, 27.09it/s]
 99%|█████████▉| 1529/1541 [03:01<00:00, 23.73it/s]
100%|█████████▉| 1534/1541 [03:01<00:00, 27.15it/s]
100%|█████████▉| 1538/1541 [03:04<00:00,  4.51it/s]
100%|██████████| 1541/1541 [03:16<00:00,  1.00it/s]
100%|██████████| 1541/1541 [03:16<00:00,  7.86it/s]
(pid=374690) 2024-01-03 18:34:52.448 | DEBUG    | lean_dojo.constants:<module>:70 - Using GitHub personal access token for authentication [repeated 30x across cluster] (Ray deduplicates logs by default. Set RAY_DEDUP_LOGS=0 to disable log deduplication, or see https://docs.ray.io/en/master/ray-observability/ray-logging.html#log-deduplication for more options.)
2024-01-03 18:38:09.790 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:529 - Querying the dependencies of LeanGitRepo(url='https://github.com/Moyvbai/lean4-example', commit='9ed7ebe5ecd3903dc59a49995da6514f39f50bfc')
2024-01-03 18:38:15.229 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for doc-gen4 main
2024-01-03 18:38:17.544 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4 v4.3.0-rc2
2024-01-03 18:38:23.038 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for std4 main
2024-01-03 18:38:26.676 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for quote4 master
2024-01-03 18:38:28.992 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4 v4.0.0
2024-01-03 18:38:34.389 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for aesop master
2024-01-03 18:38:37.309 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for ProofWidgets4 v0.0.24
2024-01-03 18:38:40.815 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-cli main
2024-01-03 18:38:44.874 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for CMark.lean main
2024-01-03 18:38:47.139 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2023-07-29
2024-01-03 18:38:51.110 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-unicode-basic main
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2024-01-03 18:38:54.397 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-cli nightly
2024-01-03 18:38:56.757 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2023-08-23
2024-01-03 18:39:00.759 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for LeanInk doc-gen
2024-01-03 18:39:03.127 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:42 - Querying the commit hash for lean4-nightly nightly-2022-12-16
Traceback (most recent call last):
  File "/home2/shuming/demo/lean.py", line 21, in <module>
    traced_repo = trace(repo)
  File "/home2/shuming/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 181, in trace
    cached_path = get_traced_repo_path(repo)
  File "/home2/shuming/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 154, in get_traced_repo_path
    traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name)
  File "/home2/shuming/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1409, in from_traced_files
    traced_files_graph = _build_dependency_graph(traced_files, root_dir, repo)
  File "/home2/shuming/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1240, in _build_dependency_graph
    tf_dep = TracedFile.from_traced_file(root_dir, json_path, repo)
  File "/home2/shuming/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 638, in from_traced_file
    raise FileNotFoundError(f"{json_path} does not exist")
FileNotFoundError: /home2/shuming/Lean/Tmp/tmpr_u61kps/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json does not exist
yangky11 commented 7 months ago

Given these lines in the log,

 94%|█████████▎| 1541/1648 [19:01<07:57,  4.46s/it]2024-01-03 18:34:43.199 | WARNING  | __main__:check_files:120 - Missing /home2/shuming/Lean/Tmp/tmpr_u61kps/workspace/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json
2024-01-03 18:34:43.204 | WARNING  | __main__:check_files:120 - Missing /home2/shuming/Lean/Tmp/tmpr_u61kps/workspace/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.dep_paths

it looks like the same OOM issue with https://github.com/lean-dojo/LeanDojo/issues/41#issuecomment-1692511187.

How much RAM do you have?

Moyvbai commented 7 months ago

This computer’s RAM is 64GB, and I initially thought it was enough. When I ran the same code on a computer with 512GB of RAM, I found that a single process occupied up to 100GB of memory. But this time, it didn't throw an error. Thanks for helping me find the cause of the problem.