Fugue style linters — shared infrastructure

linter.fugue.* is the project's family of style linters: one per mechanically-checkable rule in LEAN_STYLE.md and INSTRUCTIONS.md. Each is a Lean.Linter that runs at command elaboration and reports through Linter.logLint, so every diagnostic is a warning and style never fails a build.

This module carries what the linters share:

• Finding — a syntax node to underline and the message to show;
• mkFugueLinter / mkFugueLinterM — the wrapper turning a finding-producer into a Linter.run body, gated on the master toggle, the per-linter option, and the vendored-code skiplist;
• linter.fugue — the master toggle every wrapper checks;
• skiplist — module-path prefixes exempt from every linter.fugue.* linter;
• scan — a pre-order syntax walk that does not descend into syntax quotations.

opaque CustomPrelude.Linter.linter.fugue : Lean.Option Bool

The master switch for the project's style linters. While this is off every linter.fugue.* linter stays silent regardless of its own option, so set_option linter.fugue false in … turns the whole family off for one command.

structure CustomPrelude.Linter.Finding : Type

One linter finding: the syntax node to underline and the message to show.

• ref : Lean.Syntax

  The syntax node the warning is anchored at.

• msg : Lean.MessageData

  The warning text.

def CustomPrelude.Linter.skiplist : Array Lean.Name

Module-path prefixes exempt from every linter.fugue.* linter: vendored upstream code (keeps upstream style) and the linter sources themselves (which necessarily name the constructs they detect — linter.fugue.comments would flag its own rule list). Tests.Linter.* is not here — those fixtures must be linted for #guard_msgs to capture the warning.

Equations

• CustomPrelude.Linter.skiplist = #[`Extra.Mathlib, `CustomPrelude.Linter]

def CustomPrelude.Linter.isSkipped (mod : Lean.Name) : Bool

Whether mod sits under a skiplist prefix.

Equations

• CustomPrelude.Linter.isSkipped mod = CustomPrelude.Linter.skiplist.any fun (x : Lean.Name) => x.isPrefixOf mod

def CustomPrelude.Linter.isQuotationKind (k : Lean.SyntaxNodeKind) : Bool

Syntax-node kinds whose interior is a pattern being constructed, not proof text: a syntax quotation. A syntax linter stops descending here — the rule it enforces holds in metaprogramming code, not inside the quotations that code writes.

Equations

• CustomPrelude.Linter.isQuotationKind (pre.str "quot") = (true || pre.str "quot" == `Lean.Parser.Term.dynamicQuot || pre.str "quot" == `Lean.Parser.Tactic.quotSeq)
• CustomPrelude.Linter.isQuotationKind k = (false || k == `Lean.Parser.Term.dynamicQuot || k == `Lean.Parser.Tactic.quotSeq)

partial def CustomPrelude.Linter.scanExcept (skip : Lean.SyntaxNodeKind → Bool) (f : Lean.Syntax → Array Finding) (stx : Lean.Syntax) : Array Finding

Pre-order walk of stx, collecting f's findings at every node, without descending into syntax quotations (isQuotationKind) or any node whose kind skip accepts.

def CustomPrelude.Linter.scan (f : Lean.Syntax → Array Finding) (stx : Lean.Syntax) : Array Finding

scanExcept with no extra skip: the plain quotation-aware pre-order walk.

Equations

• CustomPrelude.Linter.scan f stx = CustomPrelude.Linter.scanExcept (fun (x : Lean.SyntaxNodeKind) => false) f stx

def CustomPrelude.Linter.hit (ref : Lean.Syntax) (msg : Lean.MessageData) : Array Finding

A one-node finding helper: #[⟨ref, msg⟩].

Equations

• CustomPrelude.Linter.hit ref msg = #[{ ref := ref, msg := msg }]

partial def CustomPrelude.Linter.collect (p : Lean.Syntax → Bool) (stx : Lean.Syntax) : Array Lean.Syntax

Every node under stx (pre-order) satisfying p, without descending into syntax quotations (isQuotationKind).

def CustomPrelude.Linter.identLast? : Lean.Syntax → Option String

The last component of an identifier's name, macro scopes erased; none for a non-identifier.

Equations

• CustomPrelude.Linter.identLast? (Lean.Syntax.ident info rawVal n preresolved) = match n.eraseMacroScopes with | pre.str s => some s | x => none
• CustomPrelude.Linter.identLast? x✝ = none

def CustomPrelude.Linter.nameHasComponent (n : Lean.Name) (s : String) : Bool

Whether some component of n (macro scopes erased) equals s.

Equations

• CustomPrelude.Linter.nameHasComponent n s = n.eraseMacroScopes.components.any fun (c : Lean.Name) => match c with | pre.str x => x == s | x => false

def CustomPrelude.Linter.crossesLine (stx : Lean.Syntax) : Bool

Whether the whitespace after stx (its trailing trivia, else the head token's) spans a line break — i.e. whatever follows stx in the source starts on a later line.

Equations

• CustomPrelude.Linter.crossesLine stx = match stx.getTrailing? with | some ss => ss.toString.any fun (x : Char) => x == '\n' | none => false

def CustomPrelude.Linter.identsUnder (stx : Lean.Syntax) : Array String

Every identifier last-component appearing anywhere under stx (quotations excepted).

Equations

• CustomPrelude.Linter.identsUnder stx = Array.filterMap CustomPrelude.Linter.identLast? (CustomPrelude.Linter.collect (fun (x : Lean.Syntax) => x.isIdent) stx)

def CustomPrelude.Linter.locationHyps (stx : Lean.Syntax) : Array String

The at <hyp> names a tactic with a trailing Tactic.location carries; #[] for none.

Equations

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

def CustomPrelude.Linter.appArgs (s : Lean.Syntax) : Array Lean.Syntax

The direct arguments of an application s (Term.app), each unwrapped through one layer of (…). #[] when s is not an application.

Equations

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

def CustomPrelude.Linter.isSetOption (opt val : String) (s : Lean.Syntax) : Bool

Whether s is a set_option <opt> <val> — command form or tactic form — for the given option-name last component and value atom.

Equations

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

partial def CustomPrelude.Linter.seqTactics (stx : Lean.Syntax) : Array Lean.Syntax

The tactics of a tacticSeq / tacticSeq1Indented / bracketed sequence, in source order. #[] for any other node.

def CustomPrelude.Linter.selectorBody? (s : Lean.Syntax) : Option Lean.Syntax

The tactic body a goal selector applies, if s is one: the project's tac_selector (all: / n,m: / n-m:), all_goals, or any_goals. none for anything else.

Equations

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

def CustomPrelude.Linter.firstOrSolveAlts? (s : Lean.Syntax) : Option Nat

first / solve alternative-count, none if s is neither.

Equations

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

partial def CustomPrelude.Linter.unwrapTac (s : Lean.Syntax) : Lean.Syntax

Strip one layer of ( … ) / { … } tactic grouping, and a single-tactic sequence, from s.

def CustomPrelude.Linter.sameShape (a b : Lean.Syntax) : Bool

Structural equality ignoring source positions (compares the reprinted text).

Equations

• CustomPrelude.Linter.sameShape a b = match a.reprint, b.reprint with | some x, some y => x.trimAscii == y.trimAscii | x, x_1 => false

def CustomPrelude.Linter.allDistinctShape (xs : Array Lean.Syntax) : Bool

Whether every pair in xs is sameShape-distinct.

Equations

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

def CustomPrelude.Linter.mkFugueLinterM (opt : Lean.Option Bool) (core : Lean.Syntax → Lean.Elab.Command.CommandElabM (Array Finding)) : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit

Turn a monadic finding-producer into a Linter.run body.

The wrapper:

• honours set_option … in at command scope, through withSetOptionIn;
• stays silent unless both the master linter.fugue and opt are enabled;
• stays silent on modules under skiplist;
• stays silent while the command still has elaboration errors — style stays out of the way of a proof the compiler is still rejecting;
• emits one Linter.logLint opt per finding, anchored at Finding.ref.

Equations

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

def CustomPrelude.Linter.mkFugueLinter (opt : Lean.Option Bool) (core : Lean.Syntax → Array Finding) : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit

mkFugueLinterM for a pure Syntax-only core — the syntax-linter kind.

Equations

• CustomPrelude.Linter.mkFugueLinter opt core = CustomPrelude.Linter.mkFugueLinterM opt fun (stx : Lean.Syntax) => pure (core stx)