Office hours

Stream: general

[Kim Morrison]

A reminder that we're holding another office hours right now! (me and Leo)

[Joachim Breitner]

Office ours happening right now, come and ask your questions. https://meet.google.com/sbx-djnu-wyo

[Kim Morrison]

Office hours with me and (probably?) Leo, at 2024-03-21T09:00:00+11:00!

https://meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Office hours with Leo and me starting now! https://meet.google.com/sbx-djnu-wyo

[Notification Bot]

4 messages were moved here from #announce > Lean FRO by Sebastian Ullrich.

[Leonardo de Moura]

Office hours with @Mac Malone and me today at 2024-04-03T14:00:00-07:00 https://meet.google.com/sbx-djnu-wyo
Questions about Lean, Std, and roadmap are also welcome.

[Mario Carneiro]

Just an FYI, I and probably others at CMU frequently cannot make these office hour meetings because they overlap with the weekly hoskinson center meetings. If you can vary the day as well as the time that would be helpful. (It's also fine if you can't)

[Kim Morrison]

Good to know, we'll see what we can do.

[Kim Morrison]

Sorry about the late message, but a reminder that we'll hold FRO office hours in a moment, at 2024-04-18T07:00:00+10:00.

[Kim Morrison]

meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Next office hours starting in one hour, 2024-04-24T17:00:00+02:00 at http://meet.google.com/sbx-djnu-wyo!

[Joachim Breitner]

At last week’s office hours someone had a very nice example of code that elaborated quickly when using some tactic, but was slow when using the explicit term as produced using show_term using the (heq ▸ h) notation (due to a well-founded recursive function being unfolded). I was hoping to see this example in an issue, but they didn’t report it yet. If you are this person, I’d still appreciate seeing this code!

[Leonardo de Moura]

Office hours today at 2024-05-01T14:00:00-07:00
Link: http://meet.google.com/sbx-djnu-wyo

[Rida Hamadani]

Joachim Breitner said:

At last week’s office hours someone had a very nice example of code that elaborated quickly when using some tactic, but was slow when using the explicit term as produced using show_term using the (heq ▸ h) notation (due to a well-founded recursive function being unfolded). I was hoping to see this example in an issue, but they didn’t report it yet. If you are this person, I’d still appreciate seeing this code!

Tagging @Somo S. because I was in that meeting 2 weeks ago and I remember that the person who presented this has the same username.

[Somo S.]

Rida Hamadani said:

Joachim Breitner said:

At last week’s office hours someone had a very nice example of code that elaborated quickly when using some tactic, but was slow when using the explicit term as produced using show_term using the (heq ▸ h) notation (due to a well-founded recursive function being unfolded). I was hoping to see this example in an issue, but they didn’t report it yet. If you are this person, I’d still appreciate seeing this code!

Tagging Somo S. because I was in that meeting 2 weeks ago and I remember that the person who presented this has the same username.

Thanks for tagging me @Rida Hamadani I was indeed the person that posed that issue.
Sorry I have taken a while to post the issue @Joachim Breitner. I have been travelling.

I have posted the issue here Elaboration of explicit term proof significantly slower than equivalent tactic proof · Issue #4051 · leanprover/lean4 (github.com)

[Joachim Breitner]

Much appreciated!

[Joachim Breitner]

mainly 4.7.0 .. (on 4.8.0-rc1, all results above were consistently about 1 or 2seconds slower)

Oh wey :-)

[Somo S.]

my pleasure @Joachim Breitner .. :smile:

[Steven Clontz]

I'm 90% of the way towards addressing this todo, but keep bumping againt issues related to types when using the Countable property (e.g. this question). I'm sure the fix is obvious to more experienced contributors; are these office hours the best way to get synchronous support from the community?

[Jireh Loreaux]

For Mathlib-related things, you may have better luck asking for direct support from some Mathlib maintainers / contirbutors. This isn't to throw shade on the FRO, only that depending on who is hosting the office hours, they may be more (e.g., Kim Morrison ) or less (e.g., Mac Malone) familiar with the inner workings of Mathlib. I'd be happy to help you a bit tomorrow one-on-one if you're available then.

[Sebastian Ullrich]

Today's office hours starting in one hour, 2024-05-08T17:00:00+02:00 at http://meet.google.com/sbx-djnu-wyo!

[Steven Clontz]

Jireh Loreaux said:

For Mathlib-related things, you may have better luck asking for direct support from some Mathlib maintainers / contirbutors. This isn't to throw shade on the FRO, only that depending on who is hosting the office hours, they may be more (e.g., Kim Morrison ) or less (e.g., Mac Malone) familiar with the inner workings of Mathlib. I'd be happy to help you a bit tomorrow one-on-one if you're available then.

Thanks Jirah - I'm running http://iuse.clontz.org this week but plan to get back into Lean mode next week. I got my goals closed, but I want to do a bit more refactoring before I bug you directly. :smile:

[Brandon Harad]

Is there anywhere I can see the schedule for office hours in advance? I desperately want to attend, but keep only seeing these messages after they conclude.

[Jireh Loreaux]

@Brandon Harad https://lean-fro.org/events/

[Kim Morrison]

A reminder of tomorrow's Lean FRO office hours at 2024-05-16T07:00:00+10:00 in http://meet.google.com/sbx-djnu-wyo.

[Kim Morrison]

A reminder of the next Lean FRO office hours at 2024-05-23T01:00:00+10:00 in http://meet.google.com/sbx-djnu-wyo.

[Sebastian Ullrich]

Today's office hours starting in one hour, 2024-06-05T17:00:00+02:00, at http://meet.google.com/sbx-djnu-wyo!

[Somo S.]

Sebastian Ullrich said:

Today's office hours starting in one hour, 2024-06-05T17:00:00+02:00, at http://meet.google.com/sbx-djnu-wyo!

I guess it ended early today?

[Sebastian Ullrich]

Yes, we ran out of questions early :)

[Kim Morrison]

Sorry for the late notice: office hours about to start!!

[Sebastian Ullrich]

Today's office hours starting in 10min(!) at http://meet.google.com/sbx-djnu-wyo!

[Henrik Böving]

Office hours in half an hour 2024-06-26T23:00:00+02:00 @ http://meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Next office hours in 15min at http://meet.google.com/sbx-djnu-wyo!

[Henrik Böving]

Next office hours in 5min at http://meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Next office hours in 20min at http://meet.google.com/sbx-djnu-wyo!

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Kim Morrison]

Office hours are moving, and will now be regularly at:

• 2024-08-22T09:00:00+10:00 every "even" week (i.e. this week and then every two weeks)
• 2024-08-29T01:00:00+10:00 every "odd" week (i.e. next week and then every two weeks)

There is a google calendar showing these events at that will remain updated.

[Kim Morrison]

meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Next office hours in 15min at http://meet.google.com/sbx-djnu-wyo!

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Kim Morrison]

Next office hours in 20 minutes at http://meet.google.com/sbx-djnu-wyo

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Alexandre Rademaker]

Not sure where to ask about the office hours. Did we have it yesterday?

[Notification Bot]

A message was moved here from #announce > Lean FRO by Riccardo Brasca.

[Riccardo Brasca]

@Alexandre Rademaker I've moved you message to this stream. We try to keep the "announce" stream only for announcements, not for discussion.

[Riccardo Brasca]

(but no worries)

[Alexandre Rademaker]

The question above is just to confirm if https://lean-fro.org/events/ is updated

[Kevin Buzzard]

Perhaps off-topic: FWIW I'm certainly expecting a mathlib community meeting on the 11th (i.e. it's listed on the calendar of events and it's happening AFAIK).

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Yuri]

Sebastian Ullrich said:

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

I had to drop off. I will try to join the next one.

[Kim Morrison]

Just noting that with daylight savings changes in both hemisphere, we are moving one of the office hours.

• Next week (this one is unchanged) will be 2024-10-24T02:00:00+11:00 (and then biweekly).
• The week after will be 2024-10-31T09:00:00+11:00 (and then biweekly).

These changes are reflected at https://lean-fro.org/events/.

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Kim Morrison]

Next office hours starting now!

[Sebastian Ullrich]

Next office hours in 1hr at http://meet.google.com/sbx-djnu-wyo!

[Kim Morrison]

Office hours starting now!

[Sebastian Ullrich]

Next office hours about to start!

[Martin Dvořák]

Office hours are AWESOME. I wonder why there aren't more people.

[Somo S.]

i usually try to attend every one, even when i have no question. If anything, its been a good way for me to socialize in sync about lean when i am otherwise completely isolated

[Brandon Harad]

Personally, I often don't have time during the day to attend. This is definitely not fixable, but I imagine that's the main reason.

[Edward van de Meent]

personally, i have yet to attend one because i didn't have a question that is so important/difficult that the FRO needs to be involved... i guess i should try and attend next time just to get an idea what it's all about...

[Edward van de Meent]

Edward van de Meent said:

so important/difficult that the FRO needs to be involved

as in, any question i have can typically be easily resolved on Zulip

[Shreyas Srinivas]

Edward van de Meent said:

personally, i have yet to attend one because i didn't have a question that is so important/difficult that the FRO needs to be involved... i guess i should try and attend next time just to get an idea what it's all about...

Same. It seems to me that it is unfair to bother the FRO with the kind of questions I have. Either they are the sort that can be answered in a few hours of debugging or asking on Zulip, or they tend to be of the moonshot variety.

[Yuri]

Martin Dvořák said:

Office hours are AWESOME. I wonder why there aren't more people.

I’ve been meaning to attend for a while, but something else always seems to come up.

The one time I was able to join briefly, I noticed that some of the questions were quite specific and didn’t seem like the best use of Lean FRO’s time. Many of those answers could have been found here on Zulip with a bit of searching.

I’ve been following the development commits as closely as possible, but at times, the issues can be a bit unclear in terms of their motivation or strategic significance, if any. I am aware that some of this is caused by my lack "theorem proving" experience.

It would be great if these office hours could include some (informal) clarification on recent, major developments in the repository. This would provide insight into a more detailed roadmap (as opposed to the high-level one on the Lean FRO site), which feels somewhat opaque at the moment—or maybe I’m just not looking in the right places?

[Alexandre Rademaker]

I try to attend all when I don’t have conflicts, I have learn tricks with questions from others.

[Julian Berman]

I also try to attend these and learn things.
For those of you saying you wouldn't want to waste the FRO's time with your question, which is a sentiment I definitely get -- the hour happens no matter what, and often it's just sat in silence if there's no questions. So I wouldn't personally think you (hypothetical you) were wasting anyone's time with asking anything, Sebastian's generally graciously waiting there no matter what.

[Joachim Breitner]

Yuri de Wit said:

It would be great if these office hours could include some (informal) clarification on recent, major developments in the repository. This would provide insight into a more detailed roadmap (as opposed to the high-level one on the Lean FRO site), which feels somewhat opaque at the moment—or maybe I’m just not looking in the right places?

You are certainly welcome to join and ask these questions there! It’s true that we don't all comprehensively publicly communicate all the plans, and every change of plans (and that would be significant amount of work), but we don’t want to be secretive, so asking is fine – including during office hours

[Mario Carneiro]

TBH I think this would be a better use of the hour than answering zulip questions

[Ashley Blacquiere]

Martin Dvořák said:

Office hours are AWESOME. I wonder why there aren't more people.

I guess most folks on the Discord are here too, but repost the weekly Office Hours announcement, just in case?

[Kim Morrison]

Office hours in 5 minutes!

[Ching-Tsun Chou]

How does one join office hours?

[Ruben Van de Velde]

Perhaps http://meet.google.com/sbx-djnu-wyo

[Ching-Tsun Chou]

Thanks!

[Edward van de Meent]

Martin Dvořák was right, office hours are awesome.

[Violeta Hernández]

Honestly I just haven't had any questions that I felt asking. But I'll make an effort to still join future office hours :smile:

[Kim Morrison]

A reminder that the next office hours will be at 2024-12-12T09:00:00+11:00 in http://meet.google.com/sbx-djnu-wyo. This will be the last one for 2024.

[Marcus Rossel]

Are the office hours happening today? The Lean FRO events calendar shows an event right now.

[Kim Morrison]

(Apologies we were a bit late! Eventually we got there, and my alarms are back on post-holidays. :-)

[Ashley Blacquiere]

Due to Lean Together, regular office hours (originally scheduled for 2025-01-15T08:00:00-08:00) have been canceled this week and removed from the calendar.

[Henrik Böving]

Office hours @ https://meet.google.com/sbx-djnu-wyo for the next hour!

[Henrik Böving]

Office hours @ https://meet.google.com/sbx-djnu-wyo

[Ashley Blacquiere]

Office hours are cancelled this week. See you again at 2025-02-19T14:00:00-08:00!

[Kim Morrison]

Office hours in 25 minutes!

[Sebastian Ullrich]

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

[Kim Morrison]

Next office hours starting in a few minutes!

[Kim Morrison]

Next office hours starting in 15 minutes: http://meet.google.com/sbx-djnu-wyo

[Kim Morrison]

Office hours starting in 5 minutes.

[Sebastian Ullrich]

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

[Ashley Blacquiere]

Due to recent daylight savings time changes, office hours are moving, and will now be regularly scheduled as follows:

• 2025-04-16T16:00:00-07:00, this week and every "even" week (i.e. this week and then every two weeks)
• 2025-04-23T08:00:00-07:00, this week and every "odd" week (i.e. next week and then every two weeks)

We'll retain this pattern through the end of daylight savings time in ~Oct. There is also an iCal that you can subscribe to!

[Kim Morrison]

A reminder there will be office hours in 15 minutes, at http://meet.google.com/sbx-djnu-wyo.

[Sebastian Ullrich]

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

[Kim Morrison]

Office hours at 2025-05-01T00:00:00+01:00 http://meet.google.com/sbx-djnu-wyo.