what happened to update-mathlib?

Stream: general

[Koundinya Vajjha]

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?

[Johan Commelin]

It moved to a new repo

[Johan Commelin]

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

[Johan Commelin]

But the install instructions are not in that repo

[Johan Commelin]

They are somewhere in the docs/ of the regular repo

[Johan Commelin]

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

[Koundinya Vajjha]

Thanks! Found the instructions for mac

[Johan Commelin]

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