Dev Setup Error

Stream: lean4

[David J. Webb]

I am trying to set up a dev environment so I can contribute to the Lean core, but I consistently run into the same error: when I run elan toolchain link lean4-stage0 build/release/stage0, I get error: not a directory: 'build/release/stage0/bin'. Using the lean.code-workspace as suggested in the dev build guide doesn't help, alas.

(I'm assuming this is the root cause of the other error I get, Lean version 'leanpriver/lean4:lean4-stage 0' is not installed, and upon attempting to install it, no such release: 'lean4-stage0')

[Kim Morrison]

Have you run a build first? You only need to link the toolchain for working in VSCode.

(Sorry, I am not a expert on the build setup, it is voodoo to me every time.)