Zulip Chat Archive

Stream: mathlib4

Topic: porting progress

Arthur Paulino (Mar 17 2022 at 13:09):

Is there a place where we can see how further in mathlib mathport goes successfully?
I think some kind of progress report would help motivating the community. Example:

Progress report
  total files:   28%
  algebra:       35%
  combinatorics: 10%
  ...

Sebastian Ullrich (Mar 17 2022 at 13:31):

https://twitter.com/andy_kelley/status/1503618085789466624 comes to mind for a similar (and apparently popular) example

Gabriel Ebner (Mar 17 2022 at 14:01):

Is there a place where we can see how further in mathlib mathport goes successfully?

The elephant in the room is of course what progress means at this stage of the port. I can only think of two axes which you can measure in percent at the moment: and that's the tactics and metaprograms (i.e., @[to_additive] and co.).

It might be useful to create issues on the mathlib4 repo for that (like Ed has done for to_additive). Then you automatically get a progress bar if you put the issues in projects. Check this out as an example: https://github.com/leanprover-community/mathlib/projects

Arthur Paulino (Mar 17 2022 at 14:13):

To me, progress is something along the lines of "how many of the files mathport successfully translates?".

It is indeed possible to create issues and make projects on GitHub that will give us an idea of progress. But I find it kind of blurry. E.g. I can't have an idea of the impact caused by the implementation of a certain set of things (some tactics and/or tags etc).

In other words, my notion of completeness of the port is "we will be done when all files from mathlib are translated to Lean 4". So my most straightforward question is: "how many of them can we successfully translate now?"

Gabriel Ebner (Mar 17 2022 at 14:14):

At a later point in the porting process, we should try to compile the synported files on their own (i.e., without the binport). Then we might get progress information like this:

files w/ syntax errors: 1%
files w/ errors in proofs: 99%
files w/ errors in defs and thm stmts: 90%
files w/o errors: 1%

I'm not sure it makes sense to try this yet (because almost all files still have errors in definitions), but if you're motivated it would be awesome to have infrastructure for testing (and measuring) ready for this experiment. After to_additive is ported the number of errors should go down significantly. On the mathport side, mathport#131 and mathport#106 are two other big issues that break lots of instances (and with that, lots of dependent definitions).

This experiment will also require some modifications to core Lean. One to address mathport#53. Then we'll also need options to ignore errors (i.e., save the olean even if there are errors so that we can continue compiling).

Gabriel Ebner (Mar 17 2022 at 14:16):

After flag day, we'll most certainly need to fix up the ported files. Only then do we really get a progress bar of the form "how many files compile successfully".

Arthur Paulino (Mar 17 2022 at 14:51):

Thanks a lot for the explanation! I'll try to stick to the Mathport low-hanging fruits (as you say it) because they're on the verge of my understanding and are good challenges for me at the moment. Maybe when those are done I will be knowledgeable enough to study Mathport code base and play with the porting experiments

Johan Commelin (Mar 17 2022 at 15:04):

@Arthur Paulino Thank you so much for all that you are doing! It's lovely to see everyone contributing in all these different places with all these different skills.

Siddhartha Gadgil (Mar 21 2022 at 08:33):

Is there some place where there is a description of the tactics (I see some described in MathLib for lean 3), or can some wiki be created to make this easy? For example, I know the decide tactic, but what is decide!? Also is symm just apply Eq.symmor something more (similarly for trans).

Mario Carneiro (Mar 21 2022 at 09:11):

I assume you know about https://leanprover-community.github.io/mathlib_docs/tactics.html ?

Mario Carneiro (Mar 21 2022 at 09:15):

The tactics in Syntax.lean are just the lean 3 tactics, although I made use of some editorial license to change the syntax to be more lean-4-ish in a few places. decide! is the lean 4 version of the dec_trivial! tactic

Mario Carneiro (Mar 21 2022 at 09:17):

As the documentation says, the symm(etry) tactic is not just apply Eq.symm, it will apply any lemma marked with the @[symm] attribute, which is placed on theorems of the form r a b -> r b a for a variety of relations r

Siddhartha Gadgil (Mar 21 2022 at 09:39):

Thanks. Yes, that link was what I meant by "MathLib for lean 3".
Are all tactics then Lean 3 tactics, but with modified names and sometimes syntax? In that case, could someone in the know add comments giving the older name (where it is not obvious).

Edward Ayers (Apr 16 2022 at 02:40):

I've made some progress with to_additive. There are still lots of bugs and todos but the majority of the mathlib code is now ported. There is a test file which is still failing but some of them are working https://github.com/leanprover-community/mathlib4/blob/42dba0238c60197c456f16a5052a5e24e56235b0/test/toAdditive.lean

Edward Ayers (Apr 16 2022 at 02:42):

It would be good to get some eyes on it because the PR is really big now

Marcus Zibrowius (Jun 28 2022 at 12:05):

Is there a place where I can read up on the plans for porting and the progress that has been made? I'm new not only to Lean but also to Zulip, and I struggle nagivating here. I can see that there are lots of discussions of these questions, but I fail to see what consensus has emerged. The github page for mathlib4 only says that the "real" port hasn't even started.

Mauricio Collares (Jun 28 2022 at 12:15):

I think https://leanprover-community.github.io/blog/posts/intro-to-mathport/ is still reasonably up to date

Kevin Buzzard (Jun 28 2022 at 12:20):

mathlib is now 910K lines of code ;-)

Mauricio Collares (Jun 28 2022 at 12:23):

Technically that's over 700K :)

Arthur Paulino (Jun 28 2022 at 12:26):

Since the porting strategies are somewhat involved, here's the long story short: there's an automated method to port mathlib code except for the metaprogramming part, which was completely revamped in Lean 4. That is, linters, tactics, tags etc have to be done by hand.

There are also things that have to be done in Lean 4 core to facilitate such automation, but in the meantime we're working on spreading the metaprogramming word because that's the bottleneck for the community side of the effort

Arthur Paulino (Jun 28 2022 at 12:28):

And then programming in Lean 4 is a requisite for understanding metaprogramming. So there are books being written on both ends

Arthur Paulino (Jun 28 2022 at 12:33):

This is the WIP book for functional programming in Lean 4: https://leanprover.github.io/functional_programming_in_lean/

This is the WIP book for metaprogramming in Lean 4: https://github.com/arthurpaulino/lean4-metaprogramming-book

Mauricio Collares (Jun 28 2022 at 12:37):

Besides the excellent documentation being written, one other piece of news that's not in the blog post comes from https://leanprover.github.io/talks/lean-update-2022-06-15.pdf (page 6): There will be increased focus on the mathlib port after LftCM 2022.

Last updated: Dec 20 2023 at 11:08 UTC