lean4 development: use local files instead of stage1

Stream: general

[Frederick Pu]

I'm importing a local file I created called "src/Lean/Elab/Womp.lean"
And im getting the following error:

object file '/mnt/c/Users/pufre/Downloads/formal_proofs/lean4/build/release/stage0/../stage1/lib/lean/Lean/Elab/Womp.olean' of module Lean.Elab.Womp does not exist

How do I make lean/elan use the local folder for Lean/Elab?

[Kim Morrison]

Have you followed the instructions at https://lean-lang.org/lean4/doc/dev/index.html?

[Frederick Pu]

Kim Morrison said:

Have you followed the instructions at https://lean-lang.org/lean4/doc/dev/index.html?

I followed every step except for

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none

since I already have elan installed.