lean installation

Stream: general

[Jeremy Avigad]

@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!

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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.

[Keeley Hoek]

In my experience lots of the snaps are just plain broken too, e.g. the vscode one

[Patrick Massot]

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