Physlib.Meta.Linters.DefsWithUnderscore
Physlib exemptions for the `defsWithUnderscore` linter
Mathlib's `defsWithUnderscore` environment linter reports every definition whose name contains an underscore. Four families of Physlib declaration trip it even though the offending name is either generated by Lean or belongs to a declaration that is not user-facing:
* `informal_definition` and `informal_lemma` elaborate to `def`s of type `InformalDefinition` and `InformalLemma`. They stand in for results that are not yet formalised, and they carry the snake_case name of the statement rather than of a definition. * `syntax`, `notation` and `macro` declarations, together with the parenthesizer and formatter that Lean generates beside them. Mathlib exempts the names Lean invents for these, but Physlib names many of them explicitly. * Anonymous instances whose generated name carries the suffix Lean appends to keep it unique across projects, `_physlib` for a declaration in `Physlib` and so on. Mathlib exempts its own `_mathlib` suffix in the same way. * Anonymous instances that Lean disambiguates with a trailing number. Mathlib exempts `_1` and `_2` but not `_3` and `_4`, which occur in `Physlib.Mathematics.DataStructures.FourTree.Basic`.
`withDefsWithUnderscoreExemptions` wraps the linter so that these pass; every other declaration is reported as before.
5 declarations
Types of parser and pretty-printer declarations
The list `Physlib.parserDeclTypes` consists of the internal Lean names representing types generated by `syntax`, `notation`, and `macro` commands, as well as their corresponding pretty-printer declarations. These types include: - `Lean.ParserDescr` - `Lean.TrailingParserDescr` - `Lean.Parser.Parser` - `Lean.Parser.TrailingParser` - `Lean.PrettyPrinter.Parenthesizer` - `Lean.PrettyPrinter.Formatter` These represent declarations used for storing parser metadata and formatting instructions rather than mathematical definitions.
Project-specific suffix for a declaration name
Given a Lean environment and a declaration name , this function identifies the project to which the declaration belongs and returns its associated suffix as an optional string. The suffix is constructed by taking the root name of the module containing (for example, "Physlib"), converting it to lowercase, and prepending an underscore (resulting in, e.g., `"_physlib"`). This is used to identify the project-specific strings that Lean appends to anonymous instances.
Detection of numeric suffixes in `declName`
The function `hasNumericSuffix` checks whether the final component of a declaration name `declName` ends with an underscore followed by a sequence of digits. Specifically, it returns true if the string representation of the last component of the name contains an underscore and the substring after the last underscore consists entirely of digits (e.g., as in `name_1` or `instance_42`).
Exemption criteria for the `defsWithUnderscore` linter
The function `defsWithUnderscoreExempt` determines whether a given declaration name should be exempted from the `defsWithUnderscore` linter. It returns `true` if the declaration meets any of the following criteria: 1. The declaration is defined as an `InformalDefinition` or an `InformalLemma` (placeholder for non-formalized results). 2. The declaration's type is categorized as a parser or pretty-printer internal type (e.g., `Lean.ParserDescr`). 3. The name of the declaration ends with a project-specific suffix, such as `_physlib`, which is commonly appended by Lean to anonymous instances. 4. The name ends with a numeric suffix (e.g., `_1` or `_42`) used for disambiguation. Otherwise, the function returns `false`.
Linter wrapper with underscore exemptions
The function `withDefsWithUnderscoreExemptions` takes a linter (of type `NamedLinter`) and returns a modified linter that suppresses reporting for specific declarations. For any declaration name , the new linter returns no error if meets the exemption criteria defined by `defsWithUnderscoreExempt`. Otherwise, it returns the result of the original linter test . The exempted declarations include informal definitions, internal syntax/parser declarations, and names with project-specific suffixes (like `_physlib`) or numeric disambiguators.