lean setup

Stream: general

[Arthur Paulino]

What do you think would be the ideal Lean setup considering that we're interested in getting the attention of people who don't necessarily know much about binaries and paths? Personally I was a bit confused on the Lean setup because when I visited the Downloads tab from the official Lean site it linked me to binaries and source files. So I thought "Huh, this is hard on some people", then I downloaded the binaries, decompressed them in a directory and added the directory to my PATH by hand.

But then, after interacting here on Zulip, I realized that elan is the binary file that's supposed to call the proper Lean binary according the Lean version of the project I'm in. So the setup that I had done by hand was unnecessary.

Since then I've been asking myself how to make the Lean setup smoother. But of course I'd prefer hear it from you guys, who have actual experience dealing with Lean projects. How do you think we could make the Lean setup more welcoming?

[Johan Commelin]

@Arthur Paulino I guess you've seen https://leanprover-community.github.io/get_started.html ?

[Johan Commelin]

We have to cater to people who have never heard of a command line before, but also to power users. Currently, using lean and mathlib effectively requires learning some technical tools: command line, git. That might change in the future, but I don't think it will happen soon.

[Johan Commelin]

This means there will be some hurdles that are not-directly-Lean-related.

[Johan Commelin]

At the same time, there are users who live in the shell and git merge for breakfast.

[Johan Commelin]

That's why we try to provide different installation methods, and different guides.

[Eric Wieser]

If your goal is to get the attention of people with a small lean project of your own for them to play around with, you can hand them a link to a gitpod instance so they can explore your code with a full lean installation in browser

[Eric Wieser]

That doesn't help bridge the gap to "yes I want to use this for my own project" very well though

[Arthur Paulino]

Johan Commelin said:

Arthur Paulino I guess you've seen https://leanprover-community.github.io/get_started.html ?

Yeap I saw that link. Mentally I'm using Coq's setup as a benchmark, for which a $ sudo apt install coq coqide does it all. But the Coq's mathematical libraries are always downloaded by default.

[Arthur Paulino]

And (damn) Coq has its own IDE, which requires a lot of work to develop

[Jannis Limperg]

If you use this Coq setup, you get something that's fine for playing around and for small projects, but not for bigger stuff (because then you want opam to manage dependencies and VSCode/Emacs/Vim for editor features). So it's more comparable in purpose to the Lean web editor.

[Patrick Massot]

You won't get any library when downloading Coq like this.

[Patrick Massot]

Anyway, we know Lean could be easier to install. I think there are people at MSR working on this.

[Scott Morrison]

Chris Lovett has recently been working on the VSCode extension, so that it automatically offers to install elan if it isn't available.

[Johan Commelin]

Didn't the Lean 3 extension already have something like that? Or was it removed again at some point?

[Kevin Buzzard]

Is the idea that the lean 4 extension replaces leanproject and offers eg a collection of projects which users can download from GitHub, and when the user clicks on them it installs the project and mathlib oleans and then opens the root project folder? That would be so helpful, says the person who yesterday supervised an install fest when trying to get a bunch of undergraduates to install his course project...

[Arthur Paulino]

Idea: this strategy of hosting cached olean files and not needing to build everything from scratch everytime could be another parameter of the toml file, so mathlib wouldn't need to be the only project with this feature

[Eric Wieser]

Yes, there's discussion of that elsewhere regarding lean-liquid

[Eric Wieser]

The difficulty is that leanpkg removes any keys from the toml file it doesn't recognize

[Eric Wieser]

Meaning it removes any config that leanproject wants to keep for itself

[Eric Wieser]

The fix would be to keep around a manifest.extra : list (string × toml.value) field of all the extra data we don't know how to parse yet, and write it back out when we modify the toml

[Scott Morrison]

Johan Commelin said:

Didn't the Lean 3 extension already have something like that? Or was it removed again at some point?

This was removed again as it was too fragile.

[Sebastian Ullrich]

@Chris Lovett has spent some serious effort on the Lean 4 implementation, in particular on Windows, please give it a try

[Chris Lovett]

Yes if you want to try Lean 4 smooth setup using VS Code, please try the "Lean4" VS Code extension and tell me if it works or not (no command line stuff required). The marketplace text is a bit out of date, this is the up to date readme. and ignore step 5. about the PATH we just changed the extension to look in the default elan install location automatically.

[Kevin Buzzard]

Oh wooah. Is this likely to work on a Windows machine where the user does not have admin access but where VS Code is already installed? That's the situation my laptop-free undergraduate users find themselves in.

[Kevin Buzzard]

Admittedly, such users (UGs without laptops) are becoming thinner on the ground recently. However many only have 8 gigs of ram...

[Sebastian Ullrich]

Definitely, you don't need admin rights to install elan, nor does it have any special dependencies

[Sebastian Ullrich]

It will not download more RAM for you, however. Yet.

[Chris Lovett]

The default location for the elan and lean toolchain install on windows is in your %USERPROFILE% (c:\users\username\.elan). You can check how many toolchain versions you already have by looking at .elan\toolchains folder, if you see a lot there you can reclaim some space by deleting them using elan toolchain uninstall <toolchainname>. If you prefer not to install on your "C:" drive you will need to install elan manually.

[Chris Lovett]

@Kevin Buzzard you mentioned laptop-free undergrads, if your school has access to github enterprise, they could potentially use github codespaces, see demo then there really is nothing installed on the local machine they are using (except vscode).