Quick compiling of a single file

Stream: lean4

[Trebor Huang]

Is there a way to quickly compile a single file without setting up a project? I would like it to be compiled instead of interpreted, and it has no dependencies, for some random testing around.

[Henrik Böving]

lean --run foo.lean should do the trick

[Trebor Huang]

Ahh, so that compiles? I haven't tried that. I'm AFK right now.

[Henrik Böving]

Oh sorry I misread that, compiling would be a bit harder. I guess you can in theory look at the output of lake build --verbose if you want to figure out the specific commands for that.

[Christian Pehle]

You can use the lean and leanc executables directly. If the file you want to compile is "foo.lean", then a command would be

lean foo.lean -c foo.c
leanc foo.c -o foo

If you want this to be an executable then foo.lean needs a main function.