The #clear_deprecations command

This file defines the #clear_deprecations date₁ date₂ really command.

This function is intended for automated use by the remove_deprecations automation. It removes declarations that have been deprecated in the time range starting from date₁ and ending with date₂.

See the doc-string for the command for more information.

def Mathlib.Tactic.instToStringRange_mathlib : ToString String.Range

A convenience instance to print a String.Range as the corresponding pair of String.Pos.

Equations

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

def Mathlib.Tactic.repos : Lean.NameSet

These are the names of the directories containing all the files that should be inspected. For reporting, the script assumes there is no sub-dir of the repo dir that contains repo as a substring. However, the script should still remove old deprecations correctly even if that happens.

Equations

• Mathlib.Tactic.repos = Lean.NameSet.ofArray #[`Mathlib, `Archive, `Counterexamples]

structure Mathlib.Tactic.DeprecationInfo : Type

The main structure containing the information a deprecated declaration.

• module is the name of the module containing the deprecated declaration;
• decl is the name of the deprecated declaration;
• rgStart is the Position where the deprecated declaration starts;
• rgStop is the Position where the deprecated declaration ends;
• since is the date when the declaration was deprecated.

• module : Lean.Name

  module is the name of the module containing the deprecated declaration.

• decl : Lean.Name

  decl is the name of the deprecated declaration.

• rgStart : Lean.Position

  rgStart is the Position where the deprecated declaration starts.

• rgStop : Lean.Position

  rgStop is the Position where the deprecated declaration ends.

• since : String

  since is the date when the declaration was deprecated.

def Mathlib.Tactic.getPosAfterImports (fname : String) : Lean.Elab.Command.CommandElabM String.Pos.Raw

getPosAfterImports fname parses the imports of fname and returns the position just after them.

This position is after all trailing whitespace and comments that may follow the imports of fname.

Equations

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

def Mathlib.Tactic.addAfterImports (fname s : String) : Lean.Elab.Command.CommandElabM String

addAfterImports fname s returns the content of the file fname, with the string s added after the imports of fname.

Equations

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

def Mathlib.Tactic.getDeprecatedInfo (nm : Lean.Name) (verbose? : Bool) : Lean.Elab.Command.CommandElabM (Option DeprecationInfo)

If nm is the name of a declaration, then getDeprecatedInfo nm returns the DeprecationInfo data for nm. Otherwise, it returns none.

If the verbose? input is true, then the command also summarizes what the data is.

Equations

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

def Mathlib.Tactic.deprecatedHashMap (oldDate newDate : String) : Lean.Elab.Command.CommandElabM (Std.HashMap (Lean.Name × String) (Array (Lean.Name × String.Range)))

The output is the HashMap whose keys are the names of the files containing deprecated declarations, and whose values are the arrays of ranges corresponding to the deprecated declarations in that file. The input oldDate and newDate are strings of the form "YYYY-MM-DD". The output contains all the declarations that were deprecated after oldDate and before newDate.

Equations

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

def Mathlib.Tactic.removeRanges (file : String) (rgs : Array String.Range) : String

removeRanges file rgs removes from the string file the substrings whose ranges are in the array rgs.

Notes.

• The command makes the assumption that rgs is sorted.
• The command removes all consecutive whitespace following the end of each range.

Equations

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

def Mathlib.Tactic.removeDeprecations (fname : String) (rgs : Array String.Range) : IO String

removeDeprecations fname rgs reads the content of fname and removes from it the substrings whose ranges are in the array rgs.

The command makes the assumption that rgs is sorted.

Equations

• Mathlib.Tactic.removeDeprecations fname rgs = do let __do_lift ← IO.FS.readFile { toString := fname } pure (Mathlib.Tactic.removeRanges __do_lift rgs)

def Mathlib.Tactic.parseLine (line : String) : Option (List String.Pos.Raw)

parseLine line assumes that the input string is of the form

info: File/Path.lean:12:0: [362, 398, 399]

and extracts [362, 398, 399]. It makes the assumption that there is a unique : [ substring and then retrieves the numbers.

Note that this is the output of Mathlib.Linter.CommandRanges.commandRangesLinter that the script here is parsing.

Equations

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

def Mathlib.Tactic.rewriteOneFile (fname : String) (rgs : Array (Lean.Name × String.Range)) : Lean.Elab.Command.CommandElabM (String × String)

Takes as input a file path fname and an array of pairs (declName, range of declaration). The declName is mostly for printing information, but is not used essentially by the function.

It returns the pair (temp file name, file without the commands that generated the declarations).

In the course of doing so, the function creates a temporary file from fname, by

• adding the import Mathlib.Tactic.Linter.CommandRanges and
• setting the linter.commandRanges option to true.

It parses the temporary file, capturing the output and uses the command ranges to remove the ranges of the commands that generated the passed declaration ranges.

Equations

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

def Mathlib.Tactic.importLT (env : Lean.Environment) (f1 f2 : Lean.Name) : Bool

The < partial order on modules: importLT env mod₁ mod₂ means that mod₂ imports mod₁.

Equations

• Mathlib.Tactic.importLT env f1 f2 = (env.findRedundantImports #[f1, f2]).contains f1

def Mathlib.Tactic.«command#clear_deprecations___Really» : Lean.ParserDescr

#clear_deprecations "YYYY₁-MM₁-DD₁" "YYYY₂-MM₂-DD₂" really computes the declarations that have the @[deprecated] attribute and the since field satisfies YYYY₁-MM₁-DD₁ ≤ since ≤ YYYY₂-MM₂-DD₂. For each one of them, it retrieves the command that generated it and removes it. It also verbosely logs various steps of the computation.

Running #clear_deprecations "YYYY₁-MM₁-DD₁" "YYYY₂-MM₂-DD₂", without the trailing really skips the removal, but still emits the same verbose output.

This function is intended for automated use by the remove_deprecations automation.

Equations

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