Zulip Chat Archive

Is there a migration guide for Lean 3 to Lean 4? I just started trying to rewrite some of my old projects from Lean 3, but I keep running into little differences here and there which are not covered by https://lean-lang.org/lean4/doc/lean3changes.html, which I'm sure the mathlib porters had to deal with many times before me...

Ruben Van de Velde (Nov 23 2023 at 20:44):

Are you using mathport?

Ruben Van de Velde (Nov 23 2023 at 20:45):

I think the porters mostly learned by doing and asking here

Scott Olson (Nov 23 2023 at 20:45):

Wasn't planning on using mathport - my projects are small enough that I prefer to port by hand and learn as I go.

Ruben Van de Velde (Nov 23 2023 at 20:47):

I see. Have you written new lean 4 code already?

Eric Wieser (Nov 23 2023 at 20:47):

I think you would learn more by comparing the output of mathport with the original, than by mangling your Lean3 code until it compiles; the former will give you idiomatic code, the latter will likely not

Scott Olson (Nov 23 2023 at 20:48):

I've found porting by hand very easy and clean for the most part, not remotely like "mangling". The hard parts are just when there are features that don't seem to have any counterpart in Lean 4. I suppose I'll set up mathport to see what it does with those features.

Eric Wieser (Nov 23 2023 at 20:51):

The things that look clean from the perpective of Lean 3 may not be considered clean from the perspective of Lean 4

Scott Olson (Nov 23 2023 at 20:53):

I don't think it just looks clean from the perspective of Lean 3 — the ported code has so far turned out much nicer and simpler than the source in most cases thanks to Lean 4's many new conveniences.