Compile single file

Stream: lean4

[James Sully]

So Functional Programming in Lean mentions lean --run, then takes you through setting up and building a lake project. But is there a way to just compile a single file into a binary?

[James Sully]

lean hello.lean seems to do nothing, and I don't see any relevant flags under lean --help

[Tomas Skrivan]

This works

lean hello_world.lean -c hello_world.c && leanc hello_world.c -o hello_world && ./hello_world

for hello_world.lean file:

def main : IO Unit := do
  IO.println "Hello World"

leanc is just a wrapper around clang with the correct flags

[James Sully]

Thanks! I guess this is not the intended workflow lol

[Tomas Skrivan]

Yeah probably not but I used to do that before lake existed :)

[James Sully]

I'm sorry you had to go through that!

[Mario Carneiro]

lake exe hello_world is the normal way to do this with lake