Documentation

Mathlib.Tactic.Linter.Style

Style linters #

This file contain linters about stylistic aspects: these are only about coding style, but do not affect correctness nor global coherence of mathlib. Historically, some of these were ported from the lint-style.py Python script.

This file defines the following linters:

All of these linters are enabled in mathlib by default, but disabled globally since they enforce conventions which are inherently subjective.

The setOption linter emits a warning on a set_option command, term or tactic which sets a pp, profiler or trace option. It also warns on an option containing maxHeartbeats (as these should be scoped as set_option ... in instead).

Whether a syntax element is a set_option command, tactic or term: Return the name of the option being set, if any.

Equations
    Instances For
      @[deprecated Mathlib.Linter.Style.setOption.parseSetOption (since := "2024-12-07")]

      Deprecated alias for Mathlib.Linter.Style.setOption.parseSetOption.

      Equations
        Instances For

          Whether a given piece of syntax is a set_option command, tactic or term.

          Equations
            Instances For
              @[deprecated Mathlib.Linter.Style.setOption.isSetOption (since := "2024-12-07")]

              Deprecated alias for Mathlib.Linter.Style.setOption.isSetOption.

              Equations
                Instances For

                  The setOption linter: this lints any set_option command, term or tactic which sets a debug, pp, profiler or trace option. This also warns if an option containing maxHeartbeats (typically, the maxHeartbeats or synthInstance.maxHeartbeats option) is set.

                  Why is this bad? The debug, pp, profiler and trace options are good for debugging, but should not be used in production code.

                  maxHeartbeats options should be scoped as set_option opt in ... (and be followed by a comment explaining the need for them; another linter enforces this).

                  How to fix this? The maxHeartbeats options can be scoped to individual commands, if they are truly necessary.

                  The debug, pp, profiler and trace are usually not necessary for production code, so you can simply remove them. (Some tests will intentionally use one of these options; in this case, simply allow the linter.)

                  Equations
                    Instances For

                      The "missing end" linter #

                      The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

                      The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

                      The "missing end" linter emits a warning on non-closed sections and namespaces. It allows the "outermost" noncomputable section to be left open (whether or not it is named).

                      Equations
                        Instances For

                          The cdot linter #

                          The cdot linter is a syntax-linter that flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter. It also flags "isolated cdots", i.e. when the · is on its own line.

                          The cdot linter flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter. It also flags "isolated cdots", i.e. when the · is on its own line.

                          isCDot? stx checks whether stx is a Syntax node corresponding to a cdot typed with the character ·.

                          Equations
                            Instances For

                              findCDot stx extracts from stx the syntax nodes of kind Lean.Parser.Term.cdot or cdotTk.

                              unwanted_cdot stx returns an array of syntax atoms within stx corresponding to cdots that are not written with the character ·. This is precisely what the cdot linter flags.

                              Equations
                                Instances For

                                  The cdot linter flags uses of the "cdot" · that are achieved by typing a character different from ·. For instance, a "plain" dot . is allowed syntax, but is flagged by the linter. It also flags "isolated cdots", i.e. when the · is on its own line.

                                  Equations
                                    Instances For

                                      The dollarSyntax linter #

                                      The dollarSyntax linter flags uses of <| that are achieved by typing $. These are disallowed by the mathlib style guide, as using <| pairs better with |>.

                                      The dollarSyntax linter flags uses of <| that are achieved by typing $. These are disallowed by the mathlib style guide, as using <| pairs better with |>.

                                      findDollarSyntax stx extracts from stx the syntax nodes of kind $.

                                      The dollarSyntax linter flags uses of <| that are achieved by typing $. These are disallowed by the mathlib style guide, as using <| pairs better with |>.

                                      Equations
                                        Instances For

                                          The lambdaSyntax linter #

                                          The lambdaSyntax linter is a syntax linter that flags uses of the symbol λ to define anonymous functions, as opposed to the fun keyword. These are syntactically equivalent; mathlib style prefers the latter as it is considered more readable.

                                          The lambdaSyntax linter flags uses of the symbol λ to define anonymous functions. This is syntactically equivalent to the fun keyword; mathlib style prefers using the latter.

                                          findLambdaSyntax stx extracts from stx all syntax nodes of kind Term.fun.

                                          The lambdaSyntax linter flags uses of the symbol λ to define anonymous functions. This is syntactically equivalent to the fun keyword; mathlib style prefers using the latter.

                                          Equations
                                            Instances For

                                              The "longFile" linter #

                                              The "longFile" linter emits a warning on files which are longer than a certain number of lines (1500 by default).

                                              The "longFile" linter emits a warning on files which are longer than a certain number of lines (linter.style.longFileDefValue by default on mathlib, no limit for downstream projects). If this option is set to N lines, the linter warns once a file has more than N lines. A value of 0 silences the linter entirely.

                                              The number of lines that the longFile linter considers the default.

                                              The "longFile" linter emits a warning on files which are longer than a certain number of lines (linter.style.longFileDefValue by default on mathlib, no limit for downstream projects). If this option is set to N lines, the linter warns once a file has more than N lines. A value of 0 silences the linter entirely.

                                              Equations
                                                Instances For

                                                  The "longLine linter" #

                                                  The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

                                                  The "longLine" linter emits a warning on lines longer than 100 characters. We allow lines containing URLs to be longer, though.

                                                  Equations
                                                    Instances For

                                                      The nameCheck linter emits a warning on declarations whose name is non-standard style. (Currently, this only includes declarations whose name includes a double underscore.)

                                                      Why is this bad? Double underscores in theorem names can be considered non-standard style and probably have been introduced by accident. How to fix this? Use single underscores to separate parts of a name, following standard naming conventions.

                                                      The nameCheck linter emits a warning on declarations whose name is non-standard style. (Currently, this only includes declarations whose name includes a double underscore.)

                                                      Why is this bad? Double underscores in theorem names can be considered non-standard style and probably have been introduced by accident. How to fix this? Use single underscores to separate parts of a name, following standard naming conventions.

                                                      Equations
                                                        Instances For

                                                          The "openClassical" linter #

                                                          The "openClassical" linter emits a warning on open Classical statements which are not scoped to a single declaration. A non-scoped open Classical can hide that some theorem statements would be better stated with explicit decidability statements.

                                                          If stx is syntax describing an open command, extractOpenNames stx returns an array of the syntax corresponding to the opened names, omitting any renamed or hidden items.

                                                          This only checks independent open commands: for open ... in ... commands, this linter returns an empty array.

                                                          Equations
                                                            Instances For

                                                              The "openClassical" linter emits a warning on open Classical statements which are not scoped to a single declaration. A non-scoped open Classical can hide that some theorem statements would be better stated with explicit decidability statements.

                                                              Equations
                                                                Instances For