[Merged by Bors] - chore(Tactic/DeprecateTo): rename deprecate to into #deprecate to

[SnirBroshi]

To conform to leanprover-community/leanprover-community.github.io#914

---

The underscore could also be a space; what do we prefer?
And should we add an in suffix?

[github-actions]

PR summary 2c7041c86c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2c7041c).

• +2 new declarations
• −1 removed declarations

-Mathlib.Tactic.DeprecateTo.commandDeprecateTo______
+Mathlib.Tactic.DeprecateTo.deprecateTo
+Mathlib.Tactic.DeprecateTo.oldStx

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 2c7041c86c
Reference commit 83b9f16b1f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[thorimur]

This looks good to me, thanks! I'm not sure exactly why, but the underscore looks better to me. I feel like lone tokens ought to connect functionality-tokens to commands or to optional arguments, but not to standard arguments, I suppose? Is there a chance we'd either (1) want to put something in front of to in the future or (2) not include to at all?

I think I prefer this without in either way. :)

[vlad902]

Just a drive-by comment to say that if this lands, there is a reference to "deprecate to" in the style guide that should be updated as well.

[SnirBroshi]

not include to at all?

#deprecate sounds nice, OTOH I think that the "to" helps intuitively understand that the new name should follow the command. I think that #deprecate wins this trade-off and the docstring already explains the syntax, but I worry that I'm biased because I already learned the syntax.

[thorimur]

Ah yeah, I definitely agree that to + new names is good; I'm more so wondering if we'll ever want functionality like #deprecate <cmd> or #deprecate <something_else> <cmd>, in which case it's nice to future-proof by having #deprecate to and not #deprecate_to.

I think either is fine though, so I'll defer to you + anyone else with an opinion :)

I should also mention: this PR should deprecate the deprecate to syntax! :)

[thorimur]

Ah, to be clear, I don't want to remove the to when there are new names. I think the question is just between #deprecate to and #deprecate_to. What I'm saying is just that any future non-to functionality would benefit from the first version!

[SnirBroshi]

Yeah but why not remove the to for a shorter command?
I'm not sure about future uses, but I think one of the first feature requests would be to copy to_additive/to_dual attributes over to the alias, which shouldn't require any new syntax from the command.

[thorimur]

I think the to makes it clear what has what role; to me #deprecate foo <cmd> reads like I'm deprecating foo instead of the following command! 😁

[SnirBroshi]

I agree, but as I said above I think that less typing for a very ephemeral command is probably worth it over the nice "to" syntax.
In the interest of less typing, if we keep the "to" I'd prefer the space version :)

[joneugster]

(I'll start a thread here to keep stuff together, but most of the comments on this PR should be seen as part of this thread here)

I think we should go for #deprecate_to xy.

• I quite agree with Snir's first message about how the _to makes the syntax clearer. I'd expect #deprecate xy to create an alias xy := ... but #deprecate_to xy is fine for the actual behaviour alias ... := xy
• #deprecate_to xy in does logically make sense, but then I'd expect the version without in to also do something (i.e. act on everything after its declaration). Since this wouldn't really make sense, I think we don't need an in. If you wanted, you could add the in as an optional syntax piece with no effect, just for ergonomics.

[joneugster]

(that being said, its kinda bikeshedding and I'm also fine with #deprecate or #deprecate to, the added # is already a big improvement in consistency)

[thorimur]

And just to be clear, you prefer #deprecate_to to #deprecate to? :) (Personally I like the space instead of the underscore, but I could see it going either way.) EDIT: maybe I loaded the page before the edit of the above comment that mentioned #deprecate to... 🙃

[SnirBroshi]

but then I'd expect the version without in to also do something

What about #whats_new in? Should we remove the in from it as well?

[thorimur]

I mentioned this on another PR recently (where we're debating #find_home for <cmd>), but I think there are two valid uses of <foo> in <cmd>: (1) to say that the effects of foo should be present while elaborating cmd (and not afterwards) (2) to act as a natural-language preposition. I think #whats_new in is really only (2).

I think prepositions as "connective keywords" are okay in general (and may be omitted when appropriate too, e.g. the way we don't need a connective before <cmd> in #deprecate to ... <cmd>), but that's just my preference :)

[joneugster]

that sounds fair 👍

What about #whats_new in? Should we remove the in from it as well?

You do have a good point here. I wouldn't be opposed if #whats_new already parsed by itself, regardless of the result of that was (same as with "in"; something else; just a warning that in is missing). I guess rn you get the parsing error unexpected token '/--'; expected 'in' which is at least instructive.

[...] but I think there are two valid uses of in : (1) to say that the effects of foo should be present while elaborating cmd (and not afterwards) (2) to act as a natural-language preposition.

Tbf, so far I've almost exclusively considered (1)

[joneugster]

I've had another idea about the question regarding #whats_new vs #whats_new in, so I've opened an RFC as #43975 if you want to explore that idea further :) It's not really relevant to this PR, but thought I mention it here

[SnirBroshi]

Great! #deprecate to it is.

FWIW #deprecateto also parses correctly and I don't know how to prevent it (tried some combinations of spaces and ppSpace to no avail), but perhaps we could call it a feature

[JovanGerb]

I want to argue for #deprecate_to with the underscore, for consistency with the convert_to tactic!

[joneugster]

FWIW #deprecateto also parses correctly and I don't know how to prevent it

I think this is a Lean feature and it's not worth working around it.

Lean has it's very unique approach on how and when whitespace is relevant for parsing...

[joneugster]

There is still some unresolved discussion about #deprecate_to vs #deprecate to, but I think this is unimportant enough that I can suggest

maintainer merge

The PR keeps the existing pattern (a space in #deprecate to) which seems to be the more conservative choice. Regardless, if people want to, I think the floor is always open for a follow-up discussion or follow-up PR. (I guess one could equally argue that it could be convert to)

Thank you for the PR!

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[grunweg]

Thanks!
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Test and lint