Important:
I deleted this post because it was out of date and causing confusion. The Lean Community now has its own website and up to date installation instructions for getting Lean and the key tool leanproject are here.
How to install mathlib and keep it up to date
This entry was posted in Technical assistance. Bookmark the permalink.
Xena 
Thanks for this very cool project. For me (on linux), `leanpkg build` did nothing. It tried to run `lean –make src`.
I changed this to `lean –make –recursive _target`, and now it is happily compiling (and heating our living room as a side effect).
LikeLike
Oh there was at least one change since I wrote that post. Lean is not a finished product yet, it’s just a project which sometimes changes its mind about how things should look. Yes, `leanpkg build` now does nothing unless you have a directory `src` containing files which import mathlib files! I usually change directory into _target/deps/mathlib now and run `leanpkg build` in there but your answer is probably better.
LikeLike
Pingback: Tonbridge | Xena
Hi. Thank you for this installation page. After I typed in PATH=$PATH:/d/git/Git/bin (I installed it in a new file called git) in msys2, nothing was returned. Does this mean git is not working? What “output” does a successful command give? Thank you.
LikeLike
I’m really sorry, I cannot help with Windows problems, I don’t have access to a Windows machine. I wrote that stuff when I was in our department computer room surrounded by them, but I won’t be there for a while as it’s the holidays. Ask at https://leanprover.zulipchat.com/, there are Windows users there. But changing your path variable in unix would not make any output appear, that’s for sure. It would just mean that unix would look in different places for the next command you type.
LikeLike
“leanpkg build” doesn’t work for me (it completes quickly and doesn’t create any olean files), but “lean –make _target/deps/mathlib” as described here does.
LikeLike