Zulip Chat Archive

Stream: general

Topic: Error using lean --run

view this post on Zulip 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 :=
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,

Thanks in advance!

view this post on Zulip 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.

view this post on Zulip Ruben Van de Velde (Dec 10 2020 at 19:20):

leanprover/ or leanprover-community/?

view this post on Zulip Rob Lewis (Dec 10 2020 at 19:20):

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

view this post on Zulip 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!

view this post on Zulip 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