## Stream: new members

### Topic: Issue with git bash and python on Windows 10

#### Emily Bain (May 29 2020 at 22:45):

I am following the instructions to install Lean found here https://leanprover-community.github.io/install/windows.html. I followed the instructions up to "Run cp "$(which python)" "$(which python)"3", at which point I got the error bash: $'\302\226cp': command not found. I then tried just running python through git bash, i.e. elbai@DESKTOP-1E616F8 MINGW64 ~$ python


and it just hangs. It seems that this is a known issue: https://stackoverflow.com/questions/32597209/python-not-working-in-the-command-line-of-git-bash. The fix suggested in the thread of using winpty python doesn't quite work for me either, as it appears to do nothing, but then all text that I enter in the terminal window becomes invisible. This is also a known issue https://github.com/microsoft/vscode/issues/45693.

Anyway I tried a load of things and have somehow managed to get myself a python3 alias, although I still cannot run python from git bash, but I will try to work around it. I may use a different shell. Since I don't really know what worked I probably won't be very helpful in trying to work out a solution, but I thought I would make people aware of the issue anyway.

#### Patrick Lutz (May 29 2020 at 22:46):

It might be helpful to add alternative instructions for Windows that just use the Windows shell instead of git bash

#### Patrick Lutz (May 29 2020 at 22:47):

Add to the lean installation guide I mean

#### Bryan Gin-ge Chen (May 29 2020 at 22:48):

I'd proceed and see if you're able to install leanproject via pip and get it working. From the SO question it looks like this may just affect the python REPL, so it may not be relevant for Lean use.

#### Emily Bain (May 29 2020 at 22:49):

Patrick Lutz said:

It might be helpful to add alternative instructions for Windows that just use the Windows shell instead of git bash

I'm trying with wsl, which is like a linux shell within windows. It'll be nice if it works!

#### Patrick Lutz (May 29 2020 at 22:52):

Bryan Gin-ge Chen said:

I'd proceed and see if you're able to install leanproject via pip and get it working. From the SO question it looks like this may just affect the python REPL, so it may not be relevant for Lean use.

If so that would be useful to add to the installation instructions

#### Bryan Gin-ge Chen (May 29 2020 at 22:54):

Yes, I think the installation instructions should be updated. If anyone successfully gets Lean working on windows and wants to write up their process, a PR here would be appreciated: https://github.com/leanprover-community/leanprover-community.github.io/pulls

#### Patrick Lutz (May 29 2020 at 22:55):

Bryan Gin-ge Chen said:

Yes, I think the installation instructions should be updated. If anyone successfully gets Lean working on windows and wants to write up their process, a PR here would be appreciated: https://github.com/leanprover-community/leanprover-community.github.io/pulls

I think @Thomas Browning successfully installed Lean on Windows, but I don't think he encountered this problem

#### Dan Stanescu (May 29 2020 at 22:55):

@Bryan Gin-ge Chen Bryan, could we not use Anaconda? Is there any conflict with Lean?

#### Emily Bain (May 29 2020 at 22:56):

It all seems to be working for me now.

#### Bryan Gin-ge Chen (May 29 2020 at 22:56):

You can use Anaconda. I've been using Anaconda python + git bash on Windows.

#### Patrick Lutz (May 29 2020 at 22:56):

Dan Stanescu said:

Bryan Gin-ge Chen Bryan, could we not use Anaconda? Is there any conflict with Lean?

I used anaconda on Ubuntu and it was fine

#### Bryan Gin-ge Chen (May 29 2020 at 22:56):

I think we just didn't want to recommend an Anaconda install to casual users.

#### Patrick Lutz (May 29 2020 at 22:57):

Emily Bain said:

It all seems to be working for me now.

So just using a different shell made everything work fine?

#### Emily Bain (May 29 2020 at 22:57):

The issue is only with git bash it seems, but would be interesting to see how many other windows 10 users encountered the same problem. If it is everyone then it would seem worth updating the instructions.

#### Emily Bain (May 29 2020 at 22:58):

Patrick Lutz said:

Emily Bain said:

It all seems to be working for me now.

So just using a different shell made everything work fine?

Yes, I think I overestimated how much the shell was actually needed for. I've set my default shell in VS Code to wsl, which hopefully shouldn't cause too many problems since it is literally an ubuntu shell.

Last updated: May 11 2021 at 12:15 UTC