Zulip Chat Archive

I think I have some time now to take the plunge and start working with/on lean4/mathlib4.
It looks reasonable to tackle the forward port of my PR #17483 as a first project.
Can somebody provide (or point me to) step-by-step instructions for how to proceed, starting from square zero (i.e., no lean4 on my (linux) machine yet)?

Eric Wieser (Mar 12 2023 at 21:06):

Here's a rough outline of how I'd recommend you proceed

Wait for the mathlib3 PR to be merged. I've pinged @Yaël Dillies privately to check they're happy with it. I think this should be easy enough to forward port to justify merging it, but want to double check everything before creating forward-porting work
Wait for mathport to regenerate against your new output. That happens every 24 hours I think.
Use the mathport output to update src/Algebra/Group/Basic.lean. This is a somewhat manual process unfortunately.
Fix all the downstream proofs again using the mathlib3 PR as a guide. You can avoid actually installing Lean 4 on your local machine by using https://gitpod.io/#https://github.com/leanprover-community/mathlib4. Make sure to update the header SHAs in all the files you fix.

Eric Wieser (Mar 12 2023 at 21:07):

Note that you might find it more informative to port a random file on #port-dashboard to get a feel for Lean4 before forward-porting something

Yaël Dillies (Mar 12 2023 at 21:09):

/me will review tomorrow morning

Michael Stoll (Mar 12 2023 at 21:20):

I have no problem with installing Lean 4 on my machine; I just haven't done it yet.
For mathlib3, I would then do leanproject get -b mathlib:<some name> to make a branch on which to work. How do I do this for mathlib4?