Zulip Chat Archive

Stream: lean4

Topic: Meetings with Leo


view this post on Zulip Mario Carneiro (Jan 06 2021 at 00:48):

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.

view this post on Zulip Leonardo de Moura (Jan 06 2021 at 01:01):

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.

view this post on Zulip Jalex Stark (Jan 06 2021 at 01:06):

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

view this post on Zulip Leonardo de Moura (Jan 06 2021 at 01:16):

@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.

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:40):

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

view this post on Zulip Jalex Stark (Jan 08 2021 at 18:37):

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.

view this post on Zulip Rob Lewis (Jan 08 2021 at 18:51):

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

view this post on Zulip Jalex Stark (Jan 08 2021 at 19:07):

"too soon" by days or weeks?

view this post on Zulip Jalex Stark (Jan 08 2021 at 19:08):

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.

view this post on Zulip Mario Carneiro (Jan 08 2021 at 20:10):

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.

view this post on Zulip Jalex Stark (Jan 08 2021 at 20:54):

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 n is very useful for informing the norms that should be set for meeting n+1 n + 1 , especially at n=0 n = 0 .


Last updated: May 07 2021 at 12:15 UTC