What is an oleans file?

Stream: new members

[Lars Ericson]

What is an oleans file? I see it mentioned from time to time.

[Mario Carneiro]

.olean is the file extension of the lean "object" files

[Mario Carneiro]

these are generated when you compile a lean file, and contains everything lean needs to compile dependent lean files

[Lars Ericson]

Except as it may happen under the hood of code, I haven't manually compiled a file. Is it like Python where the compilation happens silently in a . directory? Is there a time when I would do it explicitly? Is there a doc?

[Mario Carneiro]

it doesn't really happen under the hood in the server mode, this can be a performance issue if you have a big project

[Mario Carneiro]

with mathlib, you should be using leanproject up which downloads precompiled oleans

[Logan Murphy]

@Lars Ericson I had a project that I wanted to be called from a Command Line Interface, and there were a lot of files being imported by the main file, and they had their own imports, and so on. Using lean --run main.lean took like 30 seconds, but if I used lean --make main.lean, it would generate the olean files in my directory, and after that lean --run was instant.