branches cleanup

Stream: general

[Rob Lewis]

There are 951 branches in the mathlib repository right now. Even though the cost of a branch is very low, this feels messy -- I'm guessing many of those branches will never be touched. So, PSA, consider taking a look and cleaning up your dead branches! Err on the side of caution and don't delete anything that other people might be using. But if you created a branch and its usefulness is over, let's get rid of it.

[Yaël Dillies]

Here's a list of the least active branches

[Yaël Dillies]

All the stuff in branch#fundamental-groupoid is now in mathlib in one form or another.

[Yaël Dillies]

I am personally reviving #2770 and #5104.

[Yaël Dillies]

I am also taking care of branch#fin_range some time soon.

[Yaël Dillies]

All the stuff in branch#100-theorems-73 is now in mathlib.

[Yaël Dillies]

(uh? Zulip formatting go weee)

[Yaël Dillies]

branch#seminorm-etc can straight up be deleted as #1926 has been superseded by #4827

[Yaël Dillies]

Would be nice if someone else could make the final call on each of these.

[Alex J. Best]

I noticed some merged branches aren't deleted by bors, e.g. alexjbest/add_subgroup_nsmul (https://github.com/leanprover-community/mathlib/pull/9594) was merged but bors never deleted it? Does anyone know the reason for this? I for one assumed bors was deleting all old branches and never paid any attention. Can we run a script that deletes merged branches to clean this up?

[Yaël Dillies]

Yes, it is running now and called Yaël :wink:

[Bryan Gin-ge Chen]

I think bors only deletes branches if GitHub reports that there are no unmerged commits, but sometimes GitHub is wrong. That seems to be the case with #9594.

[Yaël Dillies]

@Chris Wong, do you wanna PR your Fibonacci words? https://github.com/leanprover-community/mathlib/compare/fibword?expand=1 It looks good.

[Yaël Dillies]

@Jujian Zhang, what's the status of #3884? We don't seem to have the juicy bits in mathlib yet.

[Yaël Dillies]

We have Fermat's Last Theorem on branch#fermat4P2 for the case n = 4. @Paul van Wamelen, will you PR it?

[Kevin Buzzard]

I thought we already had FLT for n=4 in master

[Riccardo Brasca]

We do docs#not_fermat_4

[Riccardo Brasca]

Time for n=3?

[Ruben Van de Velde]

I have n=3 sorry-free, but I got distracted by other things before figuring out how to best PR it

[Riccardo Brasca]

So maybe it's time for regular primes? This seems an ambitious but not out of reach project.

[Yaël Dillies]

@Johan Commelin, do you think we should push for #4753 to go through?

[Yaël Dillies]

And in general what do we want to do with those forgotten branches? I'm trying to revive some of them, but I obviously can't do it all.

[Johan Commelin]

Yes, that one certainly deserves to be revived.

[Johan Commelin]

It's useful for smooth/étale ring homs.

[Riccardo Brasca]

We absolutely need Kahler differentials. I thought a bit about it, but it's not clear how to characterize them without quantifying over universes.

[Chris Wong]

Yaël Dillies said:

Chris Wong, do you wanna PR your Fibonacci words? https://github.com/leanprover-community/mathlib/compare/fibword?expand=1 It looks good.

Hi Yaël! I've got a lot on my plate at the moment, but I'm happy for you (or anyone else) to PR it in my stead :)

[Chris Wong]

The approach I used for palindrome_fibword was a bit strange – it invokes the substitution directly, instead of the standard strategy using concatenation (i.e. https://math.stackexchange.com/a/3142787/18486). It might be worth investigating whether the concatenation approach is better.