What's ilean & olean

Stream: lean4

[Locria Cyber]

I was trying to build a lean file without lake.
What I got:

$ lean --deps EmptyProgram.lean
/home/user/.elan/toolchains/leanprover--lean4---nightly/lib/lean/Init.olean

[Locria Cyber]

What is that .olean file?

[Andrés Goens]

Locria Cyber said:

What is that .olean file?

it's the object file, basically a machine-readable version of the file (but it's based on the Lean core language and preserves the types, so it's not the same as the C object file that you get later down the compilation pipeline)

[Sebastian Ullrich]

It's the data loaded by import

[Locria Cyber]

What's ilean then?

[Floris van Doorn]

The .ilean file contains information related to jump-to-definition. For every declaration (or command?) it contains the locations where it is used and where it is defined. You can open it in a text editor to get an idea what is in it.