Zulip Chat Archive

Stream: general

Topic: lean setup


Arthur Paulino (Nov 04 2021 at 13:08):

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 (Nov 04 2021 at 13:09):

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

Johan Commelin (Nov 04 2021 at 13:11):

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 (Nov 04 2021 at 13:12):

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

Johan Commelin (Nov 04 2021 at 13:12):

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

Johan Commelin (Nov 04 2021 at 13:12):

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

Eric Wieser (Nov 04 2021 at 13:14):

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 (Nov 04 2021 at 13:14):

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

Arthur Paulino (Nov 04 2021 at 13:43):

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 (Nov 04 2021 at 13:50):

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

Jannis Limperg (Nov 04 2021 at 13:59):

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 (Nov 04 2021 at 14:36):

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

Patrick Massot (Nov 04 2021 at 14:36):

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

Scott Morrison (Nov 05 2021 at 03:52):

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 (Nov 05 2021 at 06:02):

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

Kevin Buzzard (Nov 05 2021 at 09:01):

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 (Nov 05 2021 at 11:46):

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 (Nov 05 2021 at 11:48):

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

Eric Wieser (Nov 05 2021 at 11:48):

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

Eric Wieser (Nov 05 2021 at 11:51):

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

Eric Wieser (Nov 05 2021 at 11:58):

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 (Nov 06 2021 at 00:10):

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 (Nov 06 2021 at 08:26):

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

Chris Lovett (Nov 06 2021 at 18:30):

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 (Nov 06 2021 at 22:22):

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 (Nov 06 2021 at 22:23):

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

Sebastian Ullrich (Nov 06 2021 at 22:28):

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

Sebastian Ullrich (Nov 06 2021 at 22:29):

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

Chris Lovett (Nov 07 2021 at 00:39):

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 (Nov 07 2021 at 00:43):

@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).


Last updated: Dec 20 2023 at 11:08 UTC