getting started with joining the porting effort

Stream: mathlib4

[Edward Ayers]

Hi I've just joined Jeremy as a postdoc in CMU, but I've been out of the Lean loop for the last year or so. As an exercise I would like to port something from mathlib3 to mathlib4. What is a good place to start? I understand there is a porting tool already present but I'm not sure where it is or how to use it. Please could someone point me in the right direction to get started?

[Patrick Massot]

Welcome back! :tada:

[Gabriel Ebner]

Welcome! Easy one first:

I understand there is a porting tool already present but I'm not sure where it is or how to use it.

It is here: https://github.com/leanprover-community/mathport If the README isn't explicit enough, please complain!

[Patrick Massot]

You can start with https://leanprover-community.github.io/blog/posts/intro-to-mathport/

[Gabriel Ebner]

Reading the blog post again, the last section on how to run mathport is pretty outdated. Please refer to the README instead.

[Gabriel Ebner]

As an exercise I would like to port something from mathlib3 to mathlib4.

On a high level, I think these are the important tasks for now:

1. Port metaprogramming commands that generate definitions. restate_axiom, mk_iff, to_additive, simps, etc.
2. Fix synport issues so that more synported code compiles. (We've made a lot of progress here recently. See the issue list on the mathport repo.)
3. Align the algebraic hierarchy so that mathlib4 ring/norm_num/etc. work on the binported/synported code.
4. Port tactics. (This file resembles a todo list: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/Syntax.lean)

[Gabriel Ebner]

@Floris van Doorn IIRC you were at some point last year starting to look into to_additive/simps. Did you get anywhere? Are you still working on it?

[Patrick Massot]

Floris is on vacation this week so he probably won't answer immediately.

[Floris van Doorn]

Gabriel Ebner said:

Floris van Doorn IIRC you were at some point last year starting to look into to_additive/simps. Did you get anywhere? Are you still working on it?

I think I made good progress for to_additive, but didn't finish it yet. I will get back to it this or next week.
I haven't started on simps yet, so someone could work on that if they want.