## Stream: general

### Topic: vscode extension installs Lean

#### Scott Morrison (Sep 17 2018 at 12:20):

I just sent a PR for the VS Code extension, that will offer to install Lean for you if it can't find a working copy. It uses elan, and just runs in the VS Code terminal.

#### Scott Morrison (Sep 17 2018 at 12:20):

I've tested it on OS X, and it seems to work quite nicely.

#### Scott Morrison (Sep 17 2018 at 12:23):

It automatically restarts the extension afterwards, so in good cases the whole Lean installation process could now be:

#### Scott Morrison (Sep 17 2018 at 12:23):

1) Install the VS Code extension

#### Scott Morrison (Sep 17 2018 at 12:23):

2) Open a Lean file

#### Scott Morrison (Sep 17 2018 at 12:24):

3) Click "Install Lean using elan" in the error box that complains you don't have Lean.

#### Scott Morrison (Sep 17 2018 at 12:24):

However I haven't tested this on Linux or Windows.

#### Scott Morrison (Sep 17 2018 at 12:24):

and I haven't thought hard about further diagnostics if something goes wrong (e.g. dependencies are unavailable).

#### Scott Morrison (Sep 17 2018 at 12:25):

If anyone feels up to trying out the PR version of the extension on Linux or Windows, please do!

#### Scott Morrison (Sep 17 2018 at 12:26):

Let me know if you need help --- running a vscode extension from source is delightfully easy.

#### Scott Morrison (Sep 17 2018 at 12:30):

Somewhat depressingly, the reason I did this was because this morning I realised just how badly my email inbox needed love and attention, and so I deleted Lean until I'd made some progress :-).

#### Scott Morrison (Sep 17 2018 at 12:30):

Sitting down after dinner tonight, my first thought was "huh, a nice opportunity to try making installation easier".

#### Scott Morrison (Sep 17 2018 at 12:32):

(For anyone keeping track, a tenure letter got written, and files for scholarship applications for a number of international PhD students got written, but my inbox is still unhappy...)

#### Scott Morrison (Sep 17 2018 at 12:39):

and for my own future reference, to make this work on Windows we'll have to ask VS Code to run elan in some sort of bash terminal, per instructions at <https://stackoverflow.com/questions/42606837/how-to-use-bash-on-windows-from-visual-studio-code-integrated-terminal>. It seems plausible that this could work for a bash terminal provided by any of git bash, linux subsystem for windows, or msys2, but I have no experience with these and I'm unsure whether VS Code would actually be able to find the installation elan created.

#### Sebastian Ullrich (Sep 17 2018 at 16:02):

This looks nice! Though I suspect it only worked for you because you already had ~/.elan/bin in your PATH - the PATH value of the VS Code process will not change when installing elan. What you could do is to just default to ~/.elan/bin/lean as the executablePath if that file exists

#### Sebastian Ullrich (Sep 17 2018 at 16:14):

I'm not sure I like the installation being completely hidden from the user

#### Johan Commelin (Sep 17 2018 at 17:23):

I'm not sure I like the installation being completely hidden from the user

I'm quite sure that there a lot of users that do like it.

#### Scott Morrison (Sep 17 2018 at 20:01):

Good point about the PATH! :-) I'll investigate that later.

#### Scott Morrison (Sep 17 2018 at 20:03):

The compromise I was going for was minimising the number of interactions required during installation, while still showing on the screen what was going on --- so it gives focus to the terminal window doing the work, but doesn't require any interaction inside that terminal window.

#### Scott Morrison (Sep 17 2018 at 20:04):

A pretty reasonable alternative would be to require the user answers the one question that elan asks by default. (Perhaps maximising the terminal window first, so it's obvious to them they need to look at that window?) I could also add a "press any key to continue" prompt at the end, so they can see the end of the output from elan before the terminal window disappears and the extension starts.

#### Sebastian Ullrich (Sep 17 2018 at 20:34):

Yeah, I was imagining something like that prompt. They may also want to at least decide between stable and nightly Lean - not that it matters much right now, or that the installer makes that particularly simple

#### Scott Morrison (Sep 18 2018 at 05:41):

I don't really understand why there is a choice to be made between stable and nightly Lean. Isn't elan deciding for itself on a per-project basis which version of Lean to give you anyway?

#### Johan Commelin (Sep 18 2018 at 06:39):

Scott, in your current workflow, where is the user supposed to make the decision about the project? We don't want them to manually touch a .toml etc...

#### Johan Commelin (Sep 18 2018 at 06:40):

I mean, if it is a Lean file in an existing project, sure... then those choices have already been made by someone else. But if it is a new Lean file in an empty directory...

#### Scott Morrison (Sep 18 2018 at 07:03):

When you type leanpkg init, how is the Lean version decided? Whatever is the logic there should be the default everywhere.

#### Sebastian Ullrich (Sep 18 2018 at 21:13):

@Scott Morrison It's the default Lean version according to elan toolchain list. Which is exactly what you can customize in the installer :)

#### Sebastian Ullrich (Sep 18 2018 at 21:16):

Of course, if we're already integrating elan into editors, we may as well have a dialog for creating a new Lean package with a Lean version chooser. Not sure what to do about stand-alone files, though we may want to de-emphasize their use anyway (e.g. it may not be posible in Lean 4 to import a stand-alone file from another one)

#### Scott Morrison (Sep 19 2018 at 01:11):

I think we should mostly decide that all new users who don't know better want the tools to provide them with stable as effortlessly as possible.

#### Scott Morrison (Sep 19 2018 at 01:11):

When they start looking at other peoples' projects, as long as they got started with elan, those projects will magically use nightly-XXX as desired.

#### Scott Morrison (Sep 19 2018 at 01:12):

And once they realise they need nightly-XXX for their own projects, they can edit a leanpkg.toml file themselves.

#### Scott Morrison (Sep 19 2018 at 07:17):

Hi @Sebastian Ullrich, how would you feel about having elan try to install missing dependencies. Something as simple as:

#### Scott Morrison (Sep 19 2018 at 07:18):

if ubuntu then
sudo apt-get install git libgmp-dev cmake
else if osx then
brew install cmake
brew install gmp


#### Scott Morrison (Sep 19 2018 at 07:19):

would get most non-windows users going a bit faster

#### Scott Morrison (Sep 19 2018 at 07:19):

heck, in the osx branch add

xcode-select --install

#### Scott Morrison (Sep 19 2018 at 07:30):

and running brew --version is harmless, surely?

#### Sean Leather (Sep 19 2018 at 07:30):

Maybe. But I'd still recommend giving the commands to the user and explaining it rather than doing it for them.

I mean, if someone has contrived to put an evil or nonfunctional brew on the $PATH, surely they can't be upset if an installer doesn't work as expected? #### Scott Morrison (Sep 19 2018 at 07:31): Having tried to clean up several broken attempts by mathematicians and students to install Lean by now, I would really like to take this stuff out of their hands :-) #### Scott Morrison (Sep 19 2018 at 07:32): I agree that power users don't want this! #### Scott Morrison (Sep 19 2018 at 07:33): If we're going to attempt something like this, it seems more sensible to me to put all the login in elan, and then have the VS Code extension just call elan. #### Mario Carneiro (Sep 19 2018 at 07:33): Maybe. But I'd still recommend giving the commands to the user and explaining it rather than doing it for them. No no, this is the source of too many problems #### Sean Leather (Sep 19 2018 at 07:34): You're welcome to do what you like, but, from past experience, I know that it's a bad idea. I can't tell you exactly what will go wrong, because things change and systems are complex, but I'm pretty sure something will go wrong. #### Scott Morrison (Sep 19 2018 at 07:34): Seeing what someone at Dagstuhl had managed to do with their windows path was pretty terrifying. :-) #### Mario Carneiro (Sep 19 2018 at 07:34): We already have a command sequence in a help file, it doesn't work half the time and the poor users don't know what to do #### Scott Morrison (Sep 19 2018 at 07:34): What if we instead put all the login in the VS Code, and #### Scott Morrison (Sep 19 2018 at 07:34): when something goes wrong #### Johan Commelin (Sep 19 2018 at 07:35): Talking about automatically fixing problems: If we detect windows, can't we just wipe it with a fresh Linux install? #### Sean Leather (Sep 19 2018 at 07:35): For Windows, an installer would be best. For Linux, a package would be best. For Mac, Homebrew would probably be best. #### Kevin Buzzard (Sep 19 2018 at 07:35): Ha ha there was a user over the summer whose Windows path rather eerily contained a bunch of directories on my laptop (/home/buzzard/Lean/whatever). #### Scott Morrison (Sep 19 2018 at 07:35): show a dialog that says "XXX not found. You may want to try running YYY in a terminal" #### Kevin Buzzard (Sep 19 2018 at 07:35): I just said "I think you can safely remove all those, they're on another system" #### Mario Carneiro (Sep 19 2018 at 07:35): "what's a terminal?" #### Scott Morrison (Sep 19 2018 at 07:35): :-) #### Scott Morrison (Sep 19 2018 at 07:36): A nice trick, because VS Code has an integrated terminal, is that we can actually pop up a terminal window #### Mario Carneiro (Sep 19 2018 at 07:36): or worse - "I installed cygwin (on linux) but it couldn't find the path" #### Scott Morrison (Sep 19 2018 at 07:36): and paste in the command the user needs #### Sean Leather (Sep 19 2018 at 07:36): BTW, there's a package manager for Windows: https://chocolatey.org/ #### Scott Morrison (Sep 19 2018 at 07:36): leaving them to just press "enter"? #### Scott Morrison (Sep 19 2018 at 07:37): Does elan currently do anything useful on windows? I have no idea. #### Kevin Buzzard (Sep 19 2018 at 07:37): I also noticed that some users, when you say "oh hold down shift", say "what's shift?" because a modern keyboard might well not have the word "shift" on it any more. Similarly for "enter" / "return". #### Mario Carneiro (Sep 19 2018 at 07:38): why not run a command that prints out the sequence of brew/whatever commands it will send, and says (y/n) #### Sean Leather (Sep 19 2018 at 07:39): Also, if you're going to do apt-get and/or brew, you'll want to update those first. #### Scott Morrison (Sep 19 2018 at 07:40): I'm pretty sure brew auto-updates these days. #### Sean Leather (Sep 19 2018 at 07:40): /usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"


And this is notoriously not secure.

#### Scott Morrison (Sep 19 2018 at 07:41):

Note our install instructions for elan are already of this form!

#### Sean Leather (Sep 19 2018 at 07:41):

I haven't seen them, but it's still true. :slight_smile:

#### Mario Carneiro (Sep 19 2018 at 07:46):

I'm not sure how you can in one line download and run a script from the internet without it being insecure

#### Mario Carneiro (Sep 19 2018 at 07:46):

that's like the definition of insecure

#### Sean Leather (Sep 19 2018 at 07:52):

In the end, it comes down to trust. https://brew.sh/ also suggests that command. I don't like it, but that's the way it is. In general, I would point to https://brew.sh when informing somebody to install brew. That way, they can read the information and become informed about what it is before installing it. Yes, one could decide to ignore the information, but at least they've been given the opportunity.

#### Sebastian Ullrich (Sep 19 2018 at 15:43):

Why do users need cmake...?

#### Sebastian Ullrich (Sep 19 2018 at 15:45):

That libgmp isn't included is basically a bug; I think it was at some point. Anyway, calling sudo may reasonably ask for a password, so the automatic installation should be in an interactive shell at the very least

#### Reid Barton (Sep 19 2018 at 15:55):

I didn't have to install cmake, but I did have to install coreutils for leanpkg. This was on a machine with no preinstalled brew on which I didn't have root access. brew says it can be installed anywhere but some packages may not be happy in nonstandard locations; I didn't have any difficulties though.

#### Reid Barton (Sep 19 2018 at 15:56):

Vscode could even install its own private brew installation

#### Reid Barton (Sep 19 2018 at 15:58):

Maybe it was elan not leanpkg that needed readlink, I think it was

#### Scott Morrison (Sep 24 2018 at 09:56):

I just updated my PR to vscode-lean, so hopefully after the VS Code Lean extension offers to install elan for you, it works first time (even though the \$PATH has not yet been updated).

#### Scott Morrison (Sep 24 2018 at 09:56):

Testing on other systems much appreciated.

#### Scott Morrison (Sep 24 2018 at 09:56):

I've gone back to the more conservative model of not pressing enter for the user during the elan script. :-)

#### Scott Morrison (Sep 24 2018 at 09:56):

Next up: testing this in Linux and Windows

#### Scott Morrison (Sep 24 2018 at 09:57):

after that, seeing if we can make elan more helpful when dependencies are missing.

#### Scott Morrison (Sep 24 2018 at 09:57):

https://github.com/leanprover/vscode-lean/pull/91

Last updated: May 11 2021 at 00:31 UTC