Topic: lean installation
Jeremy Avigad (May 20 2019 at 17:12):
@Patrick Massot I was fortunate to have my operating system crash last week so that I could try your one-line installation of Lean. It worked beautifully. Many thanks. In fact, it worked so well that I decided to follow your further instructions to set up a Lean project with a local copy of mathlib, rather than using on a global copy, as I have done all along. The instructions again worked exactly as advertised.
I have two small notes. The first is that, because I had already installed VSCode through the Ubuntu package manager (which in 18.04 is
snap rather than
apt), I ended up with two copies of VSCode. (I used
apt remove to remove one.) Second, if I understand correctly, the appropriate way to update mathlib in my project is now to use
leanpkg upgrade and then
mathlib-update. It might be helpful to say that in
Thanks again for the excellent installation procedure and documentation!
Johan Commelin (May 20 2019 at 17:20):
@Jeremy Avigad Just for the record: it is
Johan Commelin (May 20 2019 at 17:21):
apt vs other pkg managers issue: maybe we should use a different way to test whether VSCode is already installed.
Patrick Massot (May 20 2019 at 20:35):
Thanks Jeremy! Indeed https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/install_debian.sh currently doesn't test at all whether VScode is installed. It assumes that everybody uses
apt or doesn't want automatic installation of anything. It seems Ubuntu created a mess with
snap. But I'll add a simple test anyway.
Jeremy Avigad (May 21 2019 at 17:24):
Thanks. I won't defend Ubuntu. More often than not, I use
apt from a terminal instead of
snap. For example,
snap doesn't seem to know about
Keeley Hoek (May 21 2019 at 23:12):
In my experience lots of the snaps are just plain broken too, e.g. the vscode one
Patrick Massot (May 23 2019 at 15:38):
Last updated: May 15 2021 at 00:39 UTC