elan override persists when changing directory?

Stream: lean4

[Siddharth Bhat]

I noticed this behaviour today:

~/work/new/ssa/ssa$ which lean
/home/bollu/.elan/bin/lean


~/work/new/ssa/ssa$ cd ~/work/new/lean-llvm/lean4


~/work/new/lean-llvm/lean4$ which lean # elan override
/home/bollu/work/new/lean-llvm/lean4/build/stage1/bin/lean


~/work/new/lean-llvm/lean4$ cd ~/work/new/ssa/ssa # go back to original directory


~/work/new/ssa/ssa$ which lean # override still persists, even when I change directories!
/home/bollu/work/new/lean-llvm/lean4/build/stage1/bin/lean


~/work/new/ssa/ssa$ # build breaks because wrong compiler :(

Am I doing something wrong in how I'm using elan / overrides?

[Alex J. Best]

what does elan override list say?

[Siddharth Bhat]

~/work/new/ssa/ssa elan override list
/home/bollu/work/new/lean-llvm/lean4/src    /home/bollu/work/new/lean-llvm/lean4/build/stage0

[Sebastian Ullrich]

elan cannot affect which, so this has nothing to do with elan

[Siddharth Bhat]

I did indeed pull an epic fail due to my configuration of dotenv. Thanks for the debugging help Alex, Sebastian!

~/work/new/lean-llvm/lean4 cat .env
export PATH=/home/bollu/work/new/lean-llvm/lean4/build/stage1/bin:/home/bollu/work/new/lean-llvm/llvm-install/bin/:$PATH
export LD_LIBRARY_PATH=/home/bollu/work/new/lean-llvm/lean4/build/stage1/bin:/home/bollu/work/new/lean-llvm/llvm-install/lib/:$LD_LIBRARY_PATH

I had this config when I was trying to tame CMake for LLVM, and I entirely forgot about its existence after...