Mathlib community meetings

Stream: general

[Kim Morrison]

As just announced, we are rebooting community meetings. (We previously ran these regularly during the porting proceess.)

[Kim Morrison]

The first meeting will be at 2024-02-10T02:00:00+11:00 at https://meet.google.com/guj-dcde-cdq, and the intention will be to continue every second month on the 2nd Friday. Note that these meetings will be alternating with the FRO month meetings, which are focussed more on language development and the work of the Lean FRO.

The meetings will be recorded, and posted online afterwards.

(Of course, if we discover there is demand for more frequent meetings, we can do that too!)

[Kim Morrison]

In planning these meetings, we would like to balance two things:

• Ensuring that community requests and concerns are heard and addressed.
• Staying on topic and avoiding long digressions --- these will be relatively large meetings so we can't waste people's time.

While we would like to keep these meetings fairly informal, these constraints mean that we will need an agenda. To the extent that a moderator is required, there'll be someone from the maintainers handling each meeting.

[Kim Morrison]

I'll post a poll shortly with suggestions of general topics for discussion. (We've already discussed this a bit amongst the maintainers.) Ideally in future we'll keep doing such a poll for each meeting, to try to make sure everyone has a say in what these meetings cover. Please feel free to use this thread to expand on topics, suggest subtopics, etc. But let's not have this thread become actual discussion of the topics! :-)

[Kim Morrison]

/poll Discussion topics for February Mathlib community meeting

[Eric Wieser]

Was a recording made of this meeting?

[Sebastian Ullrich]

No, but we can do so next time if people are in favor

[Eric Wieser]

Ah, so I guess

Scott Morrison said:

The meetings will be recorded, and posted online afterwards.

wasn't true this time

[Adam Topaz]

Indeed a recording would have been nice, as I had to miss this meeting due to teaching (and thus will probably miss the future ones during this semester).

[Michael Rothgang]

Similar here: I would have loved to watch a recording later.

[Kim Morrison]

Sorry, yes, absolutely meant to. At the last moment I discovered I couldn't open the meeting and Sebastian or Leo needed to, and then in the rush I forgot to record. Next time!

[Kim Morrison]

To get the ball rolling for future meetings, the default date would be 2024-04-13T00:00:00+10:00, after the next FRO community meeting at 2024-03-09T02:00:00+11:00.

[Kim Morrison]

I was wondering if in the meantime we might be interested in holding a "review party".

I was thinking a coordinated time, a zoom room possibly with some breakout rooms for subject areas, and participants do any combination of

• improving editorial processes (tracking slow PRs, auto-recommendation of reviewers, maybe even trying out editflow!)
• assigning PRs to potential reviewers
• closing, reviewing, and marking PRs as awaiting-author.

[Kim Morrison]

(I'll take thumbs up on that message as interest; if it's something enough people might participate in, we can move in to scheduling. Please refine the proposal below, too!)

[Eric Rodriguez]

One thing that was briefly mentioned last meeting and I think would be good to raise again next meeting is proof golfing. It's hard to say as sometimes it's stylistic changes that are only positive, and then sometimes it's huge compressions that most people would perceive as negative.

[Martin Dvořák]

My favorite example of huge proof compression:
https://github.com/leanprover-community/mathlib4/blob/a24907839ba28f0009af978642d62e1cc3076038/Mathlib/Data/List/Basic.lean#L2493

[Michael Rothgang]

Cross-linking the April edition since I at least would have looked in this thread.

[Jireh Loreaux]

oops, I didn't realize there were two threads, sorry!

[Matthew Ballard]

The next installment of the Mathlib community meetings will be 2024-08-09T10:00:00-04:00 in a little under three weeks. All are welcome!

As the agenda is being assembled, I want to encourage you to post here to highlight issues or questions of importance to you. If you prefer, you can also DM me or any maintainer of Mathlib.

[Matthew Ballard]

Much apologies for the late notice. But the next community meeting will be 2024-10-18T10:00:00-04:00 instead of today.

I want to particularly invite people involved in the #Equational project to share their perspectives on how Mathlib's current design helped or hurt their goals.

[Michael Rothgang]

This is/will be the correct link, right? https://meet.google.com/guj-dcde-cdq

[Matthew Ballard]

Reminder that the community meeting will be in 1 hour 2024-10-18T10:00:00-04:00 . The general theme is building on top of mathlib. We have a lot of interesting projects that have recently completed or are on going. I encourage anyone involved in one of them to join and share their perspectives.

[Damiano Testa]

Will the meeting be recorded? I won't be able to attend, but would be curious to hear about what is going on!

[Matthew Ballard]

Michael Rothgang said:

This is/will be the correct link, right? https://meet.google.com/guj-dcde-cdq

Tentatively. If not, I will post a different link 10 minutes before the start.

[Matthew Ballard]

It will be at https://sc-edu.zoom.us/j/89485684468 (~ 10 minutes)

[Eric Wieser]

The claim I made in the meeting was wrong, priority really does win:

import Mathlib

notation "x" => 1
notation (priority := default+1) "x" => "1"

#eval (x : Nat) -- doesn't work, even though the low-priority one would work

[Shreyas Srinivas]

I want to add that channeling contributions at the task proposal stage has the benefit that contributors haven't already sunk formalisation effort before duplicates have been spotted.

[Matthew Ballard]

Thanks to everyone who came! I learned a good deal. The next one will come in December with more information appearing closer to the date.

[Kevin Buzzard]

Apologies -- I couldn't make this one (I was interviewing) but I had not realised that people involved in interesting projects were specifically being asked things (indeed I didn't read the message above about this because I was interviewing :-) ). Let me know if there's any questions which you just want me to hit R and say something about re FLT.

[Matthew Ballard]

Reminder that the next Mathlib community meeting will be 2024-12-13T10:00:00-05:00 at https://meet.google.com/guj-dcde-cdq All are welcome!

[Matthew Ballard]

Reminder that this will start in a little less than 50 minutes. Hope to see you there.

[Kim Morrison]

How did the meeting go? What was discussed?

[Kevin Buzzard]

And is the recording available?

[Michael Rothgang]

There was the plan of turning a transcript of the meeting into a community blog post, right? (I still think that would be great.)

[Ashley Blacquiere]

Kevin Buzzard said:

And is the recording available?

Yes! I just uploaded it to the Lean FRO channel on YouTube (HD is still processing as I write this, but SD should be available to view).

Kim Morrison said:

How did the meeting go? What was discussed?

Main topics were big wins from 2024 and hopes for Mathlib in 2025.

Michael Rothgang said:

There was the plan of turning a transcript of the meeting into a community blog post, right? (I still think that would be great.)

I have the transcript and can share if anyone would like to use it to create a blog post. Given the meeting topic, it'd be a great source for a 2024 wrap-up post.

[Matthew Ballard]

Summaries of the two main topics at #general > Highlights of 2024? and #general > Predictions for 2025? Please contribute!

[Matthew Ballard]

Our next community meeting will be tomorrow 2025-02-14T10:00:00-05:00 Please join us!

[Matthew Ballard]

Please join! Happening now!

[Matthew Ballard]

https://meet.google.com/guj-dcde-cdq

[Kim Morrison]

Anyone want to give a brief summary or recap?

[Ashley Blacquiere]

I have the recording and transcript! Haven't posted it yet, but coming soon.

[Ashley Blacquiere]

Today's Mathlib Community Meeting recording is live on YouTube.

[Kim Morrison]

Many interesting discussions (I'm just part way through).

[Kim Morrison]

The desire to have a good auto-formatter is of course reasonable! It's also very hard because of Lean's extensibility. We really want to get there but it doesn't seem likely to happen immediately!

In the meantime, can we just start linting for all the most common errors? (Spaces around colons and parentheses, for example.)

[Kim Morrison]

It's really important that reviewers don't have to do this.

[Damiano Testa]

I can look into toning down the ppRoundtrip linter, so that it can reliably check something.

[Damiano Testa]

It is already not too bad, but it flags way too much and not everything is good.

[Damiano Testa]

I can probably start by making it look at binders.

[Michael Rothgang]

I could probably whip up a text-based linter for e.g. the spacing issues. It would be less reliable than the pretty-printer based logic, but could also be useful.

[Damiano Testa]

There was already an experiment with linting whitespace: #14379.

[Damiano Testa]

While trying to get a reasonable number of exceptions with the linter, #22006 contains a few easy whitespace cleanups.

[Arthur Paulino]

As a data point reference, cargo fmt doesn't attempt to format everything. In particular, it usually skips macro syntax.

Though I'm not sure it would be very satisfying for Mathlib in particular because the vast majority of lines are within the tactic DSL. So in a sense it's what cargo fmt would skip, if we apply the analogy.

Tossing an idea in case it helps: syntax authors could provide an optional API to format the syntax they create, which would be ultimately called by lake fmt. Otherwise, output the same original string of text.

[Eric Wieser]

In theory, syntax already has such an API, in the form of instructions to the pretty printer

[Damiano Testa]

In fact, the pretty-printed syntax is what the ppRoundtrip linter uses.

[Damiano Testa]

Here is a source of many discrepancy between the pretty-printed syntax and actual mathlib code: is it

theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
    (w : { w : InfinitePlace K // w ≠ w₀ }) :

or

theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1)
    (w : {w : InfinitePlace K // w ≠ w₀}) :

(note the spaces around the brackets).

[Damiano Testa]

The pretty-printer makes a choice. However, for situations such as the one above, I am not so sure that enforcing either convention is clearly the way to go.

[Damiano Testa]

And special-casing all situation such as the one above is a lot of work! :smile:

[Damiano Testa]

Not to mention, the situations where the pretty-printed syntax is either invalid or valid but not defeq to the original!

[Arthur Paulino]

I didn't know that pretty-printed syntax could possibly not be defeq to the original source. That's pretty scary.

Regarding convention, the convention is usually whatever the auto-formatter picks. It's automatic anyway

[Damiano Testa]

A common source of non-defeq comes from casts/type ascriptions.

[Eric Wieser]

@Damiano Testa, I think you're confusing delaboration (Expr -> Syntax) with pretty printing (Syntax -> Std.Format)

[Eric Wieser]

Syntax -> String can also be ambiguous, but I think you need something more pernicious than coercions to trigger it

[Damiano Testa]

Eric, yes, I did confuse delaboration with pretty-printing!

[Damiano Testa]

#22051 removes more whitespace inconsistencies (and some missing . and typos).

[Damiano Testa]

The bulk of the changes are to make sure that doc-strings start with /-- and end with -/ -- emphasis on the spaces!

[Matthew Ballard]

Our next Mathlib community meeting will at be at 2025-04-11T10:00:00-04:00. Please join us on Google Meet https://meet.google.com/guj-dcde-cdq !

[Matthew Ballard]

Reminder: this is happening in 5!