Starting a new Lean 4 project

Stream: new members

[Martin C. Martin]

Are these instructions up to date? In particular, is it still recommended to use a nightly lake from February?

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

In general, if I want to start a new Lean 4 project with mathlib, what instructions/steps should I use?

[Martin C. Martin]

Should we call lake or leanproject?

[Martin C. Martin]

I'm on an M1 Macbook using Homebrew, if that matters.

[Alex J. Best]

You should use lake, leanproject isn't really used anymore. And the above command will setup the project to use the latest nightly, it just downloads the febuary one first in order to create the folder etc. You could change it to something more recent or something you have installed and it should work fine. I normally look and see which version the master of mathlib is using and use that

[Martin C. Martin]

Are these steps still relevant, for an M1 Macbook, starting from scratch?

1. xcode-select --install and softwareupdate --install-rosetta
2. arch -x86_64 zsh
3. Install brew: /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
4. eval "$(/usr/local/bin/brew shellenv)"

5. a. brew install elan
   b. brew install mathlibtools
   c. elan toolchain install stable
   d. elan default stable
   Then we do the Lean 4 lake thing.

[Kevin Buzzard]

This does not look right: mathlibtools are for Lean 3 I believe.

[Philipp]

I just did exactly that:

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

And now lean can't find the lean or lake binaries:

lake build
error: toolchain 'leanprover/lean4:nightly-2023-08-05' does not have the binary `C:\Users\Philipp\.elan\toolchains\leanprover--lean4---nightly-2023-08-05\bin\lake.exe`

error: toolchain 'leanprover/lean4:nightly-2023-08-05' does not have the binary `C:\Users\Philipp\.elan\toolchains\leanprover--lean4---nightly-2023-08-05\bin\lean.exe`

[Alistair Tucker]

@Martin C. Martin There is no need to do the Rosetta/x86_64 dance if you plan only to use Lean 4. It is necessary however if you want ever to run Lean 3 and are unwilling to compile it locally.