'Running' lean 4 programmes

Stream: lean4

[Gihan Marasingha]

I'm just starting out with Lean 4 using Windows Subsystem for Linux / VSCode. I initialised a project as per the instructions, choosing the nightly lean4 build.

I built the 'hello world' program (below) using leanpkg foo.

def main : IO Unit :=
  IO.println "Hello, world!"

I navigated to the build directory and tried to run the binary with lean --run foo.olean. I get several error messages:

Foo.olean:1:0: error: expected command
Foo.olean:2:134: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:2:133: error: unexpected command
Foo.olean:9:369: error: expected token
Foo.olean:9:413: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:9:412: error: elaboration function for 'numLit' has not been implemented
Foo.olean:9:501: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:9:500: error: unexpected command
Foo.olean:9:525: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:9:524: error: unexpected command
Foo.olean:20:67: error: expected token
Foo.olean:20:451: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:20:450: error: unexpected command
Foo.olean:20:1595: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:20:1594: error: unexpected command
Foo.olean:20:1697: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:20:1696: error: unexpected command
Foo.olean:24:24: error: expected token
Foo.olean:27:14: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:27:13: error: unexpected command
Foo.olean:27:841: error: tabs are not allowed; please configure your editor to expand them
Foo.olean:27:840: error: unexpected command

What am I doing wrong? Also, is there a way to create a native binary?

[Daniel Fabian]

Lean 4 is a whitespace sensitive language, meaning you must not use tabs, but must use spaces instead. Apparently your code file does use tabs at the moment.

As the error says, it's usually an editor setting to use spaces instead.

[Sebastian Ullrich]

--run expects a .lean file, not .olean

[Sebastian Ullrich]

You can create a native binary using leanpkg build bin