## Stream: new members

### Topic: Can't select Bash as Default Shell

#### 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?

#### Kevin Buzzard (Mar 22 2021 at 19:11):

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

#### 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.

#### 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.

#### 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.

#### Mario Carneiro (Mar 22 2021 at 21:47):

That's what it's supposed to look like

#### 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