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!