How to run the main function in lean 4?

Question

I am following the lean 4 tutorial and see a main function as follows:

-- Defines a function that takes a name and produces a greeting.
def getGreeting (name : String) := s!"Hello, {name}! Isn't Lean great?"

-- The `main` function is the entry point of your program.
-- Its type is `IO Unit` because it can perform `IO` operations (side effects).
def main : IO Unit :=
  -- Define a list of names
  let names := ["Sebastian", "Leo", "Daniel"]

  -- Map each name to a greeting
  let greetings := names.map getGreeting

  -- Print the list of greetings
  for greeting in greetings do
    IO.println greeting

I am not sure how to run the main function. It's not in the FAQ. I tried to call it from the command line (Ubuntu 20.04):

lean 1_whats.lean

It gives no result. The VS code IDE (with lean4 support installed following the prompt) does not seem to show anything in All Messages. I tried to add a separate line with just main, which causes an error on the preceding for line

invalid 'do' notation, expected type is not available

Obviously, this is really a beginner question.

How to run the main function in lean 4?

Answer 1

You may extract C source and compile it:

$ cat hello.lean 
def main := IO.println "Hello, World!"
$ lean -c hello.c hello.lean 
$ leanc hello.c -o hello
$ ./hello 
Hello, World!

Or pass --run option just as in Lean 3:

$ lean --run hello.lean 
Hello, World!

There is also Lake described in tutorial:

$ mkdir hello
$ cd hello
$ lake init hello
$ lake build
...
$ ./build/bin/hello
Hello, world!

Compiling or --run-ing by hand multiple interconnected files is a way harder. Suppose we have something like this:

$ cat test.lean 
def test := "HELLO"
$ cat hello.lean 
import test

def main := IO.println test

lean --run hello.lean will fail at this time:

$ lean --run hello.lean 
hello.lean:1:0: error: unknown package 'test'
hello.lean:3:12: error: unknown identifier 'IO.println'
hello.lean:3:12: error: unknown constant 'sorryAx'

For first, you need to properly set up your LEAN_PATH. There should be at least path-to-your-lean4-directory/lib/lean and your working directory:

$ echo $LEAN_PATH
/path-to-my-lean4-directory/lib/lean/:/path-to-my-working-directory

After import test Lean will look up for test.olean file in LEAN_PATH (and for directories named test). So you need to create these .olean files:

$ lean -o test.olean test.lean

And now you can run hello.lean:

$ lean --run hello.lean 
HELLO

At this moment we can also extract C code for both files:

$ lean -c test.c test.lean 
$ lean -c hello.c hello.lean

And compile them exactly as you compile C. So you may pass test.c and hello.c directly to leanc (which is wrapper around clang):

$ leanc test.c hello.c -o hello

Or firstly generate object files and then link them together:

$ leanc test.c -c -o test.o
$ leanc hello.c -c -o hello.o
$ leanc test.o hello.o -o hello

Or link them into a static/dynamic library if you want:

$ ar rcs libtest.a test.o hello.o
$ leanc libtest.a -o hello
$ ./hello 
HELLO

Answer 2

Just to first be clear, in Lean a main function is an entry point to use Lean as a programming language with input and output, and a main function is a common feature in many compiled programming languages. If you are interested in using Lean as a theorem prover, or using Lean interactively (by say executing code with #eval), then you don't need a main function, and I would point you to Theorem Proving in Lean 4.

Method 1: Building a Lean 4 (code) project using Lake

Now, how to compile a Lean 4 project to run main? Note that Lean 4 is compiled, and the tool to both make your project and compile it is lake. There are instructions here but they might be a bit confusing.

To make a new lean code project, do lake new <project_name> to make a new project directory, or if you already have a project directory, do lake init <project_name> inside that directory.

For example, lake new my_test_project makes a directory my_test_project which can be opened in vs code and adds the following files:

.gitignore
MyTestProject.lean
lakefile.lean
lean-toolchain
Main.lean

Note, lake new and lake init always add this code which comes pre-populated with a simple hello world program. In particular, Main.lean contains the main function.

To build your project, run lake build. This will add the following files:

build/
  bin/
    my_test_project
    my_test_project.trace
  ir/
    ...
  lib/
    ...

If you run the bin file, build/bin/my_test_project you will get the output:

Hello, world!

A few more notes:

• See here for advice on how to structure the files in your project. But it seems out of date with the current way Lake sets up the directory (namely with a Main.lean file).
• I don't do much development in Lean 4, but I think if you were going down this route, you could set up build tasks in VS Code to make the build and run steps go faster.

Method 2: Run a one-off lean file with lean --run

If you have a file such as the one you posted in your question which has both a main function and doesn't import other things, then it is possible to run it with lean --run <filename>.lean. If my memory serves me correctly, this can make the code run slower since it is not compiled (but that only matters if you are doing heavy computation).

Edit: See siegment's answer for how to compile a one-off lean file directly.

Note: At least right now I can't do lean --run Main.lean on the Main.lean example from Lake, since Main.lean imports other stuff. That gives me strange errors. (I don't know if that is intended or a bug.)

Edit: See siegment's answer for how to make lean --run work with more complicated projects (such as those coming from Lake).