Zulip Chat Archive

Stream: general

Topic: vscode extension installs Lean


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

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:20):

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

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:23):

Screenshot-2018-09-17-22.22.30.png Screenshot-2018-09-17-22.22.36.png

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

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:23):

1) Install the VS Code extension

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:23):

2) Open a Lean file

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

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:24):

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

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

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

view this post on Zulip Scott Morrison (Sep 17 2018 at 12:26):

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

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

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

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

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

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

view this post on Zulip Sebastian Ullrich (Sep 17 2018 at 16:14):

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

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

view this post on Zulip Scott Morrison (Sep 17 2018 at 20:01):

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:19):

would get most non-windows users going a bit faster

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:19):

heck, in the osx branch add

xcode-select --install
brew --version || /usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:21):

I'd be happy to make the PR, if something like this could be accepted.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:21):

The combination of VS Code giving a button to run elan, and elan attempting to fill in missing dependencies, could be very helpful.

view this post on Zulip Sean Leather (Sep 19 2018 at 07:22):

I don't mean to be difficult, but I think that's a really bad idea to have elan run apt-get or brew.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:23):

Why is that?

view this post on Zulip Sean Leather (Sep 19 2018 at 07:23):

Who knows what state the user's computer is in?

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:23):

(I am ignorant here)

view this post on Zulip Sean Leather (Sep 19 2018 at 07:23):

You could and probably will break something.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:23):

I guess an alternative is to fail and say "hey, you might want to type apt install gmp" or some such

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:23):

Ok!

view this post on Zulip Sean Leather (Sep 19 2018 at 07:23):

Sure, that's a good option.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:24):

Ok --- maybe I will continue tweaking the VS Code extension

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:24):

I don't really see how an apt-get command like that will break anything, at worst it will fail

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:24):

It is easy enough for it to analyze the error messages and tell you what to run.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:25):

I feel like for 99% of users that apt-get or brew command is going to be the right thing to do, and moreover for 90% of users they won't even know what it means when they run it. :-)

view this post on Zulip Sean Leather (Sep 19 2018 at 07:25):

Even if it wouldn't break anything, it's a bad idea to install software without the user having control over it. And if the user doesn't know what it's doing, that's even worse.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:25):

Ok -- I will go with dialogs that provide hints.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:25):

don't package managers themselves do this routinely?

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:26):

the user has control over the large scale execution, that is sufficient

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:27):

I think it should ask the same questions you normally see in an installer, but otherwise go about its business completely automatically

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:27):

complicated questions will just cause confusion, a power user doesn't need to use this method at all

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:28):

e.g. elan could show a prompt: "It looks like you don't have libgmp installed. Would you like to install this using brew install libgmp?"

view this post on Zulip Sean Leather (Sep 19 2018 at 07:29):

e.g. elan could show a prompt: "It looks like you don't have libgmp installed. Would you like to install this using brew install libgmp?"

In order to do that, you need to know if brew is installed.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:29):

Of course

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:29):

but detecting the operating system is easy

view this post on Zulip Sean Leather (Sep 19 2018 at 07:29):

And brew in the $PATH may not be the brew you expect, so you'd have to test for the right brew.

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:30):

and running brew --version is harmless, surely?

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:30):

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?

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:32):

I agree that power users don't want this!

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

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

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:34):

Seeing what someone at Dagstuhl had managed to do with their windows path was pretty terrifying. :-)

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:34):

What if we instead put all the login in the VS Code, and

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:34):

when something goes wrong

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:35):

I just said "I think you can safely remove all those, they're on another system"

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:35):

"what's a terminal?"

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:35):

:-)

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

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:36):

or worse - "I installed cygwin (on linux) but it couldn't find the path"

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:36):

and paste in the command the user needs

view this post on Zulip Sean Leather (Sep 19 2018 at 07:36):

BTW, there's a package manager for Windows: https://chocolatey.org/

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:36):

leaving them to just press "enter"?

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:37):

Does elan currently do anything useful on windows? I have no idea.

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

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

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:40):

I'm pretty sure brew auto-updates these days.

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

view this post on Zulip Scott Morrison (Sep 19 2018 at 07:41):

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

view this post on Zulip Sean Leather (Sep 19 2018 at 07:41):

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

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

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:46):

that's like the definition of insecure

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

view this post on Zulip Sebastian Ullrich (Sep 19 2018 at 15:43):

Why do users need cmake...?

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

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

view this post on Zulip Reid Barton (Sep 19 2018 at 15:56):

Vscode could even install its own private brew installation

view this post on Zulip Reid Barton (Sep 19 2018 at 15:58):

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

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

view this post on Zulip Scott Morrison (Sep 24 2018 at 09:56):

Testing on other systems much appreciated.

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

view this post on Zulip Scott Morrison (Sep 24 2018 at 09:56):

Next up: testing this in Linux and Windows

view this post on Zulip Scott Morrison (Sep 24 2018 at 09:57):

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

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