Toolchain Install, Directory & Server Connection

Stream: new members

[Gwilym Evans]

Hello! First post here, new to Lean.

I tried to follow along Chris Lovett's tutorial using Gitpod and Lean4 Samples but got stuck with the Rubiks file when running

'lake build rubiksJs'

error: toolchain 'leanprover/lean4:nightly' does not have the binary C:\Users\gwily\.elan\toolchains\leanprover--lean4---nightly\bin\lake.exe

But failed to reinstall it successfully after a few tries. Also having trouble with the server connecting, and from looking on forums seems it's a directory issue, and that these problems are related perhaps? I feel like I'm missing something.

Any help appreciated. Much thanks!

[Mario Carneiro]

The lean 4 samples directory is unmaintained and we are considering deleting it. Best use a different example. The issue here seems to be that the lean-toolchain file is too old, mathlib uses leanprover/lean4:v4.5.0-rc1

[Gwilym Evans]

Ah, easy then. Thank you!