leanprover
Problems with exec-path and lean-rootdir
Hi, when I create a .lean file, Emacs shows me the following message: "lean scroll hook: (error Lean was not found in the ’exec-path’ and ’lean-rootdir’ is not defined. Please set it via M-x customize-variable RET lean-rootdir RET.)" Does anyone know how can I fix that? I've tried to change the directory through M-x customize variable RET lean-rootdir RET, but then Emacs shows me the following message and nothing happens: "custom-variable-mark-to-save: Symbol’s value as variable is void:" Thanks in advance.
Do you have Lean (or elan) in your PATH? It's usually a good idea to do that anyway; after that, Emacs should copy PATH into its exec-path and lean-mode should be able to find the Lean executable.
How do I do that? I've installed elan, run source /.elan/env and added "(add-to-list 'exec-path "~/path/to/directories")" to my .emacs file and nothing worked. ):
I'm experiencing the same issue. I installed Lean through MELPA on an Ubuntu Linux system by following the instructions in the README file on https://github.com/leanprover/lean-mode, but it's not working. Does anyone know how to fix this problem?
Do you have Lean (or elan) in your PATH? It's usually a good idea to do that anyway; after that, Emacs should copy PATH into its exec-path and lean-mode should be able to find the Lean executable.
How do you add Lean to PATH?
Same issue here, the message "Symbol’s value as variable is void" was caused by not wrapping the path in paranthesis; i.e. I was entering
[path to folder with lean]/lean-3.4.2-linux
instead of
"[path to folder with lean]/lean-3.4.2-linux"
FWIW, I'm running on Ubuntu and ran into a similar problem. I had installed lean in a terminal and updated my PATH. But Emacs was started from another terminal, so it didn't have "lean" in its PATH.
I fixed it by logging out and logged back in. Then the top-level terminal (the one beneath Gnome) had the right PATH. Then, I could start Emacs and it would find "lean".
Perhaps the instructions at https://leanprover-community.github.io/install/linux.html and https://leanprover-community.github.io/install/debian_details.html could be updated to inform the user that after installing Lean they need to either start Emacs from the terminal where they installed it from, or log out and log back in again so the Gnome/etc. shell will have its PATH updated.
