search

leanprover / elan

The Lean version manager
Apache License 2.0
297 stars 34 forks source link

remove additional redundant "press any key to exit" #45

Closed lovettchris closed 2 years ago

lovettchris commented 2 years ago

fix: remove additional redundant "press any key to exit" that was happening only on windows. fix: remove reference to "Lean 3" in NoDefaultToolchain error message.

The reason for this "where installation happens in a console that may have opened just for this purpose" is no longer valid. The latest vscode extension when you install elan, you now get "press any key to continue" twice, which is odd, so this fixes that making the vscode extension experience consistent across platforms.

Kha commented 2 years ago

A bit late, but I hope this doesn't break/affect the Lean 3 extension's Lean installation? /cc @gebner

lovettchris commented 2 years ago

A bit late, but I hope this doesn't break/affect the Lean 3 extension's Lean installation? /cc @gebner

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

gebner commented 2 years ago

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

From what I can tell, the change isn't released yet, right?

Either way, the change looks innocent enough and I don't expect it to break anything. To be on the safe side we could post a heads-up on zulip once the release is out.

lovettchris commented 2 years ago

I just tested bootstrapping of lean3 from the vscode lean3 extension and it was able to download and install lean just fine, so looks like it still works.

From what I can tell, the change isn't released yet, right?

Either way, the change looks innocent enough and I don't expect it to break anything. To be on the safe side we could post a heads-up on zulip once the release is out.

I installed https://github.com/leanprover/vscode-lean changed it to run my locally build elan-init.sh and then invoke my locally built elan-init.exe and it worked fine, including the press enter key to continue prompt.

image

Kha commented 2 years ago

It's at https://github.com/leanprover/vscode-lean. But I made testing easier by going ahead and releasing the change :) .

lovettchris commented 2 years ago

It's at https://github.com/leanprover/vscode-lean. But I made testing easier by going ahead and releasing the change :) .

Thanks, I tested version 1.1.1 and found another redundant prompt... See https://github.com/leanprover/elan/pull/48