migrating mathlib to Lean 4

Stream: general

[Scott Morrison]

(This post is me trying to find out how wrong I am about what migration may look like, not any attempt to say how it will or should be!)

Gabriel made an experiment a while ago in which he managed to import an olean file generated by Lean 3 directly into Lean 4 (right?). For my purpose now, it doesn't really matter if there's some intermediate processing step.

I'm hoping that this is the case, and we may be able to follow a plan like this:

• rename all current .lean files to .lean3 files, and change community Lean to expect this
• teach leanproject (or suitable replacement) to do "dual compilation", of a collection of .lean3 and .lean files (using Lean 3 and :four_leaf_clover: respectively), where the .lean files can import .lean3 files but not vice versa
• in CI, change the all.lean3 we use to check that everything compiles compatibly back to all.lean, so it is processed by Lean 4
• declare victory :tada:
• ...
• now start on the real work!
• during this phase new contributions to mathlib would be accepted that add new .lean3 files (with the proviso you are now only allowed to import things that haven't been migrated), or that add new .lean files, or that migrate .lean3 files to .lean files.
• we build some tooling in Lean4, e.g. to automatically rename declarations, to make switching to CamelCase sane
• we start reproducing some of the major tactics from Lean3 in Lean4, e.g. the simplifier
• we gradually start switching files across, using some hybrid of reproducing Lean3 tactic well enough that proofs can be reused and rewriting proofs --- whatever is easiest
• hopefully watch the graph of "ratio of lean3 : lean4" files gradually tend to zero (like we watch the size of nolints.txt)

Is this hopelessly optimistic? Are we instead going to have to just make a new repository and work "from the bottom up"? Or is this not what we should be aspiring to in the first place?

[Ruben Van de Velde]

I think that gradual conversion as you propose is the only really feasible approach

[Scott Morrison]

The problem is we need feasible and viable. :-)

[Rob Lewis]

I find it hard to even speculate without a better sense of what we'll have to work with. It's probably a fair assumption that early releases, at least, will have bugs, performance issues, missing features, etc that won't become apparent until porting starts, and will presumably need breaking changes to be fixed. Not saying this as a complaint, just that we should expect a lot of instability early on. It might be better to iterate on some very small core of mathlib for a while at the beginning so we don't waste a ton of effort on things that we know will change.