Zulip Chat Archive

Stream: general

Topic: what happened to update-mathlib?


view this post on Zulip Koundinya Vajjha (May 22 2019 at 03:31):

i am walking a new user through lean+mathlib. i can't seem to find the update-mathlib one-liner which I used to install it before. has it been changed?

view this post on Zulip Johan Commelin (May 22 2019 at 03:34):

It moved to a new repo

view this post on Zulip Johan Commelin (May 22 2019 at 03:35):

https://github.com/leanprover-community/mathlib-tools

view this post on Zulip Johan Commelin (May 22 2019 at 03:35):

But the install instructions are not in that repo

view this post on Zulip Johan Commelin (May 22 2019 at 03:35):

They are somewhere in the docs/ of the regular repo

view this post on Zulip Johan Commelin (May 22 2019 at 03:37):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/linux.md — Installation instructions for Windows.

view this post on Zulip Koundinya Vajjha (May 22 2019 at 03:37):

Thanks! Found the instructions for mac

view this post on Zulip Johan Commelin (May 22 2019 at 03:37):

For Debian there is a dedicated page offering a 1-line installer that installs VScode, elan, update-mathlib, and all other goodies you can think of


Last updated: May 14 2021 at 13:24 UTC