search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

Problems with exec-path and lean-rootdir #15

Open oliveira-caio opened 5 years ago

oliveira-caio commented 5 years ago

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.

Kha commented 5 years ago

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.

oliveira-caio commented 5 years ago

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. ):

adeet1 commented 5 years ago

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?

adeet1 commented 5 years ago

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?

wijnand2 commented 5 years ago

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"

mdnahas commented 2 years ago

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".

mikeshulman commented 2 years ago

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.