Moving lean3 project to lean4

Stream: mathlib4

[Bernd Losert]

I was developing my lean3 project (https://github.com/berndlosert/convergence) using gitpod. I made a branch called lean4 for migrating to lean4. However, I'm not sure what to do. I updated the gitpod.yml to use lean4. What is the next step? Do I need to update the toml file? Or is there some magic invocation of lake that I need to run?

[Patrick Massot]

This is a lot more complicated I'm afraid. You need to use https://github.com/leanprover-community/mathport/#readme

[Bernd Losert]

I am willing to rewrite most of my code from scratch if that helps. I just need to get the mathlib4 dependency set up.

[Jireh Loreaux]

Don't do yourself the disservice of rewriting from scratch. Mathport is the way to go. You should be able to use mathport oneshot, and if you #align some names by hand I bet it will be relatively straightforward.

[Patrick Massot]

I don't think oneshot is relevant here since it looks like Bernd has many files to port.

[Patrick Massot]

But we can help with using mathport. Bernd, the very first step is to upgrade your project to the latest version of mathlib3.

[Jireh Loreaux]

You can just concatentate all the files into one and then use oneshot. It's a bit of extra work, but I find less than using full blown mathport when the number of files is small (as I believe is the case here).

[Eric Wieser]

I think it would be better to guide one person through using mathport properly and write more documentation than encourage people to concatenate files

[Patrick Massot]

My personal experience is that the instructions to use mathport properly are very clear.

[Alistair Tucker]

Hi! I see in the instructions for Mathport Oneshot that I can put #align statements in a file Oneshot/lean4-in/Extra.lean. Sorry for being dense, but where should I put them when running Mathport proper?

[Mario Carneiro]

@Alistair Tucker If you add "Extra" to the "extraModules" field in config-project.json, it will use the same file Oneshot/lean4-in/Extra.lean; or you can add a file in another location if you add the path to it to the "leanPath"field

[Mario Carneiro]

I didn't know anyone was actually using this feature!