## Stream: new members

### Topic: What is an oleans file?

#### Lars Ericson (Jan 05 2021 at 15:00):

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

#### Mario Carneiro (Jan 05 2021 at 15:10):

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

#### Mario Carneiro (Jan 05 2021 at 15:10):

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

#### Lars Ericson (Jan 05 2021 at 15:25):

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 (Jan 05 2021 at 15:25):

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 (Jan 05 2021 at 15:26):

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

#### Logan Murphy (Jan 05 2021 at 19:26):

@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.

Last updated: May 10 2021 at 00:31 UTC