chore: import less

[TwoFX]

No description provided.

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 752b604 against a0777ef are in. There are significant results. @TwoFX

• ✅ build//instructions: -55.8G (-0.54%)

Large changes (12✅)

• ✅ build/stat/imported bytes//bytes: -2GiB (-5.64%)
• ✅ build/stat/imported consts//amount: -4.4M (-5.36%)
• ✅ build/stat/imported modules//amount: -156.6k (-8.62%)
• ✅ elab/bv_decide_inequality//maxrss: -93MiB (-10.93%)
• ✅ elab/bv_decide_large_aig//maxrss: -103MiB (-7.45%)
• ✅ elab/bv_decide_mul//maxrss: -95MiB (-10.95%)
• ✅ elab/bv_decide_rewriter//maxrss: -99MiB (-12.88%)
• ✅ elab/bv_decide_sym_rewriter//maxrss: -102MiB (-13.22%)
• ✅ elab/bv_stress_replicate//maxrss: -105MiB (-12.91%)
• ✅ elab/bv_stress_structures_1//maxrss: -96MiB (-12.62%)
• ✅ elab/bv_stress_structures_2//maxrss: -98MiB (-12.28%)
• ✅ elab/charactersIn//instructions: -701.0M (-2.80%)

Medium changes (12✅)

• ✅ build/module/Lean.Meta.Tactic.Grind.AC.Seq//instructions: -1.1G (-21.66%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Sat.CNF.Basic//instructions: -1.9G (-19.42%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -2.2G (-4.29%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: -1.0G (-6.03%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -1.8G (-2.14%)
• ✅ build/module/Std.Tactic.BVDecide.LRAT.Internal.Checker//instructions: -1.0G (-33.78%) (reduced significance based on absolute threshold)
• ✅ elab/bv_decide_mul//instructions: -67.6M (-0.27%)
• ✅ elab/bv_decide_realworld//maxrss: -107MiB (-12.11%)
• ✅ elab/bv_decide_rewriter//instructions: -64.8M (-1.26%)
• ✅ elab/workspaceSymbols//instructions: -240.0M (-1.37%)
• ✅ misc/import Lean cold//instructions: -21.7M (-2.22%)
• ✅ misc/import Lean//instructions: -21.7M (-2.22%)

Small changes (1263✅, 10🟥)

• ✅ build/module/Init.Data.Array.Lex.Basic//instructions: -2.3M (-0.19%)
• ✅ build/module/Init.Data.Array.Lex//instructions: -1.5M (-0.34%)
• ✅ build/module/Init.Data.Array.QSort//instructions: -1.5M (-0.34%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Sort.Basic//instructions: -6.4M (-0.26%)
• ✅ build/module/Init.Data.Array.Sort//instructions: -9.5M (-2.07%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.TakeDrop//instructions: -3.7M (-0.65%)
• ✅ build/module/Init.Data.Array//instructions: -5.6M (-1.18%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -423.9M (-0.91%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.ByteArray.Extra//instructions: -3.6M (-0.59%)
• ✅ build/module/Init.Data.ByteArray.Lex//instructions: -3.7M (-0.38%)
• ✅ build/module/Init.Data.ByteArray//instructions: -3.2M (-0.70%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Dyadic.Instances//instructions: -4.1M (-0.52%)
• ✅ build/module/Init.Data.Dyadic//instructions: -4.0M (-0.89%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Float.Model.Float32//instructions: -2.5M (-0.29%)
• ✅ build/module/Init.Data.Float.Model.Format.Valid//instructions: -4.3M (-0.88%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Float.Model.Format//instructions: -4.2M (-0.90%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Float.Model.Unpacked.Basic//instructions: -4.2M (-0.56%)
• ✅ build/module/Init.Data.Float.Model.Unpacked.Operations.Add//instructions: -4.2M (-0.77%)
• ✅ build/module/Init.Data.Float.Model.Unpacked.Operations.Compare//instructions: -4.3M (-0.69%)
• ✅ build/module/Init.Data.Float.Model.Unpacked.Operations.Div//instructions: -4.0M (-0.66%) (reduced significance based on absolute threshold)
• and 1252 more
• and 1 hidden