Zulip Chat Archive

Stream: general

Topic: lean installation


view this post on Zulip 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 project.md.

Thanks again for the excellent installation procedure and documentation!

view this post on Zulip Johan Commelin (May 20 2019 at 17:20):

@Jeremy Avigad Just for the record: it is update-mathlib...

view this post on Zulip Johan Commelin (May 20 2019 at 17:21):

Concerning the apt vs other pkg managers issue: maybe we should use a different way to test whether VSCode is already installed.

view this post on Zulip 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.

view this post on Zulip 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 texlive.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 23 2019 at 15:38):

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


Last updated: May 15 2021 at 00:39 UTC