machineApplicableDeprecated tag attribute

Stream: lean4

[Richard Copley]

The comment at the head of Std.CodeAction.Deprecated says

Code action for @[deprecated] replacements

This is an opt-in mechanism for making machine-applicable @[deprecated] definitions. When enabled
(by setting the machineApplicableDeprecated tag attribute), a code action will be triggered
whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated
constant.

How is "setting the machineApplicableDeprecated tag attribute" done?
In the following example, currently an empty list of code actions is attached to the character range where my_two_pos is used.
[Edt: added import Std.CodeActionDeprecated]

import Init.Data.Nat
import Std.CodeAction.Deprecated

theorem my_zero_lt_two : 0 < 2 := Nat.le_succ _
@[deprecated my_zero_lt_two] theorem my_two_pos : 0 < 2 := my_zero_lt_two
theorem my_two_pow_pos {m : Nat} : 0 < 2 ^ m := Nat.pos_pow_of_pos m my_two_pos

[Scott Morrison]

It looks like you haven't imported Std.CodeAction.Deprecated.

[Richard Copley]

True! Adding it didn't make the code action appear.

[Richard Copley]

"Setting the machineApplicableDeprecated tag attribute" is done by the code of an elaborator, not by a user. The elaborator for alias in Std.Tactic.Alias does it, when there is a @[deprecated] alias x := y and the token deprecated in the attribute tag is not followed by an identifier.

I wonder if this is what was intended:
(1) If a target is provided in a @[deprecated] attribute, the linter sets machineApplicableDeprecated
(2) The alias tactic also sets machineApplicableDeprecated only if it wasn't already done in (1)
... but somehow point (1) didn't get implemented.

import Init.Data.Nat
import Std.CodeAction.Deprecated
import Std.Tactic.Alias

theorem newname : 0 < 2 := Nat.le_succ _
@[deprecated newname] theorem oldname1 : 0 < 2 := newname
@[deprecated newname] alias oldname2 := newname
@[deprecated] alias oldname3 := newname

theorem thm1 {m : Nat} : 0 < 2 ^ m := Nat.pos_pow_of_pos m oldname1 -- `oldname1` gets an empty list of code actions
theorem thm2 {m : Nat} : 0 < 2 ^ m := Nat.pos_pow_of_pos m oldname2 -- `oldname2` gets an empty list of code actions
theorem thm3 {m : Nat} : 0 < 2 ^ m := Nat.pos_pow_of_pos m oldname3 -- `oldname3` gets a code action

[Mario Carneiro]

machineApplicableDeprecated is public API but only usable from metaprograms. That is, this is a backend feature which is used for creating tactics and attributes that have support from the code action. The frontend version is @[deprecated] alias, and it is written such that you only get the code action if you use @[deprecated] alias specifically (not @[deprecated other] alias or @[deprecated] def)

[Mario Carneiro]

in short, the behavior you demonstrate is deliberate

[Mario Carneiro]

When you use @[deprecated a] alias b := c, it is not a machine-applicable replacement because a may not have the same type as c. If you do @[deprecated c] alias b := c then in principle it could do so, but there is not really any reason to write this (maybe we should lint against it?) since it is the same as @[deprecated] alias b := c

[Mario Carneiro]

Here's how you are supposed to write the first example:

import Init.Data.Nat
import Std.Tactic.Alias

theorem my_zero_lt_two : 0 < 2 := Nat.le_succ _
@[deprecated] alias my_two_pos := my_zero_lt_two
theorem my_two_pow_pos {m : Nat} : 0 < 2 ^ m := Nat.pos_pow_of_pos m my_two_pos

[Richard Copley]

Makes sense! Thank you for the explanation.