mathlib4 priorities

Stream: mathlib4

[Kevin Lacker]

Hello, I was wondering how the port of mathlib to lean 4 is going, and where would be the most useful place to help out. Is there something like a "list of pending TODO items"? Or a breakdown like, we need to port 200 tactics, and these 60 are already complete. Or is the bottleneck not really porting tactics, but something else?

[Johan Commelin]

cc @Gabriel Ebner @Mario Carneiro @Arthur Paulino @Scott Morrison @Edward Ayers

[Kevin Lacker]

i did read this blog post https://leanprover-community.github.io/blog/posts/intro-to-mathport/ but that is 4 months ago so hopefully some of those "todos" described have been done already

[Gabriel Ebner]

A good starting point for the tactic todo is this file: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean

[Kevin Lacker]

do the comments like /- N -/ have some secret meaning

[Gabriel Ebner]

Yes, it's described at the top of the file.

[Kevin Lacker]

oh, i see. okay so all of the tactics in this file are essentially "todo" items

[Henrik Böving]

Ocasionally core Lean implements one on the list themselves and they are not removed from the list right away but generally speaking that is correct

[Kevin Lacker]

so just to get a first-order understanding of the project, counting the occurrences of syntax (name in this file, three months ago it was at 299 and now it's at 256. this is a pace for, in about a year and a half all the tactics will be ported. does that seem vaguely accurate?

[Henrik Böving]

The rough time line was to hopefully be done by the end of this year and then get to cleaning up the compiler itself and do more funky stuff.

[Kevin Lacker]

do you expect the compiler work + "funky stuff" to be more work or less work than porting all the tactics

[Jireh Loreaux]

What is the current status of that Lean 4 meta programming guide @Arthur Paulino ? I might be interested in contributing some easy tactics to help speed the process along. I have some Haskell experience, so monads aren't entirely foreign to me.

[Henrik Böving]

Kevin Lacker said:

do you expect the compiler work + "funky stuff" to be more work or less work than porting all the tactics

That's a question for @Leonardo de Moura or @Sebastian Ullrich

Jireh Loreaux said:

What is the current status of that Lean 4 meta programming guide Arthur Paulino ? I might be interested in contributing some easy tactics to help speed the process along. I have some Haskell experience, so monads aren't entirely foreign to me.

very, very little content unfortunately, all people that write tactics rn are self taught from reading code and asking the smarter people.

[Arthur Paulino]

Jireh Loreaux said:

What is the current status of that Lean 4 meta programming guide Arthur Paulino ? I might be interested in contributing some easy tactics to help speed the process along. I have some Haskell experience, so monads aren't entirely foreign to me.

We've got the first and second chapter to a "ready-for-review" state but we need feedback from readers. @Siddhartha Gadgil wrote some content for the MetaMchapter that also needs feedback from readers. At the moment I'm doing more studies about Lean 4 so I can continue creating more content for it

[Arthur Paulino]

Link: https://github.com/arthurpaulino/lean4-metaprogramming-book
If anyone wants to help, the files that need to be changed are the ones inside the lean directory. The markdown files from md are generated automatically by lean2md

[Henrik Böving]

I've been digging into how TermElab and CommandElab work since the beginning of the week, I think I might write something on attributes (they are surprisingly fundamental to all of Lean's extensibility) and the rough workings of term elaboration and command elaboration the next days and try to dig further down along the stack so maybe we'll meet in the middle :P

[Leonardo de Moura]

Henrik Böving said:

Kevin Lacker said:

do you expect the compiler work + "funky stuff" to be more work or less work than porting all the tactics

That's a question for Leonardo de Moura or Sebastian Ullrich

I don't know how to answer this question. In the Lean 4 repo, we are currently focusing on fixing bugs and adding missing features that are relevant for the Mathlib port. The "compiler work" (i.e., code generation) is not essential for the port, thus we have postponed. I am reading "funky stuff" as many aspirational features we want, but are also not essential for the port.

[Mario Carneiro]

Henrik Böving said:

Ocasionally core Lean implements one on the list themselves and they are not removed from the list right away but generally speaking that is correct

They are removed as soon as a complete replacement is added. The only reason it would not be removed is if there are still some unimplemented features in the lean 3 tactic, or we did not notice when bumping nightly. (They are all in the Lean.Tactic namespace to maximize the probability of a name clash if one is implemented upstream so we can take it off the list.)

[Edward Ayers]

to_additive is merged

[michal wallace (tangentstorm)]

Arthur Paulino said:

Jireh Loreaux said:

What is the current status of that Lean 4 meta programming guide Arthur Paulino ?

We've got the first and second chapter to a "ready-for-review" state but we need feedback from readers....

I've just starting reading it. What sort of feedback are you looking for?

[Henrik Böving]

Whatever isn't clearly understandable or you think needs more detailed explanations/further information in general.

[Henrik Böving]

The quality goal right now is to get it to a point where we can show it to people and expect them to understand the basics of Lean 4 meta programming afterwards, assuming that they already know how monads and basic Lean 4 syntax works.