Commit 2025-08-14 23:22 609d272e

feat: tactic analysis framework (#26683) We introduce a tactic analysis framework, which allows you to write metaprograms that scan through sequences of tactics in a proof. This can be useful for linters (for example: two calls to rw that can be merged into one) or debugging (for example: making sure grind can cleanly replace omega). An analysis pass comes with an option; the ones introduced in this PR (also for debugging the framework itself) are disabled by default. The main motivation for this PR is debugging grind on the nightly-testing branch. I am still unhappy with the ComplexConfig interface, which I would like to redesign. In the meantime, the lower-level config interface seems robust and flexible enough to deal with various types of analyses.