Zulip Chat Archive

Stream: general

Topic: what happened to update-mathlib?


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?

Johan Commelin (May 22 2019 at 03:34):

It moved to a new repo

Johan Commelin (May 22 2019 at 03:35):

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

Johan Commelin (May 22 2019 at 03:35):

But the install instructions are not in that repo

Johan Commelin (May 22 2019 at 03:35):

They are somewhere in the docs/ of the regular repo

Johan Commelin (May 22 2019 at 03:37):

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

Koundinya Vajjha (May 22 2019 at 03:37):

Thanks! Found the instructions for mac

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: Dec 20 2023 at 11:08 UTC