3
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ Is that indentation intended? $\endgroup$
    – Trebor
    May 12 at 5:30
  • $\begingroup$ @Trebor I assume not since the original example is not indented. Copy and paste gone wrong? $\endgroup$
    – Jason Rute
    May 12 at 11:34
  • $\begingroup$ Thanks for pointing out the indentation issue. Just edited. $\endgroup$
    – tinlyx
    May 12 at 17:47

2 Answers 2

3
$\begingroup$

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
$\endgroup$
3
  • $\begingroup$ Just so I'm clear, can the first method work if you have multiple interconnected lean files, or do you just have to move to Lake then? Also is there something like lean --run for Lake projects, where you can run your code without compiling first? $\endgroup$
    – Jason Rute
    May 12 at 11:14
  • 1
    $\begingroup$ @JasonRute yes, it can, and lean --run can work with Lake projects. I edited my answer to explain this. $\endgroup$
    – siegment
    May 12 at 11:39
  • $\begingroup$ There is also something called scripts in Lake, but I never used this feature. $\endgroup$
    – siegment
    May 12 at 12:01
2
$\begingroup$

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).

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.