port34

Stream: lean4

[Daniel Selsam]

I finished a first proof-of-concept of a mathlib porting tool: https://github.com/dselsam/port34 The tool produces lean4 .olean files for every lean3 .lean file in mathlib. A lot of information is preserved, including (kernel) terms, attributes (e.g. reducible, class, instance, simp), mixfix notation, export declarations, and more. Some definitions and theorems can be restated easily but most are still very cumbersome to elaborate due to a myriad of differences between the two systems that have yet to be accounted for.

[Gabriel Ebner]

This is amazing! Two things I noticed in case anybody else runs into them as well:

• Even though the lean4 path is hardcoded in the makefile, you still need to add lean4 to PATH or make an elan override.
• You need to manually create the lean3/library/all.lean and mathlib/src/all.lean files.

[Gabriel Ebner]

After half an hour and 32 gigabytes of RAM, make portMathlib fails with:

[addDecl] END   analysis/normed_space/dual inner_product_space.norm_to_dual_symm_apply
[genOLeanFor] END   analysis/normed_space/dual
uncaught exception: (kernel) unknown constant 'Mathlib.category_theory.sheaf.subcanonical'
Command exited with non-zero status 1