Private module linter

This linter lints against nonempty modules that have only private declarations, and suggests adding @[expose] public section to the top or selectively marking declarations as public.

Implementation notes

env.constants.map₂ contains all locally-defined constants, and accessing this waits until all declarations are added. By linting (only) the eoi token, we can capture all constants defined in the file.

Note that private declarations from the current module are exactly those which satisfy isPrivateName, whether private due to an explicit private or due to not being made public.

We also do not count declarations which satisfy isReservedName as public declarations from the current module. While they might indeed be public, the declarations associated with reserved names are generated automatically and lazily, sometimes in downstream modules from the one in which the name was reserved.

For example, Lean might reserve the name foo.eq_1 in one module, but only add a declaration with the name foo.eq_1 to the environment in some downstream module, when Lean attempts to realize the name. If the original module is a public import of the downstream module, then this new declaration foo.eq_1 will be added to the public scope, as it would be if it had been declared in the original module.

As such, if e.g. simp realized the public declaration foo.eq_1 in some module M.Bar downstream of the module in which foo was declared, but M.Bar did not add any other public declarations, the linter should still fire on M.Bar. Ignoring reserved names ensures this.

See also the type Lean.ReservedNameAction, invocations of registerReservedNameAction and registerReservedNamePredicate for examples, and the module Lean.ResolveName for further insight.

Note that metaprograms should not add public declarations when run in private scopes. Doing so would likely be a bug in the metaprogram. As such, we do not perform further checks for automatically generated declarations such as those in isAutoDecl.

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

The privateModule linter lints against nonempty modules that have only private declarations, and suggests adding @[expose] public section or selectively marking declarations as public.