Confusion about Lean REPL

Stream: new members

[Haoyang Shi]

I'm new to Lean REPL. I use v4.15.0 to have a try.
When I input { "cmd" : "import Mathlib\ntheorem add_even (x y : ℤ) (hx : Even x) (hy : Even y) : Even (x + y) := by sorry" } , I got this:

{"messages":
 [{"severity": "error",
   "pos": {"line": 2, "column": 64},
   "endPos": {"line": 2, "column": 66},
   "data": "unexpected token '+'; expected ')', ',' or ':'"}],
 "env": 0}

Could anyone tell me what's wrong? Is there a syntex error? :pleading_face:

[Eric Wieser]

I don't think you can put the import there

[Haoyang Shi]

So what shall I do? :speechless:

[Haoyang Shi]

Help :confounded:

[Anthony Wang]

That error message is very misleading. I think the Lean REPL is actually complaining because the Mathlib import failed probably. You need to run the REPL in the root directory of a Lean project that has Mathlib as a dependency: https://github.com/leanprover-community/repl?tab=readme-ov-file#using-the-repl-from-another-project Otherwise, I also get that same error.

[Haoyang Shi]

Thanks a million! :folded_hands:
Now I found that it could run, but in a very very low speed. A simple statement may take nearly 3 minutes. Is that normal or just because of my poor computer configuration (M1 8GB)? I can hardly run my experiment in that speed. How can I solve it? :face_in_clouds:

[Anthony Wang]

For me, running lake build Mathlib first reduced the wait time from several minutes to only a few seconds.

But I would recommend using Lean in VSCode instead of the REPL unless you have a very specific reason why you need the REPL.

[Niels Voss]

I presume you are using the REPL because you want to programmatically interact with Lean? In this case, you could probably reuse the environment (recall that each REPL call gives you an environment id), so that you only have to import Mathlib once

[Haoyang Shi]

Anthony Wang 发言道：

For me, running lake build Mathlib first reduced the wait time from several minutes to only a few seconds.

But I would recommend using Lean in VSCode instead of the REPL unless you have a very specific reason why you need the REPL.

Thank you so much. Well I have to use REPL as I want to interact with Lean programmatically. I think the major reason why it's so slow is the poor RAM configuration. :melting_face:

[Haoyang Shi]

Niels Voss 发言道：

I presume you are using the REPL because you want to programmatically interact with Lean? In this case, you could probably reuse the environment (recall that each REPL call gives you an environment id), so that you only have to import Mathlib once

Yeah you are so right! It's really helpful! :face_holding_back_tears: