Help installing Lean

Stream: new members

[Luiz Felipe Martins]

I'm trying to install Lean in MacOs. Is there a "standard way" to do that?

I have tried the setup guides in different places, including here:

https://leanprover-community.github.io/install/macos.html

I'm still not successful running Lean code. A couple questions:

1) Each time a project is created, there is a lengthy download. Is that the way it is supposed to be?

2) Is there a way to run Lean code from the command line? Something like a "Hello, World"? I find it difficult to see what is wrong from Visual Code, so a command line example would be greatly appreciated.

[Julian Berman]

That's the right page -- what happens when you run that script?

[Benjamin Jones]

In (1) are you talking about the toolchain download, or downloading dependencies that are project specific, e.g. Mathlib?

For (2), yes. There's a (shameless) example here: https://github.com/benjaminfjones/reckonlean/blob/main/lakefile.lean There are exe targets defined there you can compile and run on the command line (see the README). Those targets depend on library code also in the package.