Commit 2026-03-18 08:30 30ea3163
View on Github →chore: replace aesop with grind where the latter is significantly faster (#35947)
This experiment investigates the impact of replacing particularly heavy aesop calls with grind, specifically how this change affects the instruction count as measured by the benchmarking infrastructure.
Trace profiling results (differences <30 ms considered measurement noise):
Submonoid.mem_closure_image_one_lt_iff: 125 ms before, 61 ms after 🎉SimpleGraph.Connected.connected_delete_edge_of_not_isBridge: 230 ms before, 51 ms after 🎉SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv: 899 ms before, 666 ms after 🎉SimpleGraph.IsCycles.existsUnique_ne_adj: 855 ms before, 599 ms after 🎉SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge: 962 ms before, 619 ms after 🎉SimpleGraph.IsAlternating.sup_edge: 2854 ms before, 1615 ms after 🎉SimpleGraph.Subgraph.IsPerfectMatching.symmDiff_of_isAlternating: 3103 ms before, 1734 ms after 🎉SimpleGraph.edgeSet_replaceVertex_of_not_adj: 1525 ms before, 933 ms after 🎉SimpleGraph.edgeSet_replaceVertex_of_adj: 2194 ms before, 1605 ms after 🎉SimpleGraph.tutte_exists_isPerfectMatching_of_near_matchings: 3161 ms before, 1652 ms after 🎉RootPairing.Base.sub_notMem_range_root: 1025 ms before, 978 ms after 🎉RootPairing.EmbeddedG2.mem_allRoots: 3832 ms before, 3255 ms after 🎉RootSystem.GeckConstruction.Lemmas.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_2: 3572 ms before, 2631 ms after 🎉isCompact_generateFrom: 1987 ms before, 763 ms after 🎉IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered: 2279 ms before, 2009 ms after 🎉UniformContinuousOn.comp_tendstoUniformly_eventually: 416 ms before, 151 ms after 🎉 Profiled usingset_option trace.profiler true in.