Zulip Chat Archive

Stream: general

Topic: Freezing analysis.convex.basic


Yaël Dillies (Sep 08 2021 at 14:25):

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 (Sep 08 2021 at 14:43):

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

Oliver Nash (Sep 08 2021 at 15:08):

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 (Sep 08 2021 at 15:09):

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 (Sep 08 2021 at 15:53):

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 (Sep 08 2021 at 15:55):

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 (Sep 08 2021 at 16:00):

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 (Sep 08 2021 at 16:01):

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 (Sep 08 2021 at 16:02):

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

Oliver Nash (Sep 08 2021 at 16:02):

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

Yaël Dillies (Sep 08 2021 at 16:03):

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 (Sep 08 2021 at 16:05):

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 (Sep 08 2021 at 16:49):

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 (Sep 08 2021 at 17:19):

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

Scott Morrison (Sep 09 2021 at 06:49):

I left a few comments, hopefully easy.

Yaël Dillies (Sep 09 2021 at 06:51):

Thanks!

Yaël Dillies (Sep 09 2021 at 15:07):

#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 (Sep 09 2021 at 15:13):

Yael, #9094 doesn't compile

Yaël Dillies (Sep 09 2021 at 15:14):

Fixing it :tools:

Yaël Dillies (Sep 09 2021 at 15:18):

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

Yaël Dillies (Sep 09 2021 at 22:20):

@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 (Sep 09 2021 at 22:21):

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 (Sep 09 2021 at 22:26):

Ah, further reason!

Kevin Buzzard (Sep 09 2021 at 22:45):

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 (Sep 09 2021 at 22:45):

Who needs lists anyway

Yaël Dillies (Sep 09 2021 at 22:46):

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

Patrick Massot (Sep 09 2021 at 23:24):

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 (Sep 09 2021 at 23:47):

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

Mario Carneiro (Sep 09 2021 at 23:49):

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 (Sep 09 2021 at 23:53):

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


Last updated: Dec 20 2023 at 11:08 UTC