[Merged by Bors] - chore: script for by linebreaks

[mo271]

Not quite sure if the -i inplace part will work on all systems...

[mo271]

It might be good, as suggested by @digama0 to run this when generating the files for mathlib3port

[eric-wieser]

Can mathport do this for us?

[mo271]

I think that would be very good!
In fact it might even do this for lines of length 98, 99 and 100, resulting in some linter warning, that the person porting can take care of manually in those cases, because with this script those cases are not taken care of.

[rwbarton]

mathport used to get the by location correct (at least more of the time), it seems things changed in the run that resulted in leanprover-community/mathlib3port@27def98.
But the old version has a lot of weird layout in declarations, as well.
It's also not clear to me what actually changed to cause the new layout...

[rwbarton]

Could you add a 1-2 line comment explaining what the script does (e.g. # Modify all lean files in mathlib to put "by" at the end of the previous line, where possible)?

[digama0]

mathport used to get the by location correct (at least more of the time), it seems things changed in the run that resulted in leanprover-community/mathlib3port@27def98. But the old version has a lot of weird layout in declarations, as well. It's also not clear to me what actually changed to cause the new layout...

That run was mathport #544, and if you look at the CI page from around then you will notice that that run was preceded by mathport being broken for several days, during which there was a lean bump from lean4:nightly-2022-12-16 to lean4:nightly-2022-12-22. During that period the most likely commits that could have caused this are

• fix: Format.align always prints whitespace by gebner
• fix: parenthesize by optParam values by Kha
• refactor: remove redundant state by Kha

[mo271]

Could you add a 1-2 line comment explaining what the script does (e.g. # Modify all lean files in mathlib to put "by" at the end of the previous line, where possible)?

Done

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style