deprecated alias and code action

Stream: general

[Michael Stoll]

It looks like a line like

@[deprecated (since := "2024-07-20")] alias pow_ne_one_of_lt_orderOf' := pow_ne_one_of_lt_orderOf

has the effect to get a yellow squiggle and a black strike-through in VS-code (and a message) when the deprecated name is used, but instead of offering to replace by the new name, the pop-up says "No quick fix available" (this is on VSCode). I remember that some time ago, one could get the replacement by clicking on a "quick fix" message. Could this be reinstated?

[Ruben Van de Velde]

I thought that was supposed to work, yeah

[Yaël Dillies]

Are you sure you aren't using to_additive simultaneously?

[Yaël Dillies]

Something like @[to_additive, deprecated (since := "2024-07-20")] alias pow_ne_one_of_lt_orderOf' := pow_ne_one_of_lt_orderOf will NOT register the additive alias as a deprecated version of the additive lemma

[Michael Stoll]

It is not specific to this precise renaming. (And the corresponding line for the additive version is also there.)

[Michael Stoll]

In fact, I had it happen with ZMod.nat_cast_zmod_eq_zero_iff_dvd--> ZMod.natCast_zmod_eq_zero_iff_dvd just now.

[Michael Stoll]

The pop-up message says

`ZMod.nat_cast_zmod_eq_zero_iff_dvd` has been deprecated, use `ZMod.natCast_zmod_eq_zero_iff_dvd` insteadLean 4
ZMod.nat_cast_zmod_eq_zero_iff_dvd (a b : ℕ) : ↑a = 0 ↔ b ∣ a
Alias of ZMod.natCast_zmod_eq_zero_iff_dvd.

import Mathlib.Data.ZMod.Basic

No quick fixes available

[Michael Stoll]

I.e., it "knows" what the fix would be, but doesn't provide a one-click option to perform it.

[Mario Carneiro]

are you importing Batteries.CodeAction?

[Michael Stoll]

Is this implied by import Mathlib.Tactic?

[Michael Stoll]

Anyway, adding the import does not change this behavior.

[Mario Carneiro]

MWE?

[Michael Stoll]

import Batteries.Tactic.Alias

theorem foo : True := trivial

@[deprecated] alias bar := foo

example : True := bar

Infoview: `bar` has been deprecated, use `foo` instead

Hover (on bar in the example):

`bar` has been deprecated, use `foo` instead       Lean 4
bar : True
Alias of foo.

View Problem (Alt + F8)         No quick fixes available

[Michael Stoll]

@Damiano Testa #min_imports didn't do anything here (with import Mathlib at the beginning).

[Michael Stoll]

(The (since := ...) part is not relevant. Removed in the MWE above.)

[Damiano Testa]

The new command needs import Mathlib.Tactic.MinImports and then it is per declaration and with in, so #min_imports in ... and examples are only supported for syntax/tactics currently.

[Damiano Testa]

The per file new #min_imports is a linter, but is still in development.

[Damiano Testa]

Here is an extended example:

import Mathlib

-- `#min_imports in` really likes `Lean.Parser.Command`:
-- I know about this, but have not managed to fix it yet
#min_imports in  -- import Lean.Parser.Command
theorem foo : True := trivial

#min_imports in  -- import Batteries.Tactic.Alias
@[deprecated] alias bar := foo

-- `example`s do not leave a trace in the environment,
-- so `#min_imports (in)` does not detect their `Expr` information
-- I plan to fix this for `#min_imports in`, so that it can detect
-- when `example`s increase the imports
#min_imports in
example : True := bar  -- import Lean.Parser.Command

-- import Batteries.Tactic.PermuteGoals
-- import Mathlib.Tactic.ExtractGoal
-- import Mathlib.Data.Nat.Notation
#min_imports in  -- still sees the tactic/Syntax information
example : True := by have : ℕ := 0; extract_goal; on_goal 1 => exact .intro

-- nothing
#min_imports

[Michael Stoll]

I was just trying #min_imports at the end of the file. I need to get used to #min_imports in, I guess :smile:

[Damiano Testa]

In case you find it useful, #min_imports in just received an upgrade: now it should handle better instances (named or nameless) and attributes.

[Michael Stoll]

Another observation: in the following:

import Mathlib

structure A where
  a : Nat

example : A := _

VSCode would shoe a blue lightbulb with code actions (like inserting a skeleton for the structure) on the left on top of example. Now I get the error

don't know how to synthesize placeholder
context:
⊢ A

How do I get the blue lightbulb back?

[Kim Morrison]

I think I may have broken this by replacing an import Batteries with finer imports. I'm still away from a computer, but if you could check whether adding import Batteries fixes this minimisation that would be great.

[Kim Morrison]

If so, let's work out the exact import required, add that back to something like Tactic.Basic (or even lower?), and ideally even comment the import explaining which code action it enables so I don't accidentally remove it again!

[Michael Stoll]

import Batteries indeed fixes the problem with the missing blue lightbulb.

[Michael Stoll]

(I had assumed that Mathlib imports (all of) Batteries, but it seems I'm mistaken.)

[Michael Stoll]

import Batteries.CodeAction is sufficient.

[Johan Commelin]

Kim Morrison said:

If so, let's work out the exact import required, add that back to something like Tactic.Basic (or even lower?), and ideally even comment the import explaining which code action it enables so I don't accidentally remove it again!

Done in #15003