## Stream: general

### Topic: Error using lean --run

#### Tung Tran (Dec 10 2020 at 19:16):

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

#### Rob Lewis (Dec 10 2020 at 19:20):

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 (Dec 10 2020 at 19:20):

leanprover/ or leanprover-community/?

#### Rob Lewis (Dec 10 2020 at 19:20):

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

#### Tung Tran (Dec 10 2020 at 19:26):

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 (Dec 10 2020 at 19:38):

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.

Last updated: May 09 2021 at 18:17 UTC