Zulip Chat Archive

Stream: new members

Topic: Can't select Bash as Default Shell


view this post on Zulip n Simplex Pachinko (Mar 22 2021 at 19:10):

Hello,
I'm attempting to install VS Code correctly. I have made it down the installation instructions (https://leanprover-community.github.io/install/windows.html) to as far as "install leanprover extension" to VS Code, and I am now attempting to select Bash as the default shell.
I hit Ctrl-Shift-p, which brought up the palette, I typed "select default", which showed "Terminal: Select Default Shell" as the only available option. When I clicked it, it states that the only two available shells are Command Prompt and Windows PowerShell.

My Bash is installed into a non-default location. Is that an issue?
I turned the External: Windows Exec path to the path of git-bash.exe . I then entered a test file and typed #lean 1+1 and it threw an error: "command expected Lean [1, 1]"
Anyone know where I'm going wrong?

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 19:11):

#lean 1+1 isn't a command. How about #check 1+1?

view this post on Zulip n Simplex Pachinko (Mar 22 2021 at 19:12):

Hmm. True. I thought that the first time, I actually put in "#eval 1+1" per the help file, but just mistyped, but it's working now, either way.

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 19:13):

PS I am not at all sure that changing the default shell is an essential part of the installation process; I would be tempted to just not worry. #check 1+1 will tell you that it's a natural number, #eval 1+1 will tell you which one it is.

view this post on Zulip n Simplex Pachinko (Mar 22 2021 at 19:15):

Now it has an "Info" problem: "2 Lean [1, 1]" . The 2 (line number?) is white, the rest is gray. This probably doesn't matter, since I'm getting the right answer. Thank you! Off to do the Natural Number Game.

view this post on Zulip Mario Carneiro (Mar 22 2021 at 21:47):

That's what it's supposed to look like

view this post on Zulip Mario Carneiro (Mar 22 2021 at 21:47):

The 2 is the result, the Lean is some extra info that vscode displays about the source of the hover text


Last updated: May 17 2021 at 22:15 UTC