The commandStart linter

The commandStart linter emits a warning if

• either a command does not start at the beginning of a line;
• or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

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

The commandStart linter emits a warning if

• either a command does not start at the beginning of a line;
• or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

In practice, this makes sure that the spacing in a typical declaration looks like

example (a : Nat) {R : Type} [Add R] : <not linted part>

as opposed to

example (a: Nat) {R:Type}  [Add  R] : <not linted part>

opaque Mathlib.Linter.linter.style.commandStart.verbose : Lean.Option Bool

If the linter.style.commandStart.verbose option is true, the commandStart linter reports some helpful diagnostic information.

def Mathlib.Linter.CommandStart.endPos (stx : Lean.Syntax) : Option String.Pos

CommandStart.endPos stx returns the position up until the commandStart linter checks the formatting. This is every declaration until the type-specification, if there is one, or the value, as well as all variable commands.

Equations

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

structure Mathlib.Linter.FormatError : Type

A FormatError is the main structure tracking how some surface syntax differs from its pretty-printed version.

In case of deviations, it contains the deviation's location within an ambient string.

• srcNat : Nat

  The distance to the end of the source string, as number of characters

• srcEndPos : String.Pos

  The distance to the end of the source string, as number of string positions

• fmtPos : Nat

  The distance to the end of the formatted string, as number of characters

• msg : String

  The kind of formatting error. For example: extra space, remove line break or missing space.

  Strings starting with Oh no indicate an internal error.

• length : Nat

  The length of the mismatch, as number of characters.

• srcStartPos : String.Pos

  The starting position of the mismatch, as a String.pos.

def Mathlib.Linter.instInhabitedFormatError.default : FormatError

Equations

• Mathlib.Linter.instInhabitedFormatError.default = { srcNat := default, srcEndPos := default, fmtPos := default, msg := default, length := default, srcStartPos := default }

instance Mathlib.Linter.instInhabitedFormatError : Inhabited FormatError

Equations

• Mathlib.Linter.instInhabitedFormatError = { default := Mathlib.Linter.instInhabitedFormatError.default }

instance Mathlib.Linter.instToStringFormatError : ToString FormatError

Equations

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

def Mathlib.Linter.mkFormatError (ls ms msg : String) (length : Nat := 1) : FormatError

Produces a FormatError from the input data. It expects

• ls to be a "user-typed" string;
• ms to be a "pretty-printed" string;
• msg to be a custom error message, such as extra space or remove line break;
• length (optional with default 1), how many characters the error spans.

In particular, it extracts the position information within the string, both as number of characters and as String.Pos.

Equations

• Mathlib.Linter.mkFormatError ls ms msg length = { srcNat := ls.length, srcEndPos := ls.endPos, fmtPos := ms.length, msg := msg, length := length, srcStartPos := ls.endPos }

def Mathlib.Linter.pushFormatError (fs : Array FormatError) (f : FormatError) : Array FormatError

Add a new FormatError f to the array fs, trying, as much as possible, to merge the new FormatError with the last entry of fs.

Equations

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

partial def Mathlib.Linter.parallelScanAux (as : Array FormatError) (L M : String) : Array FormatError

Scan the two input strings L and M, assuming M is the pretty-printed version of L. This almost means that L and M only differ in whitespace.

While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid flagging some line-breaking changes. (The pretty-printer does not always produce desirably formatted code.)

def Mathlib.Linter.parallelScan (src fmt : String) : Array FormatError

Scan the two input strings L and M, assuming M is the pretty-printed version of L. This almost means that L and M only differ in whitespace.

While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid flagging some line-breaking changes. (The pretty-printer does not always produce desirably formatted code.)

Equations

• Mathlib.Linter.parallelScan src fmt = Mathlib.Linter.parallelScanAux ∅ src fmt

@[reducible, inline]

abbrev Mathlib.Linter.Style.CommandStart.unlintedNodes : Array Lean.Name

unlintedNodes contains the SyntaxNodeKinds for which there is no clear formatting preference: if they appear in surface syntax, the linter will ignore formatting.

Currently, the unlined nodes are mostly related to Subtype, Set and Finset notation and list notation.

Equations

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

@[irreducible]

def Mathlib.Linter.Style.CommandStart.getUnlintedRanges (a : Array Lean.SyntaxNodeKind) : Std.HashSet String.Range → Lean.Syntax → Std.HashSet String.Range

Given an array a of SyntaxNodeKinds, we accumulate the ranges of the syntax nodes of the input syntax whose kind is in a.

The linter uses this information to avoid emitting a warning for nodes with kind contained in unlintedNodes.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Linter.Style.CommandStart.getUnlintedRanges a x✝ (Lean.Syntax.atom info "where") = match Lean.SourceInfo.getRangeWithTrailing? false info with | some trail => x✝.insert trail | x => x✝
• Mathlib.Linter.Style.CommandStart.getUnlintedRanges a x✝¹ x✝ = x✝¹

def Mathlib.Linter.Style.CommandStart.isOutside (rgs : Std.HashSet String.Range) (rg : String.Range) : Bool

Given a HashSet of String.Ranges rgs and a further String.Range rg, isOutside rgs rg returns false if and only if rgs contains a range that completely contains rg.

The linter uses this to figure out which nodes should be ignored.

Equations

• Mathlib.Linter.Style.CommandStart.isOutside rgs rg = rgs.all fun (x : String.Range) => match x with | { start := a, stop := b } => !(decide (a ≤ rg.start) && decide (rg.stop ≤ b))

def Mathlib.Linter.Style.CommandStart.mkWindow (orig : String) (start ctx : Nat) : String

mkWindow orig start ctx extracts from orig a string that starts at the first non-whitespace character before start, then expands to cover ctx more characters and continues still until the first non-whitespace character.

In essence, it extracts the substring of orig that begins at start, continues for ctx characters plus expands left and right until it encounters the first whitespace character, to avoid cutting into "words".

Note. start is the number of characters from the right where our focus is!

Equations

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

def Mathlib.Linter.Style.CommandStart.commandStartLinter : Lean.Linter

The commandStart linter emits a warning if

• either a command does not start at the beginning of a line;
• or the "hypotheses segment" of a declaration does not coincide with its pretty-printed version.

In practice, this makes sure that the spacing in a typical declaration looks like

example (a : Nat) {R : Type} [Add R] : <not linted part>

as opposed to

example (a: Nat) {R:Type}  [Add  R] : <not linted part>

Equations

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