Zulip Chat Archive

#23755 is the second of three steps in splitting Algebra.Order.GroupWithZero.Unbundled to remove another long file. It doesn't actually split, it just renames the file (and another one) to something more sensible

Jeremy Tan (Apr 07 2025 at 13:30):

:up:

Kim Morrison (Apr 07 2025 at 13:45):

Jeremy Tan said:

:up:

@Jeremy Tan, please don't ping so quickly, it's just noise, and if anything makes it less likely you'll get quick attention to PRs.

Jeremy Tan (Apr 11 2025 at 00:16):

#23928 clears deprecations from 1 to 10 October 2024 (which is a lot)

Jeremy Tan (Apr 11 2025 at 00:40):

I still have #23686 open, that fixes a bunch of induction branch names and motives

Jeremy Tan (Apr 11 2025 at 02:52):

And I would like #23860 (MeasureTheory.Integral.Lebesgue.Basic) merged first before I split the last two long files

Jeremy Tan (Apr 12 2025 at 00:02):

#23324 (depriming induction' with 5+ variables) is now unblocked

Jeremy Tan (Apr 12 2025 at 00:05):

As is #23947 (prove lintegral_eq_zero_iff' without monotone convergence, so as to help #23860)

Jeremy Tan (Apr 12 2025 at 00:08):

And #23936, which clears up files with no declarations or only deprecated ones

Jeremy Tan (Apr 15 2025 at 12:57):

#24079 replaces (almost) all instances of dot-space-space with dot-space (single sentence spacing)

Yaël Dillies (Apr 15 2025 at 13:00):

Some people like to separate their sentences with two spaces. What's the issue with that?

Jeremy Tan (Apr 15 2025 at 13:02):

Yaël Dillies said:

Some people like to separate their sentences with two spaces. What's the issue with that?

Every major English style guide says no to two spaces

Michael Rothgang (Apr 15 2025 at 13:43):

Before accepting such a change, I (personally) would like to see some consensus that this is desirable (and a PR to the style guide). This looks like a substantial bikeshedding hub, let's agree on it before making the change :-)

Jeremy Tan (Apr 15 2025 at 14:04):

I did this once for my own amusement, without intention of having this merged. I have made this PR partly to save the trouble of doing this again

Kevin Buzzard (Apr 15 2025 at 17:33):

And to cause trouble to all the people who will get merge conflicts as a result.

Kevin Buzzard (Apr 15 2025 at 17:34):

which is far more trouble than running a regex search on mathlib.

Kim Morrison (Apr 16 2025 at 00:36):

Yes, let's not do this.

Eric Wieser (Apr 16 2025 at 01:15):

I think there was a related proposal recently to use semantic line breaking, where every . is followed by a newline

Eric Wieser (Apr 16 2025 at 01:15):

(Which gives better git diffs than column wrapping, and is less
less likely to accidentally repeat a word)

Jeremy Tan (Apr 16 2025 at 02:05):

#16408 (revived) deprecates Order.Nat

Jeremy Tan (Apr 23 2025 at 00:04):

#24282 renames Lintegral, Laverage to LIntegral, LAverage (following AEStronglyMeasurable)

Jeremy Tan (May 01 2025 at 00:17):

#24483 clears the remaining deprecations from October 2024

Yaël Dillies (May 01 2025 at 06:09):

Can we please seriously consider a bot writing and merging those PRs?

Jeremy Tan (May 01 2025 at 06:13):

Yaël Dillies said:

Can we please seriously consider a bot writing and merging those PRs?

The regex can't clear out everything, manual intervention will always be needed (unlike updating dependencies)

Jeremy Tan (May 01 2025 at 06:13):

Also I don't know how to write a bot

Yaël Dillies (May 01 2025 at 06:29):

Sure, but the bot can still do most of the work, no?

Michael Rothgang (May 01 2025 at 08:59):

Task 37 from #mathlib4 > Call for help: technical/ organisational debt sounds like a fun one to pick up. Perhaps it can be regex-automated, it would certainly make mathlib nicer to read.

Damiano Testa (May 01 2025 at 11:26):

Jeremy Tan said:

Yaël Dillies said:

Can we please seriously consider a bot writing and merging those PRs?

The regex can't clear out everything, manual intervention will always be needed (unlike updating dependencies)

It need not be a regex, it could be a syntax-aware replacement. Looking at the PR, all the declaration removals could have been automated correctly, I think. The section removal could also be automated, but for that it would maybe be better if the name of the section included a date, so that the bot would know to remove it.

Yaël Dillies (May 01 2025 at 12:06):

I think empty sections can simply be another job? Removing deprecations isn't the only way to end up with an empty section

Jeremy Tan (May 02 2025 at 00:26):

In any case, I don't know how to get the bot to automatically create a PR to remove deprecations. We should start with just the regex, then see how to turn it into a syntax-aware job

Notification Bot (May 02 2025 at 00:26):

A message was moved here from #PR reviews > #24452 + #24454 + #24506: rotate_isos tactic by Jeremy Tan.

Last updated: May 02 2025 at 03:31 UTC