[Merged by Bors] - chore: add missing #align statements#1902
[Merged by Bors] - chore: add missing #align statements#1902
Conversation
kbuzzard
left a comment
There was a problem hiding this comment.
I have actually looked at all 222 changed files here; I left very few comments on specific additions. I think this is a great PR which presumably will be rotting very quickly; if I had merge powers I'd almost be tempted to merge now and fix up the potential issues I flagged later.
The PR seems to have caught the fact that in four or five files, nothing is aligned at all! Many additions are "null" in the sense that they're aligning xyz with xyz but there are still a huge number of genuine alignments.
I've always been aware that mathlib3port was adapted to deal with to_additive aligns some time after to_additive was ported, so there would be some to_additive stuff which had been missed. The technique used in this PR has caught these, but it has also caught declarations which have been generated by ext, simps and reassoc. It is probably worth opening an issue in mathlib3port asking that these declarations are auto-aligned by the porting program, otherwise you'll have to run this code again and again as the port progresses. Once the porting program knows about these (and it might do so already, I'm just observing that clearly it didn't always know about these things) you might just need to run it one last time.
Excellent work! Let's get this merged quickly.
|
Thanks, this is great! bors merge |
This PR is the result of a slight variant on the following "algorithm" * take all mathlib 3 names, remove `_` and make all uppercase letters into lowercase * take all mathlib 4 names, remove `_` and make all uppercase letters into lowercase * look for matches, and create pairs `(original_lean3_name, OriginalLean4Name)` * for pairs that do not have an align statement: - use Lean 4 to lookup the file + position of the Lean 4 name - add an `#align` statement just before the next empty line * manually fix some tiny mistakes (e.g., empty lines in proofs might cause the `#align` statement to have been inserted too early)
|
Pull request successfully merged into master. Build succeeded:
|
This PR is the result of a slight variant on the following "algorithm"
_and make all uppercase letters into lowercase_and make all uppercase letters into lowercase(original_lean3_name, OriginalLean4Name)#alignstatement just before the next empty line#alignstatement to have been inserted too early)