This repository was archived by the owner on Apr 2, 2025. It is now read-only.
This repository was archived by the owner on Apr 2, 2025. It is now read-only.
Trouble setting up: lean.executablePath incorrect #335
Description
I'm having some trouble setting up: I got the error "Unable to start the Lean server process: Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure it is a valid Lean executable"
When I open a terminal, I can see that "lean" works and points to "/scratch/gua/.elan/bin/lean". However, I have to run "source ~/.bashrc4" for this to work (for various reasons, it's not called .bashrc), the bashrc file adds the directory to my $PATH.
I also tried using "/scratch/gua/.elan/bin/lean" as the lean.executablePath, but then it gives me error: no default toolchain configured. run `elan default stable` to install & configure the latest Lean 3 community release.
Any ideas how to fix the issue?