emacs returns error when opening a lean file

Stream: general

[Daniel Choi]

I installed Lean on a Mac and went through the instructions given on the community page. When I opened a newly-created .lean file, emacs complained that

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

Unfortunately, I have no idea what to set lean-rootdir to. Any pointers? It appears that Lean will not work as intended unless I resolve this.

[Scott Morrison]

Have you used leanproject to create a new project? If you don't have a directory containing a leanpkg.toml file, then go back and follow the part of the instructions explaining how to do that. If you do have such a directory, that is the directory you want to open.

[Scott Morrison]

(I don't use emacs, so I'm not sure exactly how to translate "open the directory", which is what you'd say for VSCode.)

[Daniel Choi]

Ah, I hadn't gotten to the leanproject part of the instructions yet, thanks
But then a new problem pops up: apparently leanproject isn't defined yet? The same page suggests source ~/.profile and source ~/bash.profile, I tried both it doesn't work

[Daniel Choi]

Should have put in the effort to convert to a Linux distro, would have been much simpler :|

[Daniel Choi]

Also Mac is now using zsh instead of bash, that should affect the file name but I can't find the equivalent profile file.

[Daniel Choi]

Might have found the problem—looking at the logs, Homebrew hit an error after installing elan and so mathlibtools was never installed. Will update to confirm.

[Daniel Choi]

OK I'm up and running now; thanks for the help!

[Scott Morrison]

Great, thanks!