# Tactic analysis framework #

In this file we define a framework for analyzing sequences of tactics. This can be used for linting (for instance: report when two `rw` calls can be merged into one), but it can also be run in a more batch-like mode to report larger potential refactors (for instance: report when a sequence of three or more tactics can be replaced with `grind`, without taking more heartbeats than the original proof did).

## Using the framework #

The framework runs, but does nothing by default (`set_option linter.tacticAnalysis false` to turn it off completely). Enable the analysis round `roundName` by enabling its corresponding option: `set_option linter.tacticAnalysis.roundName true`.

To add a round of analysis called `roundName`, declare an option `linter.tacticAnalysis.roundName`, make a definition of type `Mathlib.TacticAnalysis.Config` and give the `Config` declaration the `@[tacticAnalysis linter.tacticAnalysis.roundName]` attribute. Don't forget to enable the option.

## Warning #

The `ComplexConfig` interface doesn't feel quite intuitive and flexible yet and should be changed in the future. Please do not rely on this interface being stable.

source
opaque linter.tacticAnalysis :
Lean.Option Bool

The tactic analysis framework hooks into the linter to run analysis rounds on sequences of tactics. This can be used for linting, or in a more batch-like mode to report potential refactors.

source
structure Mathlib.TacticAnalysis.TacticNode :
Type

Information about a tactic in a sequence, parsed from infotrees and passed to a tactic analysis pass.

- ctxI : Lean.Elab.ContextInfo

  `ContextInfo` at the infotree node.

- tacI : Lean.Elab.TacticInfo

  `TacticInfo` at the infotree node.

- mayFail : Bool

  This tactic is allowed to fail because it is in a `try`/`anyGoals`/etc block.

Instances For

source
@[reducible, inline]
abbrev Mathlib.TacticAnalysis.TacticNode.runTacticCode (i : TacticNode) :
Lean.MVarId → Lean.Syntax → Lean.Elab.Command.CommandElabM (List Lean.MVarId)

Run tactic code, given by a piece of syntax, in the context of a tactic info node.

Convenience abbreviation for `ContextInfo.runTacticCode`.

Equations

- i.runTacticCode goal code = i.ctxI.runTacticCode i.tacI goal code

Instances For

source
structure Mathlib.TacticAnalysis.Config :
Type

Stores the configuration for a tactic analysis pass.

This provides the low-level interface into the tactic analysis framework.

- run : Array TacticNode → Lean.Elab.Command.CommandElabM Unit

  The function that runs this pass. Takes an array of infotree nodes corresponding to a sequence of tactics from the source file. Should do all reporting itself, for example by `Lean.Linter.logLint`.

Instances For

source
structure Mathlib.TacticAnalysis.Pass extends Mathlib.TacticAnalysis.Config :
Type

The internal representation of a tactic analysis pass, extending `Config` with some declaration meta-information.

- run : Array TacticNode → Lean.Elab.Command.CommandElabM Unit
- opt : Option (Lean.Option Bool)

  The option corresponding to this pass, used to enable it.

  Example: `linter.tacticAnalysis.grindReplacement`.

Instances For

source
structure Mathlib.TacticAnalysis.Entry :
Type

Each tactic analysis round is represented by the declaration name for the `Config`.

- declName : Lean.Name

  The declaration, of type `Config`, that defines this pass.

- optionName : Lean.Name

  The option, of type `Lean.Option Bool`, that controls whether the pass is enabled.

Instances For

source
def Mathlib.TacticAnalysis.Entry.import (e : Entry) :
Lean.ImportM Pass

Read a configuration from a declaration of the right type.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Mathlib.TacticAnalysis.instOrdEntry :
Ord Entry
Equations

- Mathlib.TacticAnalysis.instOrdEntry = { compare := fun (a b : Mathlib.TacticAnalysis.Entry) => compare (a.declName, a.optionName) (b.declName, b.optionName) }

source
opaque Mathlib.TacticAnalysis.tacticAnalysisExt :
Lean.PersistentEnvExtension Entry (Entry × Pass) (List Entry × Array Pass)

Environment extensions for `tacticAnalysis` declarations

source
def Mathlib.TacticAnalysis.findTacticSeqs (tree : Lean.Elab.InfoTree) :
Lean.Elab.Command.CommandElabM (Array (Array TacticNode))

Parse an infotree to find all the sequences of tactics contained within `stx`.

We consider a sequence here to be a maximal interval of tactics joined by `;` or newlines. This function returns an array of sequences. For example, a proof of the form:

    by
      tac1
      · tac2; tac3
      · tac4; tac5

would result in three sequences:

- `#[tac1, (· tac2; tac3), (· tac4; tac5)]`
- `#[tac2, tac3]`
- `#[tac4, tac5]`

Similarly, a declaration with multiple `by` blocks results in each of the blocks getting its own sequence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.TacticAnalysis.runPasses (configs : Array Pass) (trees : Lean.PersistentArray Lean.Elab.InfoTree) :
Lean.Elab.Command.CommandElabM Unit

Run the tactic analysis passes from `configs` on the tactic sequences in `stx`, using `trees` to get the infotrees.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.TacticAnalysis.tacticAnalysis :
Lean.Linter

A tactic analysis framework. It is aimed at allowing developers to specify refactoring patterns, which will be tested against a whole project, to report proposed changes.

It hooks into the linting system to move through the infotree, collecting tactic syntax and state to call the passes on.

Equations

- One or more equations did not get rendered due to their size.

Instances For

### Work in progress: `Config` building blocks #

In this section we define `ComplexConfig` which is supposed to make it easier to build standard analysis rounds.

Work in progress note: This interface does not feel intuitive yet and might be redesigned. Please do not rely on it being stable!

source
inductive Mathlib.TacticAnalysis.TriggerCondition (ctx : Type u_1) :
Type u_1

The condition is returned from the `.trigger` function to indicate which sublists of a tactic sequence to test.

The `context` field can be used to accumulate data between different invocations of `.trigger`.

- skip {ctx : Type u_1} : TriggerCondition ctx

  `skip` means that the current tactic and the ones before it will be discarded.

- continue {ctx : Type u_1} (context : ctx) : TriggerCondition ctx

  `continue` means to accumulate the current tactic, but not yet run the test on it.

- accept {ctx : Type u_1} (context : ctx) : TriggerCondition ctx

  `accept` means to run the test on the sequence of `.continue`s up to this `.accept`.

Instances For

source
instance Mathlib.TacticAnalysis.instBEqTriggerCondition {ctx✝ : Type u_1} [BEq ctx✝] :
BEq (TriggerCondition ctx✝)
Equations

- Mathlib.TacticAnalysis.instBEqTriggerCondition = { beq := Mathlib.TacticAnalysis.instBEqTriggerCondition.beq }

source
def Mathlib.TacticAnalysis.instBEqTriggerCondition.beq {ctx✝ : Type u_1} [BEq ctx✝] :
TriggerCondition ctx✝ → TriggerCondition ctx✝ → Bool
Equations

- Mathlib.TacticAnalysis.instBEqTriggerCondition.beq Mathlib.TacticAnalysis.TriggerCondition.skip Mathlib.TacticAnalysis.TriggerCondition.skip = true
- Mathlib.TacticAnalysis.instBEqTriggerCondition.beq (Mathlib.TacticAnalysis.TriggerCondition.continue a) (Mathlib.TacticAnalysis.TriggerCondition.continue b) = (a == b)
- Mathlib.TacticAnalysis.instBEqTriggerCondition.beq (Mathlib.TacticAnalysis.TriggerCondition.accept a) (Mathlib.TacticAnalysis.TriggerCondition.accept b) = (a == b)
- Mathlib.TacticAnalysis.instBEqTriggerCondition.beq x✝¹ x✝ = false

Instances For

source
structure Mathlib.TacticAnalysis.ComplexConfig :
Type 1

Specifies which analysis steps to take.

The overall design will have three user-supplied components:

- trigger on a piece of syntax (which could contain multiple tactic calls);
- test if a suggested change is indeed an improvement;
- tell the user where changes can be made.

- out : Type

  Type returned by the `.test` function.

- ctx : Type

  Type returned by the `.trigger` function.

- trigger (context : Option self.ctx) (currentTactic : Lean.Syntax) : TriggerCondition self.ctx

  Determines which (sequences of) tactics to analyze.

  `context` is `some ctx` whenever the previous trigger returned `continue ctx`, `none` at the start of a tactic sequence or after a `skip`/`accept`.

  If the last returned value is `continue` at the end of the sequence, the framework inserts an extra `done` to run the `trigger` on.

- test (ctxI : Lean.Elab.ContextInfo) (i : Lean.Elab.TacticInfo) (context : self.ctx) (goal : Lean.MVarId) : Lean.Elab.Command.CommandElabM self.out

  Code to run in the context of the tactic, for example an alternative tactic.

- tell (stx : Lean.Syntax) (originalSubgoals : List Lean.MVarId) (originalHeartbeats : Nat) (new : self.out) (newHeartbeats : Nat) : Lean.Elab.Command.CommandElabM (Option Lean.MessageData)

  Decides what to report to the user.

Instances For

source
def Mathlib.TacticAnalysis.testTacticSeq (config : ComplexConfig) (tacticSeq : Array (Lean.TSyntax `tactic)) (i : TacticNode) (ctx : config.ctx) :
Lean.Elab.Command.CommandElabM Unit

Test the `config` against a sequence of tactics, using the context info and tactic info from the start of the sequence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.TacticAnalysis.runPass (config : ComplexConfig) (seq : Array TacticNode) :
Lean.Elab.Command.CommandElabM Unit

Run the `config` against a sequence of tactics, using the `trigger` to determine which subsequences should be `test`ed.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.TacticAnalysis.Config.ofComplex (config : ComplexConfig) :
Config

Constructor for a `Config` which breaks the pass up into multiple pieces.

Equations

- Mathlib.TacticAnalysis.Config.ofComplex config = { run := Mathlib.TacticAnalysis.runPass config }

Instances For

source
opaque linter.tacticAnalysis.dummy :
Lean.Option Bool

A dummy option for testing the tactic analysis framework