1st Lean Dev Update Meeting

Stream: lean4

[Leonardo de Moura]

We are planning to have monthly dev update meetings from now on :)
The goal of these meetings is:

• Announce new features.
• Introduce new team members. Please come and meet @Sarah Smith our new program manager.
• Explain our roadmap.
• Get feedback from you!

Time: 2022-06-15T08:00:00-07:00
We will be using Microsoft Teams.
You can join on your computer or mobile app using the link: https://teams.microsoft.com/l/meetup-join/19%3ameeting_MWRhYjgzZjgtOTFmNy00MzllLWFkMjctYjg3MDliMTI1MTA1%40thread.v2/0?context=%7b%22Tid%22%3a%2272f988bf-86f1-41af-91ab-2d7cd011db47%22%2c%22Oid%22%3a%2255de0542-d78b-4cde-913e-65215a57d62d%22%7d

We are looking forward to seeing you all there.

[John Burnham]

Just to clarify, these meetings are open for anyone in the community to attend? And is that 11am Pacific Time?

[Julian Berman]

I assume yes for the former given it was shared here publicly, but for the latter, you actually see the time in your own time zone (so it's 11 ET here which I assume you're in too.)

[John Burnham]

Oh, I see, the date has localization, thanks!

[Leonardo de Moura]

John Burnham said:

Just to clarify, these meetings are open for anyone in the community to attend? And is that 11am Pacific Time?

Yes, they are open to anyone :)

[Leonardo de Moura]

Thanks to everybody that joined the meeting today.
We would love to hear suggestions on how to make these meetings more effective in the future. Please post your ideas here. Thanks!

[Arthur Paulino]

First idea that comes to my mind is a platform for people to post questions without needing to worry about the visibility on the (tight) chat widget

[Henrik Böving]

I couldn't make it today sadly, will there be a recording? If not that's my suggestion :p

[Leonardo de Moura]

Arthur Paulino said:

First idea that comes to my mind is a platform for people to post questions without needing to worry about the visibility on the (tight) chat widget

We will try to find a better platform. Any suggestions?

[Leonardo de Moura]

Henrik Böving said:

I couldn't make it today sadly, will there be a recording? If not that's my suggestion :p

Great suggestion. My mistake. I completely forgot to press the record button :( I will make sure I do not forget next time.

[Arthur Paulino]

Leonardo de Moura said:

We will try to find a better platform. Any suggestions?

sli.do is a rather common pick

[Mario Carneiro]

How about a stream?

[Mario Carneiro]

public but not default subscribed

[Arthur Paulino]

Mario Carneiro said:

How about a stream?

How can a stream handle the level of interactivity that a meeting offers? From what I understood, it's desirable that audience members can jump in and speak out too

[Mario Carneiro]

Rust does all its meetings over zulip

[Mario Carneiro]

but I think it would work even if it is hybrid with a zoom meeting for the presenter

[Mario Carneiro]

it will be harder to follow after the fact though if it's not entirely on one platform

[Mario Carneiro]

one way around that would be for the presenter to put zulip questions on screen while answering them

[Mario Carneiro]

so that way you would get the full experience if you watched it after the fact

[Julian Berman]

Perhaps another small suggestion is publishing the meetings to a (subscribeable) calendar. I completely forgot about it :P

[Gabriel Ebner]

Mario Carneiro said:

How about a stream?

Or even just a topic in the #lean4 stream. That is great for visibility of the meeting, and the chat log is easily accessible for later reference. I'm happy whenever a conference has a hybrid zulip/zoom model.

[Mario Carneiro]

The main reason to avoid #lean4 stream is if the meeting notes are too disjointed to be useful by people who aren't participating. If it's just a once-a-month meeting which is expected to be of general interest then it's probably fine

[Henrik Böving]

Maybe we could have a separate stream with one topic per meeting where people can put in their questions? That way they would be more easily discoverable than when they are just yet another topic in #lean4

[Henrik Böving]

Ah mario already said that, silly scrolling.

[Siddhartha Gadgil]

Thanks for the meeting. I found it very helpful.
My two cents: I found Teams a very good platform for this (maybe familiarity having taught online at our Institute on Teams).

[Gabriel Ebner]

It might also be good to post the slides somewhere for future reference. (I hope I didn't miss a link somewhere.)

[Leonardo de Moura]

Gabriel Ebner said:

It might also be good to post the slides somewhere for future reference. (I hope I didn't miss a link somewhere.)

Great suggestion. They are available here: http://leanprover.github.io/talks/lean-update-2022-06-15.pdf

[Henrik Böving]

Leonardo de Moura said:

Gabriel Ebner said:

It might also be good to post the slides somewhere for future reference. (I hope I didn't miss a link somewhere.)

Great suggestion. They are available here: http://leanprover.github.io/talks/lean-update-2022-06-15.pdf

Since I'm seeing the "LeanInk + Doc-Gen4 + ???" there but couldn't attend, were there some suggestions regarding the ??? part?^^

[Leonardo de Moura]

@Henrik Böving I am very grateful you are already investigating this integration. When I wrote "???", my intention was "???" = "whatever the person leading the effort needs to do to make it awesome".

[Arthur Paulino]

Hey the next meeting is not going to be tomorrow, right? Just asking because the previous one was ~30 days ago

[Mac]

@Arthur Paulino No, Leo is planning on doing it after the ICERM after-party -- either the week of July 25, or first week of August.

[Arthur Paulino]

Alright, as I suspected. Thanks!