deprecate to -- a deprecation tool

Writing

deprecate to new_name new_name₂ ... new_nameₙ
theorem old_name : True := .intro

where new_name new_name₂ ... new_nameₙ is a sequence of identifiers produces the Try this suggestion:

theorem new_name : True := .intro

@[deprecated (since := "YYYY-MM-DD")] alias old_name := new_name

@[deprecated (since := "YYYY-MM-DD")] alias old_name₂ := new_name₂
...

@[deprecated (since := "YYYY-MM-DD")] alias old_nameₙ := new_nameₙ

where old_name old_name₂ ... old_nameₙ are the non-blacklisted declarations (auto)generated by the initial command.

TODO:

• the "new" names come fully qualified with their namespace -- if the deprecation is happening inside a namespace X, it would be better to remove the X prefix from them;
• preserve formatting of existing command?

def Mathlib.Tactic.DeprecateMe.mkDeprecationStx (id : Lean.TSyntax `ident) (n : Lean.Name) (dat : optParam (Option String) none) : Lean.Elab.Command.CommandElabM (Lean.TSyntax `command)

Produce the syntax for the command @[deprecated (since := "YYYY-MM-DD")] alias n := id.

Equations

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

def Mathlib.Tactic.DeprecateMe.newNames (old : Lean.Environment) (new : Lean.Environment) : Array Lean.Name

Returns the array of names that are in new but not in old.

Equations

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

def Mathlib.Tactic.DeprecateMe.renameTheorem (newName : Lean.TSyntax `ident) : Lean.TSyntax `command → Lean.TSyntax `Lean.Parser.Command.declId × Lean.TSyntax `command

If the input command is a theorem or a lemma, then it replaces the name of the resulting declaration with newName and it returns the old declaration name and the command with the new name.

If the input command is neither a theorem nor a lemma, then it returns .missing and the unchanged command.

Equations

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

def Mathlib.Tactic.DeprecateMe.commandDeprecate_to______ : Lean.ParserDescr

Writing

deprecate to new_name new_name₂ ... new_nameₙ
theorem old_name : True := .intro

where new_name new_name₂ ... new_nameₙ is a sequence of identifiers produces the Try this suggestion:

theorem new_name : True := .intro

@[deprecated (since := "YYYY-MM-DD")] alias old_name := new_name

@[deprecated (since := "YYYY-MM-DD")] alias old_name₂ := new_name₂
...

@[deprecated (since := "YYYY-MM-DD")] alias old_nameₙ := new_nameₙ

where old_name old_name₂ ... old_nameₙ are the non-blacklisted declarations (auto)generated by the initial command.

The "YYYY-MM-DD" entry is today's date and it is automatically filled in.

deprecate to makes an effort to match old_name, the "visible" name, with new_name, the first identifier produced by the user. The "old", autogenerated declarations old_name₂ ... old_nameₙ are retrieved in alphabetical order. In the case in which the initial declaration produces at most 1 non-blacklisted declarations besides itself, the alphabetical sorting is irrelevant.

Technically, the command also take an optional String argument to fill in the date in since. However, its use is mostly intended for debugging purposes, where having a variable date would make tests time-dependent.

Equations

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