diff between .lean and .olean

Stream: general

[Abhishek Cherath]

Are .olean files like object files that speed things up somehow? how's that work exactly? are they just like the object files gcc generates before linking?

[Johan Commelin]

they certainly speed things up

[Johan Commelin]

compiling mathlib takes between 30 minutes and 2 hours on most machines

[Johan Commelin]

but with the leanproject tool, you can just download olean files in 5 seconds, and you're up and running.

[Mario Carneiro]

They are kind of like gcc object files, although there is no linking going on. An olean file stores the result of elaboration of a complete lean file, meaning that in order to compile one lean file you only need the olean files of all dependents

[Abhishek Cherath]

Mario Carneiro said:

They are kind of like gcc object files, although there is no linking going on. An olean file stores the result of elaboration of a complete lean file, meaning that in order to compile one lean file you only need the olean files of all dependents

I see so when I say import x from mathlib, it doesn't just macro expand the .lean files, it uses the pre ASTed or whatever .olean file

[Mario Carneiro]

Well not really either one. It declares a dependency on the other lean file; the environment objects for all dependents are merged to form the initial environment for the current file. It's a more semantically meaningful thing than C style text replacement

[Mario Carneiro]

In server mode it will generally use the olean files if they exist and the hashes match and you aren't currently editing that other file

[Abhishek Cherath]

Mario Carneiro said:

Well not really either one. It declares a dependency on the other lean file; the environment objects for all dependents are merged to form the initial environment for the current file. It's a more semantically meaningful thing than C style text replacement

yes that's what I meant, so the way lean knows what's already known is from the final env state from prev files, and because of olean it doesn't have to do all the work

[Mario Carneiro]

right