Documentation

Mathlib.Tactic.Linter.DeprecatedModule

The deprecated.module linter #

The deprecated.module linter emits a warning when a file that has been renamed or split is imported.

The usage is as follows. Write

import B
...
import Z

deprecated_module "Optional string here with further details" (since := "yyyy-mm-dd")

in module A with the expectation that A contains nothing else. This triggers the deprecated.module linter to notify every file with import A to instead import the direct imports of A, that is B, ..., Z.

source
opaque Mathlib.Linter.linter.deprecated.module :
Lean.Option Bool

The deprecated.module linter emits a warning when a file that has been renamed or split is imported. The default value is true, since this linter is designed to warn projects downstream of Mathlib of refactors and deprecations in Mathlib itself.

source
opaque Mathlib.Linter.deprecatedModuleExt :
Lean.SimplePersistentEnvExtension (Lean.Name × Array Lean.Name × Option String) (Std.HashSet (Lean.Name × Array Lean.Name × Option String))

Defines the deprecatedModuleExt extension for adding a HashSet of triples of

  • a module Name that has been deprecated and
  • an array of Names of modules that should be imported instead
  • an optional String containing further messages to be displayed with the deprecation

to the environment.

source
def Mathlib.Linter.deprecated_modules :
Lean.ParserDescr

deprecated_module "Optional string" (since := "yyyy-mm-dd") deprecates the current module A in favour of its direct imports. This means that any file that directly imports A will get a notification on the import A line suggesting to instead import the direct imports of A.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Linter.«command#show_deprecated_modules» :
    Lean.ParserDescr

    A utility command to show the current entries of the deprecatedModuleExt in the format:

    Deprecated modules

'MathlibTest.DeprecatedModule' deprecates to
#[Mathlib.Tactic.Linter.DocPrime, Mathlib.Tactic.Linter.DocString]
with message 'We can also give more details about the deprecation'

...
    Equations
    Instances For