lean-toolchain point to local build

Stream: lean4

[David Renshaw]

Suppose I want to use a locally-built lean4 binary to compile a project. Can I update my lean-toolchain file to some value that will tell lake to use the local binary instead of downloading a nightly?

[Sebastian Ullrich]

Yes! See elan toolchain link.

[Chris Lovett]

normally I use elan toolchain link custom ~/git/lean4/build/release/stage1/