Imports
/-
Copyright (c) 2026 Robert Sneiderman. All rights reserved.
Released under Apache 2.0 license.
Authors: Robert Sneiderman
-/
module
public import Physlib.Meta.Informal.Basic
public meta import Batteries.Tactic.Lint
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 defs 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.
@[expose] public meta section
The types of the declarations that syntax, notation and macro commands produce, along
with the pretty-printer declarations generated beside them. These hold parser data rather than
a mathematical definition, so their names are exempt from the naming convention.
def parserDeclTypes : List Name :=
[``Lean.ParserDescr, ``Lean.TrailingParserDescr, ``Lean.Parser.Parser,
``Lean.Parser.TrailingParser, ``Lean.PrettyPrinter.Parenthesizer,
``Lean.PrettyPrinter.Formatter]
The suffix Lean appends to the generated name of an anonymous instance to keep it unique
across projects, for example _physlib for a declaration of the Physlib project. This
mirrors Lean.Elab.Command.NameGen.mkBaseNameWithSuffix.
def projectSuffix (env : Environment) (declName : Name) : Option String := do
let idx ← env.getModuleIdxFor? declName
return "_" ++ env.header.moduleNames[idx]!.getRoot.toString.decapitalize
Whether the final component of declName ends in an underscore followed by a number, the
suffix Lean adds when the name it generated for an anonymous instance is already taken.
def hasNumericSuffix (declName : Name) : Bool :=
let parts := (declName.components.getLast?.getD .anonymous).toString.splitOn "_"
1 < parts.length && !parts.getLast!.isEmpty && parts.getLast!.all Char.isDigit
Whether the defsWithUnderscore linter should pass over declName.
def defsWithUnderscoreExempt (declName : Name) : CoreM Bool := do
let env ← getEnv
let some info := env.find? declName | return false
if let .const head _ := info.type.getAppFn then
if head == ``InformalDefinition || head == ``InformalLemma then return true
if parserDeclTypes.contains head then return true
if let some suffix := projectSuffix env declName then
if (declName.components.getLast?.getD .anonymous).toString.endsWith suffix then return true
return hasNumericSuffix declName
withDefsWithUnderscoreExemptions linter behaves like linter except that it passes over
the declarations selected by defsWithUnderscoreExempt.
def withDefsWithUnderscoreExemptions (linter : NamedLinter) : NamedLinter :=
{ linter with
test := fun declName => do
if ← defsWithUnderscoreExempt declName then return none else linter.test declName }