# 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`.

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

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

source
@[reducible, inline]
abbrev Mathlib.Linter.Style.multiGoal.exclusions :
Std.HashSet Lean.SyntaxNodeKind

The `SyntaxNodeKind`s 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.

Instances For

source
@[reducible, inline]
abbrev Mathlib.Linter.Style.multiGoal.ignoreBranch :
Std.HashSet Lean.SyntaxNodeKind

The `SyntaxNodeKind`s 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.

Instances For

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

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

Instances For