How does one compile Lean program that imports Mathlib?

Stream: new members

[Ilmārs Cīrulis]

I have such file in a test project (default Basic.lean):

--- import Mathlib

partial def printing_function (start : Nat) : IO Unit :=
  do IO.println start
     printing_function (start + 1)

def main : IO Unit := printing_function 0

First I build using lake build, then I compile using leanc .lake/build/ir/Testing/Basic.c -O3 -o Basic.exe and the resulting executable works great.

The problem appears in the moment when I uncomment the line import Mathlib. I don't understand how to get executable in such case. :(

[Ilmārs Cīrulis]

When I try to run the file (with import Mathlib uncommented), the result is such error message:

PS C:\Users\ilmar\Documents\Testing> lean --run Testing/Basic.lean
Testing/Basic.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
c:\Users\ilmar\.elan\toolchains\leanprover--lean4---v4.27.0-rc1\lib\lean
PS C:\Users\ilmar\Documents\Testing>

[Ilmārs Cīrulis]

About compiling the .c files -- I have given up.
I have to learn about compiling C projects or smth like that, probably, and then try again.

[Henrik Böving]

The c files already get compiled by lake for you there is no need to do it yourself

[Ilmārs Cīrulis]

O, okay, thanks!