Mathlib community meeting

Stream: Equational

[Matthew Ballard]

The next community meeting will be 2024-10-18T10:00:00-04:00 instead of today.

I want to particularly invite everyone involved here to join to share their perspectives on how Mathlib's current design helped or hurt their goals. Insights from projects like this are valuable for future growth of the community.

A link to the meeting will be provided closer to the appointed time.

[Matthew Ballard]

Please feel free to use this thread to brainstorm :)

[Shreyas Srinivas]

I think we need to figure out how much of Mathlib we used in the first place

[Shreyas Srinivas]

We basically reinvented the meta theory of Free Magmas

[Shreyas Srinivas]

Further, we avoided using the Mul typeclass in favour of our own Magma typeclass

[Shreyas Srinivas]

And another thing: this is not mathlib specific, but we found that overriding the function composition notation increased CI time considerably and it was simpler to use a previously unused symbol

[Shreyas Srinivas]

One pain point w.r.t. Mathlib was finding notation that was not already used and globally visible. I personally wish that we could freely import Mathlib without worrying about having to find out which notations are globally imported. What I mean is, it would be nice to be able to "hide" notations imported from mathlib in general, but at least namespacing and localising most notations would already help

[Matthew Ballard]

Reminder for 2024-10-18T10:00:00-04:00. Please join! See #general > Mathlib community meetings for more details.

[Michael Bucko]

Shreyas Srinivas schrieb:

What I mean is, it would be nice to be able to "hide" notations imported from mathlib in general, but at least namespacing and localising most notations would already help

Just a note, perhaps custom typeclasses with lazy evals (deferring certain operations until their results are needed) could help? Also, perhaps some sort of next-level scoping is needed for such projects, too? (to avoid the CI time increase you mentioned).

[Shreyas Srinivas]

I don't think laziness helps in anyway with notation. There are ways to explicitly provide scope like using namespaces and local notations. Mathlib already uses them (there is the BigOperators namespace for example)

[Shreyas Srinivas]

Long term, it would really help if all of Mathlib was namespaced. Lean already allows us to open a namespace with only the items we need

[Eric Wieser]

But I think scoping everything in mathlib would be unnecessarily hostile to mathematicians; while it's sometimes annoying that mathlib is in the way, a tool to move things back out of the way would be enough to make everyone mostly happy, as you said here:

Shreyas Srinivas said:

it would be nice to be able to "hide" notations imported from mathlib in general,

[Shreyas Srinivas]

Well mathematicians can just open Mathlib without any qualifications.

[Eric Wieser]

(deleted)

[Matthew Ballard]

Please come have this discussion over video :)

[Eric Wieser]

I think video + audio would be a little easier!

[Matthew Ballard]

That can be managed :)