How to let lake use your own custom build?

Stream: general

[Luc Duponcheel]

Nomally the lean-toolchain file contains a line like leanprover/lean4:v4.21.0, afaik, referring to the dirctory leanprover--lean4---v4.21.0 in ~/.elan/toolchains. I made a custom build following the instructions, and in build/releases/stage1 I obtain (among others) a bin, lib ... directory. How can I now use my own custom build? I tried copying the stage1 content to a leanprover--lean4---v4.xy.z directory in ~/.elan/toolchains and updated lean-toolchain accordingly, but that did not work.

FYI : I changed this true flag to false on line 670 of CoreM.leanand made my custom build for the v4.22.0 release. (cfr my "what happened upgrading from lean4:v4.21.0 to lean4:v4.22.0" topic).

Maybe not a good idea in the first place?

[Vasilii Nesterov]

I think you need to use elan toolchain link as described here: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md

[Luc Duponcheel]

Vasilii, I'm going to have a look at it tomorrow, thanks so much.