Daniel Selsam (Jan 29 2021 at 04:01):
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 (Jan 29 2021 at 09:22):
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
Gabriel Ebner (Jan 29 2021 at 09:57):
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
Last updated: May 18 2021 at 23:14 UTC