deprecation automation

Stream: general

[Damiano Testa]

Dear All,

a few times the question arose of what is the "correct deprecation syntax". What do you think of adding something like what is below to get some approximately standardized answer to this question?

import Std.Tactic.TryThis
import Std.Tactic.Alias

open Lean Elab in
elab "depr " newId:ident oldId:ident : command => Command.liftTermElabM do
  match (← getEnv).find? newId.getId with
  | some _ => throwError "'{newId.getId}' has already been declared"
  | none =>
    let _ ← Term.elabTerm oldId none
    Std.Tactic.TryThis.addSuggestion (← getRef) (← `(command| @[deprecated] alias $newId := $oldId))

depr oldName Nat
/-
Try this: @[deprecated]
alias oldName := Nat
-/

[Yury G. Kudryashov]

Isn't it easier to use text snippets?

[Yury G. Kudryashov]

At least in Emacs, they can insert current date.

[Yury G. Kudryashov]

I guess, VSCode has a similar functionality.

[Damiano Testa]

What I had in mind was something that would (eventually) also be able to figure out what the old name to be deprecated was and be aware of auto-generated declarations associated with the initial declaration.

A prototype of this is #10864: it does not work as well as I would like yet, but it is aware, for instance of the fact that @[to_additive] adds two declarations to the environment and proposes to deprecate both.

[Damiano Testa]

The command currently behaves as follows:

-- write `deprecate to` and a sequence of names before the declaration to deprecate
deprecate to good_mul good_add
/-- I also have a doc-string -/
@[to_additive "As do I"]
theorem aDeprecatable_mul : True := .intro

/- Try this:
/-- I also have a doc-string -/
  @[to_additive "As do I"]
  theorem aDeprecatable_mul : True :=
    .intro
  @[deprecated]
  alias aDeprecatable_mul := good_mul
  @[deprecated]
  alias aDeprecatable_add := good_add

There are currently 3 main issues:

• the suggested "repeat" command still uses the old name, not the new one;
• the date is not inserted;
• the formatting of the suggested output is not ideal.

[Damiano Testa]

Yury G. Kudryashov said:

At least in Emacs, they can insert current date.

Yes, this is possible in VSCode as well and, in fact, the copyright snippet inserts the current year automatically.

[Damiano Testa]

I fixed (somewhat hackily) the issues that were present with the deprecation tool. Now, it works as follows:

deprecate to id₁ id₂ ... idₙ "2024-02-23"
theorem easy : True := .intro

produces

theorem easy : True := .intro

-- 2024-02-23
@[deprecated] alias easy := id₁

-- 2024-02-23
@[deprecated] alias d₂ := id₂
...

-- 2024-02-23
@[deprecated] alias dₙ := idₙ

assuming that easy autogenerated n non-blacklisted declarations (e.g. to_additive ones).

There is still a small issue with namespaces (i.e. the tool is unaware of them). Other than that, it is up for review!

Also, since it auto-eliminates itself, any major bugs should not affect much: once the deprecations are placed in, the command disappears.

[Damiano Testa]

Following a suggestion of @Thomas Murrills, I've updated the deprecation tool of #10864. Now it stays in-place and it is essentially a macro that expands

deprecate_to id₁ id₂ ... idₙ 2024-02-23
theorem easy₁ : True := .intro

to

@[deprecated] alias easy₁ := id₁
@[deprecated] alias easy₂ := id₂
...
@[deprecated] alias easyₙ := idₙ

This has the advantage of

• reducing duplication,
• automatically taking care of finding the auto-generated lemmas and
• having the date as part of the syntax.

In particular, using this tool, the date must be present and, if this is desired, the tool may stop autogenerating the deprecated aliases automatically once a certain grace period has passed (this is not implemented).

#11195 applies the tool in a couple of places, to showcase its usage.

[Yury G. Kudryashov]

Do you have an example with multiple idₙs?

[Yury G. Kudryashov]

I failed to parse the one in your message above.

[Damiano Testa]

Ah, good point! I will update the PR: my main use-case was deprecating a lemma tagged with to_additive.

[Damiano Testa]

(There are tests in the PR that use to_additive already, but I will look for a "real-world" example.)

[Damiano Testa]

In any case, the first id₁ matches the name shown in the declaration. The others line up (randomly) with the remaining auto-generated declarations. You can check what the order is by using deprecate_to! ...: you get a table of what the pairings are and you can update as you want.

[Thomas Murrills]

Very nice! :) (Btw, as the suggester I feel obligated to say that I do like the macro, but given that it was one of two suggestions, I'm not sure which the community will like best (if either)! :) )

One possible issue with it (which admittedly I'm just thinking through now, apologies) is that it seems to leave the deprecated theorem as the actual theorem, so that we wind up with theorem old_foo ... in source. I suspect we want the source code to be biased towards the current situation, so that we wind up with theorem new_foo ... and a deprecation-based command nearby.

One way to achieve this would be to simply invert things: we have something like

deprecating old_mul_foo old_add_foo
@[to_additive] theorem new_mul_foo ...

(Not sure how much work this would be, apologies for suggesting more.)

I also wonder if the assignments should be in source just in case e.g. the decls later get generated in different orders due to e.g. changes to the internals of @[to_additive]. So maybe it would look like

deprecating old_mul_foo with old_add_foo := new_add_foo, old_other_bar := new_other_bar
@[to_additive] theorem new_mul_foo ...

or some other syntax, I'm not sure.

I also think there's room for automation here (though I don't know if it would be in the same PR)! In that case it would be nice to write something like

deprecating? old_mul_foo
@[to_additive] theorem new_mul_foo ...

and get a clickable suggestion of how many assignments you need and what the pairings should be. (We could even maybe guess the old names by replacing new_mul_foo with old_mul_foo and seeing what the environment would be?)

What do you think?

[Damiano Testa]

@Yury G. Kudryashov, I looked around, but it seems that to_additive already handles the deprecated attribute, so the gain for multiple declarations arising from to_additive is slightly diminished, as you have to write the old additivized name manually: it would be an extra twist to make the deprecation tool handle automatically the to_additive name-replacement.

[Damiano Testa]

@Thomas Murrills, if I understand correctly, the name that is visible in the code

deprecate_to depr_name date
theorem new_name ...

is already as you say, right? The theorem new_name is the name that should stay, the one that should disappear is the one on the line above. Or maybe I misunderstood your comment! (EDIT: the original version of the PR started with the "wrong" name appearing and replaced it with the "correct" one as a Try this suggestion. The newer version starts with the "correct" syntax already present.)

[Damiano Testa]

Also, currently, the multi-name assignment is mostly a non-issue: it is a struggle to find lemmas that generate more than one extra declaration, and I would have to think hard before I can find one that auto-generated 2 new ones and is deprecated!

[Damiano Testa]

As for the ordering issue, I also think that a simpler approach would be to match the identifiers that the user types with the new environment declarations in the following order:

• first, the one that is actually in the source syntax;
• next, all the remaining ones in alphabetical order.

This way, the two orders are fixed: the user one on one hand and the (almost) alphabetical on the other hand. The tool does give an option to show what the assignment is, so the user can tweaks the names that they provide to adjust to the auto-generated ones.

[Damiano Testa]

(But, as I said, more than 2 declarations per lemma is really rare and, with up to two declarations, there is no ambiguity in the ordering.)

[Thomas Murrills]

Damiano Testa said:

Thomas Murrills, if I understand correctly, the name that is visible in the code

deprecate_to depr_name date
theorem new_name ...

is already as you say, right? The theorem new_name is the name that should stay, the one that should disappear is the one on the line above. Or maybe I misunderstood your comment! (EDIT: the original version of the PR started with the "wrong" name appearing and replaced it with the "correct" one as a Try this suggestion. The newer version starts with the "correct" syntax already present.)

Oh, ok, is the PR description/comment above out of date? Currently it says that given

deprecate_to bar
theorem foo := …

we get

@[deprecated] alias foo := bar

which would deprecate foo.

[Thomas Murrills]

Damiano Testa said:

As for the ordering issue, I also think that a simpler approach would be to match the identifiers that the user types with the new environment declarations in the following order:

• first, the one that is actually in the source syntax;
• next, all the remaining ones in alphabetical order.

This way, the two orders are fixed: the user one on one hand and the (almost) alphabetical on the other hand. The tool does give an option to show what the assignment is, so the user can tweaks the names that they provide to adjust to the auto-generated ones.

Ah, ok, that makes sense! (I didn’t really have a sense of how frequently this would be used for deprecating multiple generated declarations. :) ) (There’s some extant order on Name which makes this easy, right?)

[Damiano Testa]

Yes, the comment above talks about the old version of the PR: this started with the "unwanted" syntax and, via a Try this converted it to the "wanted" one.

[Damiano Testa]

The ordering is not implemented, but, at worst, it can go via alphabetical in Name.toString.

[Thomas Murrills]

Ah, maybe it’s just a definition and not an instance of anything? (I could swear there’s something out there that I’ve encountered before…)

[Damiano Testa]

Sorry, by "not implemented", I meant "not implemented in the PR". Certainly the order is there already in Core/Std.

[Thomas Murrills]

Ah, gotcha!

[Damiano Testa]

#10864 just received a positive comment: can I ping this PR for some further comments?

Thanks!

[Thomas Murrills]

I’ll try to give it a proper review today or tomorrow, looking forward to it landing soon if there are no objections! :)

[Thomas Murrills]

(Also I expect there might be further discussion on whether to keep it as a macro or not, so I’ll try to make this simply a “technical” review on the rest of the code if no consensus is reached before I review it. That way it’s at least just the one remaining question.)

[Damiano Testa]

Thomas, thank you for the offer to review! As you will see from the PR comments, Scott is not too positive about the PR.

I wonder whether making it an attribute as @[deprecate! old_name YYY-MM-DD] would be better. Where the ! means, create the alias as well.

So there would be

-- currently available
@[deprecate] lemma x ... -- simply deprecate, do not propose a replacement version
@[deprecate new_name] alias x ... -- deprecate, proposing `new_name`

-- extension
@[deprecate! old_name YYY-MM-DD] lemma x ... -- create an alias and deprecate `old_name`

There is an asymmetry in this approach in that the deprecation tag goes on the new lemma, rather than the old one, but there is no need for the explicit alias to be present in the code.

[Kim Morrison]

I guess I don't understand what problem this is solving. Could you explain what is not working or unpleasant about the current setup?

[Damiano Testa]

For me, these were the main motivations.

• Avoid having to write a separate alias command, that is completely determined once you know the new lemma name and the old one. Also, there were several questions on Zulip about how to correctly deprecate a lemma and fixing an easy-to-remember "standard" seemed helpful.
• The date is part of the syntax.
• As a mild stylistic bonus, I like that deprecate x means that x is deprecated, as opposed to something like prefer x.

I initially also thought that it would be useful with auto-generated lemma names (which it is), but it turned out that to_additive already has a deprecation flag and to_additive is the biggest source of autogenerated names that should really be deprecated as a whole.

[Kim Morrison]

Ah, great, not having to write the alias is what I was missing.

[Kim Morrison]

As long as you're sure avoiding creating too many ways to say the same thing, then I remove my objection!

(Can we forbid or discourage the old style with an alias??)

[Damiano Testa]

Scott Morrison said:

As long as you're sure avoiding creating too many ways to say the same thing, then I remove my objection!

(Can we forbid or discourage the old style with an alias??)

I cannot be sure, but the new syntax seems easier to remember than having to add a separate alias command.

As for "deprecating the deprecation alias", I can look into it: since it is a Std extension, I am pretty sure that we can make it so that if the deprecate alias has an actual syntax reference, then it might emit a warning. I have not thought about it carefully, though.

[Damiano Testa]

Or simply, the deprecated alias emits a warning and the "preferred syntax" catches the warining.

[Mario Carneiro]

I also don't really understand the motivation. You say "Avoid having to write a separate alias command, that is completely determined once you know the new lemma name and the old one" but alias asks for very little information beyond the old and new names. I don't see much benefit in a separate syntax for the same thing, and the attribute syntax is more limited in the other metadata you can provide (e.g. docstrings).

[Yaël Dillies]

I don't think you can deprecate the @[deprecated] alias syntax since your new syntax only works when the lemma to be deprecated is defined in the same file as the lemma it is deprecated to

[Damiano Testa]

These are all fair points. In fact, in my initial proposal I had a Try this that took the old command and the new name and did the renaming and the writing of the alias command.

[Damiano Testa]

However, it then evolved into hiding the "boiler-plate syntax" and this is its current form. So, my conclusion is:

• the Try this was nice, but maybe not too useful;
• the new macro version is nice, but it is limited enough that it may not be a good replacement for "deprecate alias".

[Michael Rothgang]

Since I "re-sparked" this discussion, let me weigh in. My personal motivation was ergonomics: I did the renamings and was then asked to add the deprecations (which meant having to go over the whole diff and having to switch between the diff and VS Code to actually make the change). And reading up on/cargo-culting the deprecation syntax first.

Having to write or copy-paste a long name twice was a tad annoying... but thinking again, that was actually not so bad and I don't see such a strong case any more.

[Michael Rothgang]

I wonder, however, if there's a way to automate the deprecation in a different way:

• can we have a code action for deprecating a lemma (which uses the syntax will have agreed on), and
• can the rename handler trigger this code action?
  This would solve all the issues for me while avoiding this particular bikeshed about a new tool.

[Yaël Dillies]

I've opened #13206 for a code snippet which I found useful