This post is now very old and out of date so I deleted it; for instructions on installing Lean see the Lean community website here.
Installing Lean (and VSCode) on Windows from scratch
This entry was posted in Technical assistance. Bookmark the permalink.
Xena 
Pingback: Proving trivial things with Lean | Xena
I got an error when installing it on macOS, something along the lines of that it couldn’t run “lean –version”. This is what I did to fix it!
1. Install homebrew from https://brew.sh.
2. Install the program gmp using homebrew, by typing “brew install gmp” into your terminal.
I figured this out by searching online, and following the directions from this post on StackOverflow: https://stackoverflow.com/questions/26555902/ruby-v-dyld-library-not-loaded-usr-local-lib-libgmp-10-dylib
It worked for me and some other people using macs during the first meeting (Thurs 5th Oct)!
LikeLiked by 1 person
If you are trying to install Lean on macOS using the steps outlined above (in addition to Philip Thiede’s comment) and you’re still stuck on step 4 (“Tell the VSCode Lean extension where Lean is”) then be aware of the type of quotation marks in this webpage.
If you’re copying the executable path from the webpage, then the use of the ‘curly’ “” quotation marks will not work. Instead, replace this with ‘straight’ “” quotation marks, and this should work now.
LikeLike
I made an html error. I think they’re fixed now. Thanks Elliott.
LikeLike
Peiran Wu sent me a very helpful email, saying that they had managed to get VS Code working with Lean installed in C:\Program Files (i.e. a path name with a space in). Their trick was that instead of setting “lean.executablePath” in the VS Code User Settings, one can add the directory of the Lean binary to the system path by modifying the Windows system environment variable. I’m sure google will be able to tell you how to change system environment variables in any recent version of Windows, so this sounds like a great solution.
Thanks Peiran!
LikeLike