Recordings of porting meetings wanted

Stream: general

[Shreyas Srinivas]

Joachim Breitner said:

Next office hour in 53 mins! http://meet.google.com/sbx-djnu-wyo

Do we still have the recordings of the mathlib porting meetings we had three years ago?

[Shreyas Srinivas]

I am looking for the meeting where we declared the mathlib port complete.

[Shreyas Srinivas]

around June-July 2023 as I recall

[Shreyas Srinivas]

I believe those meetings morphed into the office hours we have today, which is why I am asking here.

[Shreyas Srinivas]

I recall @Matthew Ballard was the host of these meetings

[Shreyas Srinivas]

I can explain in DM why I am looking for this specific meeting recording if anyone from that meeting wants to know

[Ashley Blacquiere]

The oldest recording that we have is from Oct. 2023: Mathlib Community Meeting playlist

[Matthew Ballard]

I don't think I hosted porting meetings

[Matthew Ballard]

Though I happily participated!

[Mario Carneiro]

I think I hosted most of them

[Matthew Ballard]

I took up the semi-monthly community meetings a bit after

[Mario Carneiro]

It was on a different link than the office hours, I think it was zoom

[Shreyas Srinivas]

If you have a recording of the last port meeting (where we declared it complete) and could share it with me, I'd be super grateful.

[Mario Carneiro]

that was on my CMU zoom account, I have no idea if I still can access it

[Shreyas Srinivas]

were they posted on youtube? I recall some meetings were

[Mario Carneiro]

maybe

[Mario Carneiro]

if so they won't be on my persoonal youtube acct, they will be on leanprover-community

[Shreyas Srinivas]

Found the recording link you posted, but sadly it says the recording doesn't exist anymore : #mathlib4 > Mathlib4 porting meeting series @ 💬