Error using lean --run

Stream: general

[Tung Tran]

Hello everyone! I'm trying to run lean (built from source from the official leanprover/lean git repo) on my .lean file, but an error occurred:
$ ../bin/lean --run src/test_lean.lean
<unknown>:1:1: error: unknown declaration 'main'

I traced it back to line 646 in lean.cpp:
eval_helper fn(main_env, opts, "main");

But I've got no clue what to do next. Also, the file test_lean.lean has the following content (which is a part of tutorial):
import data.real.basic

example {a b c : ℝ} (hab : a ≤ b) : c + a ≤ c + b :=
begin
rw ← sub_nonneg,
have key : (c + b) - (c + a) = b - a, -- Here we introduce an intermediate statement named key
{ ring, }, -- and prove it between curly braces
rw key, -- we can now use the key statement
rw sub_nonneg,
exact hab,
end

Thanks in advance!

[Rob Lewis]

What are you trying to do with the --run flag? lean --run file.lean looks for def main : io unit (or possibly tactic unit too?) in file.lean and executes it.

[Ruben Van de Velde]

leanprover/ or leanprover-community/?

[Rob Lewis]

If your aim is just to check your example, use lean file.lean without the flag.

[Tung Tran]

Thanks everyone for the fast response!
I was using leanprover/ (I've tried both leanprove/ and the community version, though). I was just checking as well, but having no output makes me think something was wrong. And thank you Rob, that was great help!

[Patrick Massot]

Tung, since you seem to be the kind of person who wants to build everything from source and do everything the hard way, you should read https://leanprover-community.github.io/toolchain.html. That's about the only community-written documentation telling the truth instead of making things look easy.