The "ppRoundtrip" linter

The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially from the pretty-printed version of itself.

opaque Mathlib.Linter.linter.ppRoundtrip : Lean.Option Bool

The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially from the pretty-printed version of itself.

The linter makes an effort to start the highlighting at the first difference. However, it may not always be successful. It also prints both the source code and the "expected code" in a 5-character radius from the first difference.

def Mathlib.Linter.polishPP (s : String) : String

polishPP s takes as input a String s, assuming that it is the output of pretty-printing a lean command. The main intent is to convert s to a reasonable candidate for a desirable source code format. The function first replaces consecutive whitespace sequences into a single space ( ), in an attempt to side-step line-break differences. After that, it applies some pre-emptive changes:

• doc-module beginnings tend to have some whitespace following them, so we add a space back in;
• name quotations such as ``Nat get pretty-printed as `` Nat, so we remove a space after double back-ticks, but take care of adding one more for triple (or more) back-ticks;
• notation3 is not followed by a pretty-printer space, so we add it here (https://github.com/leanprover-community/mathlib4/pull/15515).

def Mathlib.Linter.polishSource (s : String) : String × Array Nat

polishSource s is similar to polishPP s, but expects the input to be actual source code. For this reason, polishSource s performs more conservative changes: it only replace all whitespace starting from a linebreak (\n) with a single whitespace.

def Mathlib.Linter.posToShiftedPos (lths : Array Nat) (diff : Nat) : Nat

posToShiftedPos lths diff takes as input an array lths of natural numbers, and one further natural number diff. It adds up the elements of lths occupying the odd positions, as long as the sum of the elements in the even positions does not exceed diff. It returns the sum of the accumulated odds and diff. This is useful to figure out the difference between the output of polishSource s and s itself. It plays a role similar to the fileMap.

def Mathlib.Linter.zoomString (str : String) (centre offset : Nat) : Substring

zoomString str centre offset returns the substring of str consisting of the offset characters around the centreth character.

def Mathlib.Linter.capSourceInfo (s : Lean.SourceInfo) (p : Nat) : Lean.SourceInfo

capSourceInfo s p "shortens" all end-position information in the SourceInfo s to be at most p, trimming down also the relevant substrings.

partial def Mathlib.Linter.capSyntax (stx : Lean.Syntax) (p : Nat) : Lean.Syntax

capSyntax stx p applies capSourceInfo · s to all SourceInfos in all nodes, atoms and idents contained in stx.

This is used to trim away all "fluff" that follows a command: comments and whitespace after a command get removed with capSyntax stx stx.getTailPos?.get!.

def Mathlib.Linter.PPRoundtrip.ppRoundtrip : Lean.Linter

The "ppRoundtrip" linter emits a warning when the syntax of a command differs substantially from the pretty-printed version of itself.

The linter makes an effort to start the highlighting at the first difference. However, it may not always be successful. It also prints both the source code and the "expected code" in a 5-character radius from the first difference.