Meetings with Leo

Stream: lean4

[Mario Carneiro]

During his talk, @Leonardo de Moura mentioned that he prefers face to face meetings over zulip discussion, and could perhaps spend 1-2 hours per week on such meetings. I think that we should try to coordinate this as a regular meeting that we can all plan to attend or not as our schedule permits. I think that smaller and more regular communication will be a very good thing for keeping the lines open and moving the port along, and we can set up an agenda beforehand based on problems that have come up on zulip during the week. I am inspired in part by the Rust project team meetings, that often start with some triage of issues that have popped up on the tracker or reports on ongoing work. For the time being I don't think we need anything so formal as that, but being able to collect all the random issues folks come up with and present them in a short time span seems like a good use of time.

[Leonardo de Moura]

Yes, I am happy to meet every week for 1 - 2 hours.
Early in the morning (7 am PST) is best for me because it would never collide with MSR meetings.

[Jalex Stark]

Leo, do you want this to be a group meeting that you "run" or that someone else "runs" in consultation with you?

[Leonardo de Moura]

@Jalex Stark It would be great if the mathlib devs "run" it and start the meetings describing the most pressing issues. I am happy to listen, discuss potential solutions, and answer questions.

[Johan Commelin]

For the Europeans: 7 am PST is 16:00 CET (Paris, Berlin, Amsterdam)

[Jalex Stark]

Leo, does Tuesday Jan 12 at 0700 PST = 1000 EST = 1600 CET work for you? I'm happy to show up and take meeting minutes.

[Rob Lewis]

The mathlib maintainers will set something up soon. I suspect this Tuesday is too soon. But 7am PST seems like the ideal time slot.

[Jalex Stark]

"too soon" by days or weeks?

[Jalex Stark]

I'd urge against trying to have too much of an agenda / delaying by being too formal. It would be fine if all that happened at the meeting is that Leo explains some design decisions or people talked about half-formed thoughts about mathlib porting.

[Mario Carneiro]

The problem that I would like to solve with these meetings is that Zulip is a firehose of mostly-irrelevant information for Leo, and this meeting is a good way to distill that information down to the things that are in his jurisdiction. Leo likes to be able to work for long stretches without interruption, and this arrangement makes it easy to still talk about the important things, but it requires compressing a lot of stuff into a short span and that requires some discipline. I think if we fill the meeting with half formed thoughts about porting, we won't have the time to get to everything we need to and will start hunting for additional time outside the meetings.

[Jalex Stark]

For sure it would be bad to waste anyone's time with a bad meeting. It sounds like you're thinking about this in a sane way and I will now refrain from pushing any particular opinions about how this meeting should be organized. I just want to highlight that it's important for the norms of a fixed meeting to evolve with time, and the data you get from the lived experience of meeting $n$ is very useful for informing the norms that should be set for meeting $n + 1$, especially at $n = 0$.