Monthly Community Meeting

Stream: general

[Leonardo de Moura]

Lean Focused Research Organization (FRO) - Monthly Community Meeting

Time & Date: 2023-10-13T07:00:00-07:00

Video call link: https://meet.google.com/guj-dcde-cdq
Or dial: ‪(DE) +49 40 8081616820‬ PIN: ‪222 556 634‬#
More phone numbers: https://tel.meet/guj-dcde-cdq?pin=3354363659596

Agenda:

I. Opening Remarks

II. Our Mission and Vision for Lean

• Overview of the mission statement
• Long-term vision for the Lean project

III. FRO Model and Structure

• Outline of the organization's structure
• https://www.convergentresearch.org/
• The Lean FRO team

IV. Development Philosophy

• Code Ownership
• Expectations around contributions and code quality

V. RFC (Request For Comments) and PR (Pull Request) Processes

• The lifecycle of an RFC and a PR
• How the community can contribute
• Key points of consideration during reviews

VI. Next Steps and Short Term Deliverables

• Upcoming milestones
• Key deliverables and expected timelines

VII. Q&A

• Open floor for questions, concerns, or suggestions from community members

[Ruben Van de Velde]

Sounds interesting - will there be a summary of the discussed points after the meeting?

[Eric Wieser]

Or a recording?

[Leonardo de Moura]

Good point. We will record the meeting.

[Leonardo de Moura]

We have updated the Google meet link above.

Google Meet joining info
Video call link: https://meet.google.com/guj-dcde-cdq
Or dial: ‪(DE) +49 40 8081616820‬ PIN: ‪222 556 634‬#
More phone numbers: https://tel.meet/guj-dcde-cdq?pin=3354363659596

[Leonardo de Moura]

Bump.

[Eric Rodriguez]

just to note for people interested, the meeting will start in 2 minutes

[Patrick Massot]

One thing I wanted to ask during the meeting but forgot: what happened to the plan of having compiled tactics? It originally was one of the promises of Lean 4 but, as far as I understand, it never became practicable and none of the heavy-lifting Mathlib tactic (ring, linarith, aesop...) is compiled.

[Jireh Loreaux]

I was teaching during the meeting, but I would very much appreciate a recording if it is available.

[Patrick Massot]

It was recorded, and I'm we'll get to know when the recording becomes available.

[Eric Wieser]

Note the Q&A was not recorded

[Matthew Ballard]

Sorry for the tardiness of my question in the chat. It might be better answered here anyway: what is envisioned for documentation for intermediate to advanced users to empower them to level up? (Number Blocks but with details about the unification algorithm in the place of arithmetic? :smile: )

[Mario Carneiro]

Currently the Lean Metaprogramming Book is the only general resource in that area. @David Thrane Christiansen @Arthur Paulino Should the FRO inherit maintainership of that book and/or extend it?

[Matthew Ballard]

That has been a wonderful reference!

[Mauricio Collares]

An alternative solution (which might be easier to implement, and which was inspired by Leo's recent podcast appearance) would be a reading list of papers relevant to understanding Lean's implementation. By that, I don't mean a non-awesome "awesome list" of all important papers ever, just the ones that provide most bang for the buck. In his interview, Leo mentioned it was very helpful to be able to ask people at MSR and SRI for such suggestions early in the project.

[Arthur Paulino]

Mario Carneiro said:

Should the FRO inherit maintainership of that book and/or extend it?

I'm not sure tbh. It depends on how David would like to do it, I think. That repo has a certain infra and it may not be the way he would want to maintain it.

My initial motivation was to get something started to empower metaprogrammers during the Mathlib port. Now that the port is done, it's possible that the Lean FRO members choose a different way. Or even prefer to start from scratch, using that book as a reference (or not). Either way is fine by me (as an author)

[Shreyas Srinivas]

can it become an mdbook? I have lost track of how many pdf copies I have downloaded.

[David Thrane Christiansen]

I've found that resource to be very valuable myself!

I don't yet have a clear plan - something that accomplishes it's goals will be a part of the manuals and tutorials that I'll be preparing, but I don't yet know if the current text is the right basis (or if the authors want us to take it over - it's their work!). As more is determined, I'll announce it.

[David Thrane Christiansen]

I could see a different structure being needed once we have a detailed reference manual, for instance.

[David Thrane Christiansen]

Or not!

[David Thrane Christiansen]

RE mdbook - the current plan is not to build everything with mdbook, but rather to build a Lean DSL for documentation. mdbook might be a targeted output format, though

[Mario Carneiro]

Maybe a reference manual is a better place to start then. How should that be structured? Should we focus on docstrings and leave the mdbooks to the more high level stuff?

[Mario Carneiro]

Regarding the doc DSL mentioned in the meeting, I think this is a cool idea but to me it's a lower priority than writing actual documentation text. I think we should try to organize a docs push powered by external contributors, the API surface area is huge and we need to ramp the work up to another scale.

[Mario Carneiro]

(This is not to say that they shouldn't be worked on concurrently, they require very different skill sets after all.)

[David Thrane Christiansen]

For API reference (docstrings), I think the "army of volunteers" is a good approach

[David Thrane Christiansen]

The plan is to port everything that's in an mdbook today to the new DSL, to reduce the fragmentation of the documentation ecosystem

[Mario Carneiro]

For the "army of volunteers" approach to work, we need to effectively communicate that those kind of PRs are welcomed and expedite PRs in that area (like lean4#2645). People are currently very afraid to open PRs, and justifiably so given the history, so we have to work hard to combat the impression that opening a PR burns social capital and the probability of the PR getting in is low

[Utensil Song]

Personally I would really love to see an integrated whole of what blueprint, mdBooks, doc-gen4, and LeanInk has offered. From informal goals, outlines to lemma API surface then to source and annotated goal states.

It would be really excited to see its seemless integration with Reservoir, that just write lean code and doc following a guide, then package index, CI, document publish are all taken care of.

[Eric Wieser]

One thing that might help is policy on how much documentation to contribute at once; the danger is that a PR adding 10 docstrings has a problem in one of them and then never gets merged

[Mario Carneiro]

8 people is not a lot if the goal is to build a language, but 8 maintainers can easily sustain an order of magnitude more work if they are shepherding work done by others. There is currently a large imbalance between the set of people able to meaningfully contribute and the set of people responsible for the work, which means that in the current situation the best way to speed up overall progress is for the people with the keys to less time making direct improvements and more time on reviewing work from the community. (And I say this as someone who has exactly this problem, working on things myself instead of reviewing for std4. But at least I have hopefully given people the right kind of impression to be motivated to submit work to std4.) This is basically exactly how mathlib4 got started, we were at 2 maintainers for a long time before we needed to grow the maintainer base. A comfortable ratio seems to be about 10-15 contributors per maintainer.

[Matthew Ballard]

At the same time, I think there is resource that other new languages don’t have. Mathlib contributors are large in number and very skilled. A sticking point is many come with a background somewhat orthogonal to software development. Making it easier for them to leverage their skill in mathlib to expertise with the core of Lean would unlock that resource.

[Kevin Buzzard]

I think that more mathematicians would write tactics if there was a document which did something like the following:

1) showed how to write a tactic which just chains some other tactics together (e.g. in the complex number game I prove $\mathbb{C}$ is a ring and every axiom is proved with intros; ext; simp; ring)
2) showed how to write a tactic which is just aesop with a specific simp set (e.g. can one write continuity this way?)
3) showed how to write assumption (note: this is the first time we have any meta code involved)
4) showed how to write Jeremy's first order logic tactic which he explains in the final chapter of "Programming in Lean", a resource which was written for a very early version of Lean 3 (a bunch of the code in there didn't even run in Lean 3.4.1) and which I can no longer find on the internet!

This would be an orthogonal approach to "in order to write tactics you must first learn about this gigantic monad heirarchy". I want to argue that the four examples above prove that this is not the case.

[Shreyas Srinivas]

You want tutorials. I agree. I think there is a thread about this already.

[Eric Wieser]

On the note of the gigantic monad hierarchy, it would be great if a version of https://github.com/leanprover-community/mathlib4/wiki/Monad-map was in the documentation somewhere

[Kevin Buzzard]

programming_in_lean.pdf

Here's my local copy of Programming In Lean. A document about Lean, never finished, last updated in 2016. This document taught me what a monad was. The last chapter is a very lucid explanation by I think @Jeremy Avigad on how to write a tableau prover for propositional logic.

[Jeremy Avigad]

Thanks for the kind words. Yes, that was me. I learned how to metaprogram in Lean 3 by writing finish, and then I wrote that around the same time.

[Marc Huisinga]

Mario Carneiro said:

8 people is not a lot if the goal is to build a language, but 8 maintainers can easily sustain an order of magnitude more work if they are shepherding work done by others. There is currently a large imbalance between the set of people able to meaningfully contribute and the set of people responsible for the work, which means that in the current situation the best way to speed up overall progress is for the people with the keys to less time making direct improvements and more time on reviewing work from the community. (And I say this as someone who has exactly this problem, working on things myself instead of reviewing for std4. But at least I have hopefully given people the right kind of impression to be motivated to submit work to std4.) This is basically exactly how mathlib4 got started, we were at 2 maintainers for a long time before we needed to grow the maintainer base. A comfortable ratio seems to be about 10-15 contributors per maintainer.

Just to provide a personal perspective (i.e. not representative for anyone else in the FRO): I'm slow at reviewing PRs and switching contexts greatly hurts my productivity. I would certainly not be able to sustain an order of magnitude of more work if all I did was shepherding work by others; my productivity may even decrease. People are very different in this regard.
My personal experience from previous software projects is also that a lot of people contributing to the same code base and then bailing to leave the maintenance work to others is really bad from a productivity perspective in the long term. And reviewing the code in such detail that you can maintain it as well as the person that originally wrote it is a lot of extra work vs. the person that wrote the code also being fully responsible for it in the future.

I also suspect that software is considerably more difficult to review than mathlib proofs where you can easily confirm that they state the correct definition or lemma and that the proof is correct. Style checking and such applies to both. Similarly, I consider maintaining a software library with well-defined APIs to be easier than maintaining a monolithic application.

Just to be clear: I'm only arguing against the case for a general massive increase in productivity here, not PRs in general (which are valuable for other reasons, too).

[Jireh Loreaux]

I think the army of volunteers proposal was primarily (only?) for documentation, but maybe I'm wrong.

[Sebastian Ullrich]

A recording of the presentation is now available at https://youtu.be/jaibFnoMDSw

[Miguel Marco]

Kevin Buzzard said:

I think that more mathematicians would write tactics if there was a document which did something like the following:

1) showed how to write a tactic which just chains some other tactics together (e.g. in the complex number game I prove $\mathbb{C}$ is a ring and every axiom is proved with intros; ext; simp; ring)
2) showed how to write a tactic which is just aesop with a specific simp set (e.g. can one write continuity this way?)
3) showed how to write assumption (note: this is the first time we have any meta code involved)
4) showed how to write Jeremy's first order logic tactic which he explains in the final chapter of "Programming in Lean", a resource which was written for a very early version of Lean 3 (a bunch of the code in there didn't even run in Lean 3.4.1) and which I can no longer find on the internet!

This would be an orthogonal approach to "in order to write tactics you must first learn about this gigantic monad heirarchy". I want to argue that the four examples above prove that this is not the case.

That would definitely help me. I would like to write a tactic that is basically iterating cases' as long as the created hypothesis are of type exists or and (that is, something like rcases but without having to give the nested structure). I haven't dared to try yet because it is not clear to me where to begin.

[Sebastian Ullrich]

Patrick Massot said:

One thing I wanted to ask during the meeting but forgot: what happened to the plan of having compiled tactics? It originally was one of the promises of Lean 4 but, as far as I understand, it never became practicable and none of the heavy-lifting Mathlib tactic (ring, linarith, aesop...) is compiled.

Good question. You might know that I put a great deal of effort into making such native compilation possible with zero setup. Today we mostly use this feature when creating executables, such as mathlib's cache. The last time I investigated this topic, the simple reason we didn't move forward was that we really didn't spend all that much time in the interpreter all in all (~10% afair). As precompiling a tactic is not free either, especially with the enormous dependency closure some important mathlib tactics have, optimization effort seemed better spent on other components first. It would be good to reevaluate this state after the recent significant optimizations have landed.

[Alex Kontorovich]

Sebastian Ullrich said:

A recording of the presentation is now available at https://youtu.be/jaibFnoMDSw

It's 29 seconds long...?

[Patrick Massot]

Kevin Buzzard said:

I think that more mathematicians would write tactics if there was a document which did something like the following:

1) showed how to write a tactic which just chains some other tactics together (e.g. in the complex number game I prove $\mathbb{C}$ is a ring and every axiom is proved with intros; ext; simp; ring)
2) showed how to write a tactic which is just aesop with a specific simp set (e.g. can one write continuity this way?)
3) showed how to write assumption (note: this is the first time we have any meta code involved)
4) showed how to write Jeremy's first order logic tactic which he explains in the final chapter of "Programming in Lean", a resource which was written for a very early version of Lean 3 (a bunch of the code in there didn't even run in Lean 3.4.1) and which I can no longer find on the internet!

This would be an orthogonal approach to "in order to write tactics you must first learn about this gigantic monad heirarchy". I want to argue that the four examples above prove that this is not the case.

Do you mean some Lean 4 port of https://leanprover-community.github.io/lean3/extras/tactic_writing.html?

[Ruben Van de Velde]

Alex Kontorovich said:

Sebastian Ullrich said:

A recording of the presentation is now available at https://youtu.be/jaibFnoMDSw

It's 29 seconds long...?

Huh, it was half an hour when I looked at it before

[Matthew Ballard]

I think tactics are essential but I was thinking more in terms of core itself. Sustainability becomes more feasible with a larger base who are knowledge about how the sausage is made.

[Henrik Böving]

Miguel Marco said:

Kevin Buzzard said:

I think that more mathematicians would write tactics if there was a document which did something like the following:

1) showed how to write a tactic which just chains some other tactics together (e.g. in the complex number game I prove $\mathbb{C}$ is a ring and every axiom is proved with intros; ext; simp; ring)
2) showed how to write a tactic which is just aesop with a specific simp set (e.g. can one write continuity this way?)
3) showed how to write assumption (note: this is the first time we have any meta code involved)
4) showed how to write Jeremy's first order logic tactic which he explains in the final chapter of "Programming in Lean", a resource which was written for a very early version of Lean 3 (a bunch of the code in there didn't even run in Lean 3.4.1) and which I can no longer find on the internet!

This would be an orthogonal approach to "in order to write tactics you must first learn about this gigantic monad heirarchy". I want to argue that the four examples above prove that this is not the case.

That would definitely help me. I would like to write a tactic that is basically iterating cases' as long as the created hypothesis are of type exists or and (that is, something like rcases but without having to give the nested structure). I haven't dared to try yet because it is not clear to me where to begin.

This thing in particular would be trivial if we had a match goal equivalent to Coq, you wouldn't even have to dive into meta code in order to do it, it could be a simple macro.

[Eric Wieser]

I think the best way to write such a macro is to use Qq, but then that means that the documentation no longer belongs in core...

[Bulhwi Cha]

Ruben Van de Velde said:

Huh, it was half an hour when I looked at it before

Perhaps something is going wrong with YouTube.

[Sebastian Ullrich]

Alex Kontorovich said:

Sebastian Ullrich said:

A recording of the presentation is now available at https://youtu.be/jaibFnoMDSw

It's 29 seconds long...?

:joy: Thanks for telling me! Since I clearly don't understand YouTube's editor, I've restored the uncut original.

[Arthur Paulino]

I watched it and it's AWESOME news all the way through :clap:

[josojo]

Thanks for uploading. Great to see what is all happening.

Could we also get the actual presentation linked? There are some links in the presentation that I wanna click on :)

[Utensil Song]

Some of these exciting links are:

• https://lean-fro.org/
• https://lean-lang.org/
• http://speed.lean-lang.org/ (note: not HTTPS)
• https://loogle.lean-lang.org/
• https://live.lean-lang.org/
• https://reservoir.lean-lang.org/
• lean4checker
• lean4lean
• Lean 4 extension update "Commands & Walkthrough"
• Lake performance boost
• Lake cloud releases
• lake toolchain intelligence: leanprover/lake#180 related: #7282 #7652
• Documentation tooling, haven't found the link to the demo, but discussions here
• LeanInfer
• llmstep
• repl
• lean-training-data

[Scott Morrison]

Also https://github.com/leanprover-community/repl. I'd be very happy to have bug reports, criticisms, and requests for this one. The tactic mode is a bit half-baked at the moment, but I'm waiting to learn from users what is needed most here.

[Sebastian Ullrich]

The slides are at https://lean-lang.org/talks/community-meeting-oct-2023.pdf

[Leonardo de Moura]

Lean Focused Research Organization (FRO) - Monthly Community Meeting - November edition
Time-zone-aware time: 2023-11-21T07:00:00-08:00
Meeting details and links:
Tuesday, November 21 · 7:00 – 8:00am
Time zone: America/Los_Angeles
Google Meet joining info
Video call link: https://meet.google.com/guj-dcde-cdq
Or dial: ‪(US) +1 617-675-4444‬ PIN: ‪335 436 365 9596‬#
More phone numbers: https://tel.meet/guj-dcde-cdq?pin=3354363659596

[Joachim Breitner]

Has anyone per chance already created a public calendar with these meetings that one can subscribe to?

[Henrik Böving]

I have a webdav share with my org mode calendar if you want in on that :stuck_out_tongue:

[Leonardo de Moura]

Hope to see you all next Tuesday.

[Leonardo de Moura]

Another reminder for the Monthly Community Meeting.
The Lean FRO roadmap is now available here: https://lean-fro.org/about/roadmap/
We will cover it during the meeting tomorrow.

[Sebastian Ullrich]

You can also subscribe to a calendar of all community meetings as iCal

[Julian Berman]

(Go to calendar.google.com, click "+" in Other Calendars > From URL in the left sidebar, paste that URL in, for anyone like me who wants to add that to your GCal)

[Alex J. Best]

I couldn't make it today unfortunately, was this meeting recorded or is there any summary beyond the (very interesting!) roadmap?

[Mario Carneiro]

It was recorded, hopefully it will appear online soon

[Floris van Doorn]

I would also like to watch the recording!

[Sebastian Ullrich]

Uploading now!

[Sebastian Ullrich]

https://youtu.be/4IDrPL4I_bU

[Filippo A. E. Nuccio]

I love @Leonardo de Moura's remark that Zulip can be scaring for many people, I met several colleagues telling me so.

[Scott Morrison]

This is very important to remember, and all the more important to try to account for your own bias on this concern, the more you personally use zulip! :-)

[Scott Morrison]

It took the mathoverflow moderators far too long at first to appreciate just how scary and unfriendly mathoverflow appeared to many would-be users. Sadly by the time we realised, so much of the culture was already set (so that what we thought we had carefully and successfully cultured ended up being different from what we later wished for).

[Filippo A. E. Nuccio]

I understand what you are saying very well, but we should not forget that MO was a great success! Thanks for building it.

[Eric Wieser]

Filippo A. E. Nuccio said:

Zulip can be scaring for many people

I remember finding this myself long ago, and felt for quite a while that posting outside the #new members stream was a scary prospect.

[Damiano Testa]

I would also like to add that I am one of the people who found MO great, but personally had always some reservations towards it. I feel much more comfortable on this Zulip. Of course, this is for entirely personal reasons: I find both projects awesome!

[Rob Lewis]

Today's FRO community meeting will happen today at 2024-01-12T10:00:00-05:00 as part of the ongoing #Lean Together 2024 workshop. We'll be using the LT2024 Zoom meeting instead of the old Google link: https://brown.zoom.us/j/94792332977

[Kim Morrison]

The January community meeting recording is now available: https://youtu.be/iv_0-cbH5ow

[Mario Carneiro]

Is there an FRO meeting starting now?

[Henrik Böving]

Yes

[Henrik Böving]

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

[Mario Carneiro]

I think it would be useful to have either the outline or the slide available before or at the same time as the meeting start, it would help to solicit questions since there are so many independent threads going on it's difficult to remember everything

[Patrick Massot]

I didn’t see it coming at all and completely missed it. It would be really nice to post reminder on the previous day.

[Patrick Massot]

I’ll wait for the recording now.

[Thomas Murrills]

Oops, I’m in the same boat.

Maybe a bot could post to zulip based on the events calendar? Would this be easy to set up?

[Patrick Massot]

Oh that would be nice!

[Filippo A. E. Nuccio]

Patrick, you know that you can subscribe to the CalDav/google calendar, right? Do you stick to an old -fashioned pen-and-paper agenda while replacing pen-and-paper mathematics with Lean :smirk: ?

[Henrik Böving]

Patrick Massot said:

I’ll wait for the recording now.

https://www.youtube.com/watch?v=vb1pPkG9e-8

[Jireh Loreaux]

The next Mathlib community meeting was originally scheduled for 2024-04-19T09:00:00-05:00, but this is being postponed for a week until 2024-04-26T09:00:00-05:00. I hope to see you there. This message will be followed by a poll for topics of interest to discuss during the meeting. Feel free to contribute your own topic ideas.

[Jireh Loreaux]

/poll Topics for Mathlib community meeting 2024-04-26T09:00:00-05:00
Mathlib roadmap
PR review concerns and successes
Avenues of communication
Community blog

[David Renshaw]

Can the calendar event be updated? https://lean-fro.org/events/ (it's still showing as 19 April)

[Jireh Loreaux]

Just a reminder that this is happening in two days. I'll post another reminder an hour before it starts.

[Jireh Loreaux]

Reminder: starts in just over an hour.

[Andrew Yang]

Is there a link to the meeting?

[Joachim Breitner]

https://meet.google.com/guj-dcde-cdq
Waiting for some host to start the meeting.

[Andrew Yang]

Thanks!

[Jireh Loreaux]

There should be a recording available at some point, but I tried to take a few notes very quickly. They may be incomplete or otherwise bad in places, as it was a bit hard to do while leading.

[Jireh Loreaux]

Mathlib roadmap

• Developing curated lists of topics

• Figuring out what people want from Mathlib (e.g., what's missing, what things they need for their projects)
  This requires input from people who don't already contribute Mathlib.

• Getting non-expert Lean users to create Lean blueprints for things they want to see in Lean

• Examples: Nevanlinna theorem

Std/Boost

• tabled discussion until the next meeting

Avenues of communication

• Mutual inductive types are hard to work with in Lean (maybe belongs in the roadmap section above)
• The community website needs lots of updating still

PR reviews concerns and successes

• nothing mentioned

Community blog

• no new updates recently
• people who are starting may use that to gauge activity and interest
• This Month in Mathlib
• Maybe use PRs with emoji reactions as ones that should go on the blog: ask authors to write a short blurb
• Have authors create short blurbs for PRs they feel should go on the blog. This could be on a wiki page or after the --- on their PR.

Other questions or points of discussion

• the Ethereum foundation is looking to host a formalization competition for formalizing ZKVM ($10s of millions of dollars in bounties to encourage the wider community to prove correctness of these circuits).
  Justin Drake is the point of contact and is available on Telegram as justindrake

• Label system for reservoir to tag packages with their focus? Planned for the future.

• Should we move to more loosely coupled hierarchies? Talk to Johan who has started trying this out a bit. Preliminary results suggest it should be an improvement.
• Sometimes we should scope instances for very low-level classes that cause big issues with type class search (Subingleton, etc.)
• Some relevant Lean 4 issues: lean4#2905 and lean4#3996

[Ruben Van de Velde]

One of my favourite English facts is that "to table a discussion" means both to put something on the agenda and to remove something from the agenda

[Michael Stoll]

This may be a British vs American thing...

[Anatole Dedecker]

Sorry I couldn’t be here, what is meant by "more loosely coupled hierarchies" ?

[Joachim Breitner]

Ruben Van de Velde said:

One of my favourite English facts is that "to table a discussion" means both to put something on the agenda and to remove something from the agenda

Relatedly, “to punt (on) something” has a simiar ambiguity, it seems: https://english.stackexchange.com/q/388162/44740

[Jireh Loreaux]

My personal favorite self-antonym (for which I've just learned that the fascinating words contronym, contranym or autantonym exist):

cleave (verb): split or sever (something), especially along a natural line or grain.

cleave (verb): stick fast to. adhere strongly to (a particular pursuit or belief).

[Jireh Loreaux]

Anatole Dedecker said:

Sorry I couldn’t be here, what is meant by "more loosely coupled hierarchies" ?

In the context we used it today, it means separating the data structures from the prop bits, and only having mixin classes for the overlap. So maybe we would have an algebra data chain (Field → Ring → Monoid) and an ordered data chain (LinearOrder → PartialOrder → Preorder), but then LinearOrderedField would just take Field and LinearOrder as parameters, and the rest of the field are props. (at least that was my interepretation of the discussion)

[Patrick Massot]

I was teaching during the meeting but let me comment on the website and blog stuff. I agree it is very sad that things are not moving. This is why I called for help during the opening talk of LT2024. Updating the remaining Lean 3 pages on the website is pretty easy because we can do them one at a time and this is a one-shot job. Some people simply need to decide to prioritize this task. The blog is harder. I think the monthly post was very useful but it was a lot of work, done mostly by two people. We did have a python script listing rss stream posts with emojis. But this was only a very crude filter. And then one needed to come up with some categories and minimal narrative. I would love to see some team talking up this task, but don’t advertise it as something a script scrapping Zulip can do.

[Anatole Dedecker]

Jireh Loreaux said:

Anatole Dedecker said:

Sorry I couldn’t be here, what is meant by "more loosely coupled hierarchies" ?

In the context we used it today, it means separating the data structures from the prop bits, and only having mixin classes for the overlap. So maybe we would have an algebra data chain (Field → Ring → Monoid) and an ordered data chain (LinearOrder → PartialOrder → Preorder), but then LinearOrderedField would just take Field and LinearOrder as parameters, and the rest of the field are props. (at least that was my interepretation of the discussion)

Ah yes, 100% yes, I’ve been wanting that refactor for a long time (I never pushed strongly for it because I have no idea about the performance implications)

[Jireh Loreaux]

@Patrick Massot one thing that was in the meeting but not reflected in my notes above: we all understand the monthly updates were too much work for just the blog editors, and we were brainstorming ways that it could be accomplished with significantly less effort on your part (or whoever is on the team).

[Jireh Loreaux]

One thing that we could try for the month of May: when a maintainer merges a PR they feel like should be listed on the monthly blog update, they ask the author to contribute a line / sentence to a wiki page (with an @ mention so that the author sees it). There can even be instructions like: give a one sentence summary. Then at the end of the month the editors just curate this page into an actual post. This distributes the work of choosing the PRs to the entire maintainer team, and it crowdsources the actual summaries.

[Patrick Massot]

This sounds very much worth trying.

[Robert Maxton]

Doesn't this make generalizing over algebraic structures difficult? Especially since for now, category theory is its own branch of Mathlib and importing e.g. Bundled or BundledHom as your method of abstraction involves pulling in a whole bunch of extra imports

[Robert Maxton]

Right now I'm trying to write a structure that will back a tactic (so it should have minimal dependencies), that needs to take "any" equivalence eqv, and am running into this exact problem -- the best I can do AFAICT is write eqv : α → α → Prop, and e.g. RingEquiv doesn't actually fit that signature, it has signature (R : Type u) → (S : Type v) → [inst : Mul R] → [inst : Mul S] → [inst : Add R] → [inst : Add S] → Type (max u v)

[Robert Maxton]

so anyone using my function is actually going to have to do their own bundling themselves

[Jireh Loreaux]

What does that have to do with the proposal for separating the hierarchies?

[Robert Maxton]

I was addressing the line

In the context we used it today, it means separating the data structures from the prop bits

Replacing (more) bundled types with unbundled mixins means that the type signature will be increasingly variable and thus harder to quantify over.

...Though I suppose my specific example doesn't get any worse if you split the existing hierarchies further?

[Jireh Loreaux]

Two things:

1. I wouldn't count on Mathlib's type class hierarchy settling down in general.
2. I think this proposal, if anything, would contribute to stabilization, not detract from it.

[Anatole Dedecker]

Also, it sounds like your approach would require the much larger change of going fully bundled instead of semi-bundled, e.g (R : Ring) instead of (R : Type) [Ring R]. This is essentially antithetic to what we've been doing so far (except in category theory) so I wouldn't count on Mathlib chnaging anytime soon in that aspect.

[Robert Maxton]

Fair enough!

[Sebastian Ullrich]

Recording is now up at https://youtu.be/YkqbXjdZJuw

[Kim Morrison]

Apologies I wasn't able to make the meeting, I was far from the internet and sound asleep. :-)

A few follow-up comments, after listening to it in the background:

• On the undergraduate curriculum, we still have almost nothing in differential equations / numerical analysis (although the number theorists are beginning to encroach here!).
• Separate projects (with a leader!) are clearly the way to make progress in specific directions, rather than Mathlib-internal roadmaps or github projects.
  • How can we make it easier for such projects to form? (Currently the model is too often "be famous already, and announce you want to do something in Lean").
  • Sometimes this can involve recruiting a blueprint author who is not necessarily already a Lean expert.
  • Blueprints and dependency graphs are essential!
• Review queue: we need new tooling. The github search interface is not enough. We need to be able to see quickly what is assigned to whom, which PRs have stalled (either with an assigned reviewer or without), etc. This is essentially journal submission management (both the software, and managing editors!), but I think in practice we need bespoke tooling.
• Blog posts
  • The FRO blog is more active now. Does it help to occasionally "reblog", to avoid long periods of silence?
  • Can we pay someone? (Particularly for writing this "month in mathlib". It's a lot of work, and I don't believe it can be crowdsourced.) Hoskinson? Someone's grant? Apply for a grant?
  • If we want to try crowd-sourcing, I would suggest just doing it directly in the repo. (PR descriptions or the wiki page are simply too much overhead, given that this isn't being done at all at present.) Just add a this_month_in_mathlib.md file in the repo, and ask people to add a bullet point. Then copy and paste to the blog. If it is embarrassingly unused, we delete the file again later. The downside of this is that it is harder to modify "after the fact", when someone notices that a certain PR was mention-worthy.

[Sebastian Ullrich]

Slides for today:
Monthly-Community-Meeting-10-May-2024.pdf

[Sebastian Ullrich]

Recording: https://youtu.be/sJipZYPKX6Q

[Michael Rothgang]

Kim Morrison said:

• Blog posts
  • [...] Can we pay someone? (Particularly for writing this "month in mathlib". It's a lot of work, and I don't believe it can be crowdsourced.) Hoskinson? Someone's grant? Apply for a grant?

I recently came across a call by the DFG (German research foundation) for research software infrastructures. Calls are open all year round; I wonder if applying for a grant there could work.
Presumably whoever applies needs to be in Germany, though...

[Yaël Dillies]

Is it somewhere in here? https://www.dfg.de/de/foerderung/foerderinitiativen/nfdi

[Michael Rothgang]

It's here: https://www.dfg.de/de/foerderung/foerdermoeglichkeiten/programme/infrastruktur/lis/lis-foerderangebote/forschungssoftwareinfrastrukturen

[Michael Rothgang]

English version: https://www.dfg.de/en/research-funding/funding-opportunities/programmes/infrastructure/lis/funding-opportunities/research-software-infrastructures

[Riccardo Brasca]

Is there a meeting today?

[David Renshaw]

I am "waiting for the host to join"

[Damiano Testa]

What link?

[Riccardo Brasca]

https://meet.google.com/guj-dcde-cdq?authuser=0&hs=122

[Riccardo Brasca]

@Damiano Testa you add this calendar to any app you use

[Riccardo Brasca]

this is how I don't forget the meetings :D

[Sebastian Ullrich]

I let people in but as I think we're on schedule for a Mathlib-led community meeting, I don't have any agenda. I'm not sure anyone else does.

[Sebastian Ullrich]

I ended the call for lack of agenda and participants. @David Renshaw gave a great, quick demo on an embedding of chess into Lean though!

[Eric Wieser]

(cc @Julian Berman, who built https://lean-across-the-board.readthedocs.io/en/latest/ a while ago)

[Julian Berman]

And @Yakov Pechersky who did a ton (most?) of the useful work on that!

[Kim Morrison]

Sorry about this: this monthly community meeting was meant to be run by the Mathlib maintainers, and it seems we dropped the ball and collectively managed to forget about the meeting.

[Sebastian Ullrich]

At the FRO, we've made the decision to discontinue our (up to now bimonthly) community meetings in favor of focusing on the release blog posts and the office hours, neither of which we had when we started the community meetings. We believe that the latter two are better suited for documenting new features and answering questions from the community, respectively. Questions specifically about a new release are in scope and welcome at the office hours as well.

We are happy to keep providing the technical hosting for the maintainers-led meetings if desired.