Importing mathlib into Lean 4

Stream: general

[Gabriel Ebner]

I've just come back from the workshop in Bonn where @Sebastian Ullrich patiently answered lots of questions about the Lean 4 API, and I managed to write a small importer from mathlib to Lean 4. This just creates a Lean 4 olean file with all the mathlib declarations (taken from the textual export format), so don't get your hopes up for converting the mathlib source code. There's no notation and no tactics. My main motivation for this importer is to try writing automation in Lean 4. https://github.com/gebner/lean4-mathlib-import

import Import.Mathlib
#check (deriv : (real → real) → (real → real))

It takes about 6 minutes and 13.5 gigabytes of RAM to import the 213 megabyte export file. The resulting Mathlib.olean file is 3.2 gigabytes large (and it doesn't even contain proofs). However importing this 3.2 gigabyte file is surprisingly snappy: it only takes 1.8 seconds on my machine.

[Sebastian Ullrich]

Any ideas on where the massive blowup is from? Does it compress well?

[Mario Carneiro]

the large size of the olean file is surprising to me, since tree duplication doesn't explain that

[Mario Carneiro]

unless it was reduplicated and not merged again

[Mario Carneiro]

If terms are getting split out into different identical subtrees with different term IDs, it might not compress well because all the addresses are different

[Gabriel Ebner]

Any ideas on where the massive blowup is from? Does it compress well?

zstd compresses it to 362M, the Lean 3 olean files are 70M uncompressed (including proofs). The blowup is probably in part because I'm not deduplicating the terms (and I guess the writeModule function doesn't either). Every definition duplicates the term, since I replace the names.

[Sebastian Ullrich]

@Gabriel Ebner It does now! https://github.com/leanprover/lean4/commit/469562d524adf9fefbbfa6904d8a7f24dff7b009 https://github.com/leanprover/lean4/commit/3c5b3cd91f1e059e73dfbc82e042a6eec1bc8fdc

[Gabriel Ebner]

Oh wow, this moves quickly. I've already added support for Expr.replace, I'll run the import again.

[Gabriel Ebner]

Now Mathlib.olean is just 89 megabytes, and the importer only requires 2 gigabytes of RAM!

[Regivan Hugo Nunes Santiago]

Dear Friends, I need to import a theory, but lean returns the following:

file 'Kenny_comm_alg/ideal_operations' not found in the LEAN_PATH

Can you help me?