[Merged by Bors] - feat: tactic analysis framework by Vierkantor · Pull Request #26683 · leanprover-community/mathlib4

Vierkantor · 2025-07-03T17:09:06Z

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.

github-actions · 2025-07-03T17:10:23Z

PR summary dac1d0caf8

Import changes exceeding 2%

%	File
+16.67%	`Mathlib.Init`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.ExtractGoal	35	14	-21 (-60.00%)
Mathlib.Init	30	35	+5 (+16.67%)
Mathlib.Tactic	2944	2949	+5 (+0.17%)

Import changes for all files

Files	Import difference
There are 6700 files with changed transitive imports taking up over 283434 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

+ ComplexConfig
+ Config
+ Config.ofComplex
+ Entry
+ Entry.import
+ Pass
+ TriggerCondition
+ findTacticSeqs
+ goalSignature
+ grindReplacementWith
+ instance : Ord Entry
+ linarithToGrind
+ mergeWithGrind
+ omegaToGrind
+ ringToGrind
+ runCoreMWithMessages
+ runMetaMWithMessages
+ runPass
+ runPasses
+ runTactic
+ rwMerge
+ tacticAnalysis
+ terminalToGrind
+ testTacticSeq
+ x
+ xy
+ y
+ yz
+ z

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-07-03T18:41:32Z

Let me just say that I'm extremely excited to see such a tactic analysis tool!
Your use case sounds very interesting, I have another one: for a "there's a faster tactic to do this" linter, e.g. testing if continuity can be replaced by fun_prop. I never was bothered enough to write one myself, but would look forward to using it!

Vierkantor · 2025-07-08T14:37:57Z

I added a test for number of heartbeats! This seems to have been much easier than I expected! Today I tried and failed to make it work for a sequence of tactics too, but it seems very hard to look at an infotree and figure out where the individual tactics live, and which ones follow each other. Perhaps we should be tracking the list of goals, like in the flexible tactics linter?

I'll be on holiday for the coming 2 weeks, and will pick this up in a bit. The single tactic usecase seems to work well, feel free to play around with your continuity/fun_prop idea!

Mathlib/Tactic/TacticAnalysis.lean

Mathlib/Tactic/TacticAnalysis/Declarations.lean

Mathlib/Tactic/ExtractGoal.lean

Mathlib/Tactic/TacticAnalysis.lean

Mathlib/Tactic/TacticAnalysis/Declarations.lean

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Mathlib/Tactic/TacticAnalysis.lean

kim-em · 2025-08-14T23:21:56Z

bors merge

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

mathlib-bors · 2025-08-15T00:14:55Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Vierkantor added 2 commits July 3, 2025 19:05

Check if there is a call to linarith that we can replace with grind.

9e23fed

Import in Mathlib.Init.

2f1dd2b

Vierkantor added the WIP Work in progress label Jul 3, 2025

github-actions bot added t-meta Tactics, attributes or user commands large-import Automatically added label for PRs with a significant increase in transitive imports labels Jul 3, 2025

Vierkantor added 2 commits July 3, 2025 19:18

Fix panics

07fc0ba

mk_all

980e322

Vierkantor added 5 commits July 7, 2025 10:48

Rename

e549c20

Refactor: extract the runTactic code

2b5f5ca

Move context and state between the CommandElabM and the MetaM

d74e84d

Test for number of heartbeats too

eab7261

Some configurability

c2f66fd

Vierkantor added 5 commits July 21, 2025 11:24

Merge remote-tracking branch 'upstream/master' into t4t

7f0b338

Merge remote-tracking branch 'upstream/master' into t4t

ec235d0

Merge remote-tracking branch 'upstream/master' into t4t

59680c6

Fix grind being unable to create auxiliary theorems sometimes

003cdc7

Support sequences of tactics

1f1b640

Vierkantor changed the title ~~WIP: tactic analysis for calls to linarith that can become grind~~ WIP: tactic analysis for calls to linarith/omega/ring that can become grind Jul 28, 2025

Vierkantor added 3 commits July 29, 2025 16:42

Hook up ExtractGoal and MinImports to the tactic analysis framework

c4848ec

Cleanup for reviewing

e492706

Add a test file

d5181ad

Vierkantor changed the title ~~WIP: tactic analysis for calls to linarith/omega/ring that can become grind~~ feat: tactic analysis framework Aug 7, 2025

Vierkantor removed the WIP Work in progress label Aug 7, 2025

Vierkantor marked this pull request as ready for review August 7, 2025 16:06

Vierkantor added 3 commits August 13, 2025 10:26

Merge remote-tracking branch 'upstream/master' into t4t

ea42dde

Docstrings and mk_all

d4b1402

More docstrings

9392e74

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis/Declarations.lean Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis/Declarations.lean Show resolved Hide resolved

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis/Declarations.lean Outdated Show resolved Hide resolved

Documentation

e33f1e2

Vierkantor commented Aug 13, 2025

View reviewed changes

Mathlib/Tactic/ExtractGoal.lean Show resolved Hide resolved

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/TacticAnalysis/Declarations.lean Outdated Show resolved Hide resolved

Vierkantor and others added 6 commits August 13, 2025 16:47

More documentation improvements

6f3c11a

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Migrate to a new file

c3b3b2e

Split up into three passes

9ea16a1

Remove commented-out line

73e3a3e

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

Also report if 'grind' is slower than the original sequence

74116ee

Update Mathlib/Tactic/ExtractGoal.lean

b868f5d

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

kim-em reviewed Aug 13, 2025

View reviewed changes

Mathlib/Tactic/TacticAnalysis.lean Outdated Show resolved Hide resolved

Unnecessary import.

cb4af12

ghost added the ready-to-merge This PR has been sent to bors. label Aug 14, 2025

mathlib-bors bot changed the title ~~feat: tactic analysis framework~~ [Merged by Bors] - feat: tactic analysis framework Aug 15, 2025

mathlib-bors bot closed this Aug 15, 2025

Conversation

Vierkantor commented Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dac1d0caf8

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Jul 3, 2025

Uh oh!

Vierkantor commented Jul 8, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Vierkantor commented Jul 3, 2025 •

edited

Loading

github-actions bot commented Jul 3, 2025 •

edited

Loading