The "multiGoal" linter

The "multiGoal" linter emits a warning where there is more than a single goal in scope. There is an exception: a tactic that closes all remaining goals is allowed.

There are a few tactics, such as skip, swap or the try combinator, that are intended to work specifically in such a situation. Otherwise, the mathlib style guide ask that goals be focused until there is only one active goal at a time. If this focusing does not happen, the linter emits a warning. Typically, the focusing is achieved by the cdot: ·, but, e.g., focus or on_goal x also serve a similar purpose.

TODO:

• Should the linter flag unnecessary scoping as well? For instance, should

  example : True := by
    · · exact .intro
  

  raise a warning?
• Custom support for "accumulating side-goals", so that once they are all in scope they can be solved in bulk via all_goals or a similar tactic.
• In development, on_goal has been partly used as a way of silencing the linter precisely to allow the accumulation referred to in the previous item. Maybe revisit usages of on_goal and also nested induction and cases.

opaque Mathlib.Linter.linter.style.multiGoal : Lean.Option Bool

The "multiGoal" linter emits a warning when there are multiple active goals.

@[reducible, inline]

abbrev Mathlib.Linter.Style.multiGoal.exclusions : Std.HashSet Lean.SyntaxNodeKind

The SyntaxNodeKinds in exclusions correspond to tactics that the linter allows, even though there are multiple active goals. Reasons for admitting a kind in exclusions include

• the tactic focuses on one goal, e.g. ·, focus, on_goal i =>, ...;
• the tactic is reordering the goals, e.g. swap, rotate_left, ...;
• the tactic is structuring a proof, e.g. skip, <;>, ...;
• the tactic is creating new goals, e.g. constructor, cases, induction, ....

There is some overlap in scope between ignoreBranch and exclusions.

Tactic combinators like repeat or try are a mix of both.

Equations

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

@[reducible, inline]

abbrev Mathlib.Linter.Style.multiGoal.ignoreBranch : Std.HashSet Lean.SyntaxNodeKind

The SyntaxNodeKinds in ignoreBranch correspond to tactics that disable the linter from their first application until the corresponding proof branch is closed. Reasons for ignoring these tactics include

• the linter gets confused by the proof management, e.g. conv;
• the tactics are intended to act on multiple goals, e.g. repeat, any_goals, all_goals, ...

There is some overlap in scope between exclusions and ignoreBranch.

Equations

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

partial def Mathlib.Linter.Style.multiGoal.getManyGoals : Lean.Elab.InfoTree → Array (Lean.Syntax × Nat × Nat × Nat)

getManyGoals t returns the syntax nodes of the InfoTree t corresponding to tactic calls which

• leave at least one goal that was present before it ran (with the exception of tactics that leave the sole goal unchanged);
• are not excluded through exclusions or ignoreBranch;

together with the number of goals before the tactic, the number of goals after the tactic, and the number of unaffected goals.

def Mathlib.Linter.Style.multiGoal.multiGoalLinter : Lean.Linter

The "multiGoal" linter emits a warning when there are multiple active goals.

Equations

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