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.removeRanges (file : String) (rgs : Array Lean.Syntax.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.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.«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.