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.

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.

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.

@[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.

@[reducible, inline]

abbrev Mathlib.TacticAnalysis.TacticNode.runTacticCodeCapturingInfoTree (i : TacticNode) : Lean.MVarId → Lean.Syntax → Lean.Elab.Command.CommandElabM (List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree)

Run tactic code, capturing InfoTrees for extracting "Try this:" suggestions.

Returns both the resulting goals and the InfoTrees produced during tactic execution. Use collectTryThisSuggestions from Mathlib.Lean.Elab.InfoTree to extract suggestions.

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.

structure Mathlib.TacticAnalysis.Passextends 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.

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.

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

Read a configuration from a declaration of the right type.

@[implicit_reducible]

instance Mathlib.TacticAnalysis.instOrdEntry : Ord Entry

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

Environment extensions for tacticAnalysis declarations

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.

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.

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.

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!

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 .continues up to this .accept.

@[implicit_reducible]

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

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

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 : ℕ) (new : self.out) (newHeartbeats : ℕ) : Lean.Elab.Command.CommandElabM (Option Lean.MessageData)

  Decides what to report to the user.

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.

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 tested.

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

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

opaque linter.tacticAnalysis.dummy : Lean.Option Bool

A dummy option for testing the tactic analysis framework