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.

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.

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.

def Mathlib.Linter.addModuleDeprecation {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadQuotation m] (msg? : Option String) : m Unit

addModuleDeprecation adds to the deprecatedModuleExt extension the pair consisting of the current module name and the array of its direct imports.

It ignores the Init import, since this is a special module that is expected to be imported by all files.

It also ignores the Mathlib.Tactic.Linter.DeprecatedModule import (namely, the current file), since there is no need to import this module.

Equations

• One or more equations did not get rendered due to their size.

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.

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

• Mathlib.Linter.«command#show_deprecated_modules» = Lean.ParserDescr.node `Mathlib.Linter.«command#show_deprecated_modules» 1024 (Lean.ParserDescr.symbol "#show_deprecated_modules")

opaque Mathlib.Linter.DeprecatedModule.IsLaterCommand : IO.Ref Bool

IsLaterCommand is an IO.Ref that starts out being false. As soon as a (non-import) command in a file is processed, the deprecated.module lintersets it totrue. If it is false, then the deprecated.module` linter will check for deprecated modules.

This is used to ensure that the linter performs the deprecation checks only once per file. There are possible concurrency issues, but they should not be particularly worrying:

• the linter check should be relatively quick;
• the only way in which the linter could change what it reports is if the imports are changed and a change in imports triggers a rebuild of the whole file anyway, resetting the IO.Ref.

def Mathlib.Linter.DeprecatedModule.deprecated.moduleLinter : Lean.Linter

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.

Equations

• One or more equations did not get rendered due to their size.