How to install mathlib and keep it up to date


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.

About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Technical assistance. Bookmark the permalink.

6 Responses to How to install mathlib and keep it up to date

  1. jmc says:

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


    • xenaproject says:

      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.


  2. Pingback: Tonbridge | Xena

  3. h-k-chris says:

    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.


    • xenaproject says:

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


  4. “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.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s