[Merged by Bors] - chore: rename op_norm to opNorm

[sgouezel]

---

[adomani]

Picking up on this conversation, what would you think of adding after each modified #align x y something like:

theorem YYY ...

#align XXX YYY

@[deprecated YYY] alias YYYold := YYY -- deprecated on 2024/02/02

Catching changed aligns is relatively easy and then it is simply a matter of reading the git diff.

[sgouezel]

It would definitely be an improvement, but still not perfect because some lemmas are not backported from Lean 3 and therefore have no #align. If you know how to write a script reading git diff, it shouldn't be much more complicated to check for lines starting with theorem or lemma and see if the characters before the first ( or { or [ (i.e., the name) have changed, and then add the deprecation line at the first empty line after the theorem statement. Not completely fail-proof, but good enough for 99% of the cases I would say, and the remaining ones can be fixed by hand. Don't hesitate to experiment as much as you want on this branch! I'm marking it as WIP for now to let you experiment. You can put it back to awaiting review once you're happy with the result, or bored with the experiments!

[adomani]

Ok, I'm busy for about an hour, but will play with it a little afterwards!

[adomani]

Btw, the main issue is not finding the start of the theorem, but the end.

[sgouezel]

Evyerthing between theorem or lemma and the first ( or { or [ should be the theorem name, right? And then go to the next empty line to put the deprecated statement? This breaks if there is an empty line in the proof, but this should be rare enough that it's not an issue, I guess.

[adomani]

Yes, after theorem/lemma the first consecutive block of "mostly characters, digits, underscores and a few more symbols" is the theorem name. What does not necessarily work so well is finding the end of the whole declaration, not the end of the name, as not always declarations are separated by empty lines. However, this may be the case for the specific declarations touched in this PR (and for most declarations anyway), so I will use this heuristic, if needed.

[adomani]

Ok, my previous comment was a little misguided: the deprecation statement does not need to be right after the statement to deprecate, although it is probably desirable that it is.

Anyway, I have a rough script for adding deprecations and the latest commit only adds the deprecations. Let's see if CI is happy and then what actual issues there are with the deprecations!

[sgouezel]

This is awesome, thanks a lot!
Is the script easy to use? I can easily imagine that it would help me very often!

[adomani]

The script is easy to use, but it assumes that every line that has a theorem/lemma in the diff corresponds to a name change to be deprecated. This applies if you change anything on that line, not necessarily the name! Also, it assumes that the new declarations appear in the same order as the old ones and in the same files.

I'll polish it up and make it available, though maybe tonight and after a little more testing.

[adomani]

The script that I used is here.

To use it, copy it to your computer, make it executable and run it. You have the option of passing a commit hash that the script will use to figure out what has been deprecated. If you do not provide one, then the script will try to find the master commit from which you branched and use that. If you use a Unix-based system, the commands below should work (assuming that you saved the file in the root directory and called it add_deprecation.sh):

chmod u+x add_deprecation.sh
./add_deprecation.sh
##  you will be prompted to provide a commit hash, but the script suggests a guess
##  you can also pass the hash explicitly when you run the command

The heuristic that the script uses for finding which declarations to deprecate is very crude. This means that in order for the script to have a chance of producing a useful output, the PR should be carefully prepared to assist the script. Basically, your PR was perfect: just lemma renames and fixing up proofs. As soon as there are more changes happening on lines containing theorem/lemma, the script will get confused.

[urkud]

Thanks! 🎉
bors merge

[mathlib-bors]

Build failed:

• Lint style

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style