Freezing analysis.convex.basic

Stream: general

[Yaël Dillies]

Dear convex analysts, could we try not to touch analysis.convex.basic for a little while? I'm scrambling it all in #9058 which means I have to reproduce changes by hand from a mangled diff.

[Johan Commelin]

Do you have an estimate for how long you want to freeze it?

[Oliver Nash]

I'm in favour of the generalisation of #9058 but I'm a bit wary of a freeze (though I'm sure I could be persuaded). I wonder an alternative approach would be to split analysis.convex.basic into several files so that even if we still opt to freeze, the impact will be smaller.

[Oliver Nash]

For clarity, I mean to precede #9058 by a simple PR that changes nothing except for splitting the file. @Yaël Dillies Do you think this would help?

[Eric Wieser]

It seems to me a lot of the scrambling is reordering lemmas around. If you're worried about conflicts, it might make sense to first make a PR to reorder the lemmas in a somewhat sensible order, and a second one to generalize them

[Yaël Dillies]

Johan Commelin said:

Do you have an estimate for how long you want to freeze it?

A week maybe? I'm working hard on it and in 3 days I went through half of analysis.convex.basic. So 3 more days it is, then probably 2 or 3 more for the other files using convex stuff.

[Yaël Dillies]

Oliver Nash said:

I'm in favour of the generalisation of #9058 but I'm a bit wary of a freeze (though I'm sure I could be persuaded). I wonder an alternative approach would be to split analysis.convex.basic into several files so that even if we still opt to freeze, the impact will be smaller.

I'm already planning on splitting analysis.convex.basic into analysis.convex.function (Yury already wanted that in #4787) and analysis.convex.combination. But this won't help much as the bulk of the work is to find the correct generality of each lemma, and I'm not scrambling the 3 future files together.

Eric Wieser said:

It seems to me a lot of the scrambling is reordering lemmas around. If you're worried about conflicts, it might make sense to first make a PR to reorder the lemmas in a somewhat sensible order, and a second one to generalize them

This won't help much either because the scrambling is motivated by the necessary assumptions, and as said above this is the hard part of what I'm doing.

[Oliver Nash]

It's not my call but I'm even more wary after hearing more. I encourage you to find ways to break down this work into more PRs.

[Yaël Dillies]

Well I can always just leave ℝ in some places. This is the easy way to split the work.

[Oliver Nash]

Right: a general definition is much more important than a general lemma etc.

[Yaël Dillies]

Okay well if you agree with this approach then a first PR can be ready this evening, if I get out of the orange bar hell.

[Oliver Nash]

Bear in mind, it's not my call. Others may see things differently. But delivering a stream of smaller PRs that generalise things incrementally (definitions first, then lemmas) will probably make everyone's life better.

[Eric Wieser]

Yaël Dillies said:

Well I can always just leave ℝ in some places. This is the easy way to split the work.

I think this is a sensible approach; generalize the definition and the really basic APIs, and replace convex with convex ℝ everywhere else. Then you can do the rest piecewise in later PRs.

[Yaël Dillies]

Here's the first one! #9094
it generalizes segment and open_segment

[Scott Morrison]

I left a few comments, hopefully easy.

[Yaël Dillies]

Thanks!

[Yaël Dillies]

#9115 puts finset.center_massin its own file. It commutes with #9094, but I'm now stuck. One of them must go through for me to continue the refactor.

[Eric Rodriguez]

Yael, #9094 doesn't compile

[Yaël Dillies]

Fixing it :tools:

[Yaël Dillies]

It was the new notation, that already existed anyway. :sweat_smile:

[Yaël Dillies]

@Patrick Massot, localized [x, y] notation causes parsing problems. I'll just remove it and you can keep declaring it locally, as it was done before.

[Mario Carneiro]

By the way, [x, y] notation is one of the few remaining unresolved mathport issues. There are some things that can still be done but I would rather the overload didn't exist

[Yaël Dillies]

Ah, further reason!

[Kevin Buzzard]

This is simple to fix -- give us our notation back and the CS people can use some random unicode thing for their lists

[Kevin Buzzard]

Who needs lists anyway

[Yaël Dillies]

something... something... finset something... something...

[Patrick Massot]

Mario Carneiro said:

By the way, [x, y] notation is one of the few remaining unresolved mathport issues. There are some things that can still be done but I would rather the overload didn't exist

This is really sad for Lean 4. Can't we get that weird super specialized list thing localized (or scoped or whatever)?

[Mario Carneiro]

It's not a problem with lean 4 so much as with mathport

[Mario Carneiro]

The problem is that we have a notation name conflict, so we don't know whether we want the list notation or the ... whatever this is

[Mario Carneiro]

Also, there is a lot more reliance on macros in lean 4 that might unfold to something containing list brackets. I really don't think it's a good idea to overload them