Auto-replace deprecated aliases?

Stream: general

[Yury G. Kudryashov]

My current workflow when I rename a theorem in Mathlib is:

• write deprecate to newName before theorems;
• run code action to rename the theorem and generate a deprecated alias (works most of the time, with some bugs around namespace handling);
• push to Github, wait for CI (should compile with warnings);
• get cache;
• run lake build locally (should print a bunch of warnings without recompiling anything);
• go over the warnings in the reverse order and manually replace old names with new names.

For lemmas with sufficiently long names, I can use text search&replace to apply renames, but for short names (e.g., prod_mk -> prodMk) it fails. Is there a better way to replace all usages of a name, including dot notation?

[Michael Rothgang]

For steps (1) and (2), you can also just rename the theorem, and use scripts/add_deprecations.sh, right? (Not saying this is better: is this worse in practice? If we can centralise maintenance efforts on one instead of N ways of doing the same, that's generally good.)

[Michael Rothgang]

For steps (5) and (6): I believe @Damiano Testa's bump_deprecations tool did this. What would maintainers think about adding this to mathlib or batteries?

[Yaël Dillies]

scripts/add_deprecations.sh does me very well, I must say

[Michael Rothgang]

Currently, it is a separate repository - so others can use it. That makes sense in principle --- but raises the bar for using it in mathlib a lot: I have to

• realise that using the tool would actually help me here. (For just 10 deprecations, it's faster to do them by hand.)
• remember the path of the project and the correct incantation to put into my lakefile. (Yes, it was on zulip. But so I'd need to find that comment --- if I'd bookmark that, just find the bookmark. Still, one minute of searching and a context switch.)
• modify my lakefile accordingly, by hand
• push to CI and wait for mathlib to recompile

[Yaël Dillies]

Pressing F2 on a declaration name is the supposedly canonical way to perform renames, but it is basically useless due to its lack of namespace-awareness

[Michael Rothgang]

The first steps may only take me 5 minutes overall (in the best case)... but force me to context-switch out of what I'm doing right now. The last step in the best case (remembered before pushing to CI first) may only increase mathlib build times (to "build all of mathlib" as opposed to incrementality). In the worst case, I only remember after pushing, and then it's 40 extra minutes of waiting. That's why I never use the tool.

[Michael Rothgang]

What would help me use bump_deprecations is

• (in lake) have some lake add bump_deprecations command, which would find the project on reservoir, find the right version for my project (if existing) and adds it to my lakefile. (Basically, the equivalent of Rust's cargo add.) This would speed up the first three steps above a lot, and do away with all the context-switching.
• (in lake?) Have a notion of dev-dependency, which don't require rebuilding all of mathlib for adding it. Basically, adding a new executable does not effect any changes on mathlib, hence should not require a full rebuild.
• (in mathlib) integrate the tool into mathlib or batteries. Or at least add it as a dependency to mathlib, so it's always available.

[Michael Rothgang]

Yaël Dillies said:

Pressing F2 on a declaration name is the supposedly canonical way to perform renames, but it is basically useless due to its lack of namespace-awareness

There's another reason: I cannot use this for more than one rename reliably due to olean invalidation.
If I rename to a new identifier of different length and want to do another rename which touches the same line, F2 will still use the old syntax positions --- which means changing the middle of the line, and actually not the identifier. In other words, renaming more than one declaration can become a gamble.

[Michael Rothgang]

(The tool is at https://github.com/adomani/UpdateDeprecations, for the record --- and not on reservoir.)

[Michael Rothgang]

@Damiano Testa It seems the UpdateDeprecations tool does not have a license --- which is presumably why it's not on reservoir. A no-bikeshed option could be to copy mathlib's license, the Apache 2.0 license.

[Damiano Testa]

UpdateDeprecation was still somewhat experimental and I have not looked at it in quite some time.

[Damiano Testa]

In theory, it should attempt to replace names, being aware of namespaces and somewhat of dot notation, but I have not tried testing it too much.

[Damiano Testa]

Part of the reason that I did not develop it further is that I was hoping that it would latch onto refactor, but that is on hold.