Zulip Chat Archive

Stream: new members

Topic: Issue with git bash and python on Windows 10


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

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

view this post on Zulip Patrick Lutz (May 29 2020 at 22:47):

Add to the lean installation guide I mean

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

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

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

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

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

view this post on Zulip Dan Stanescu (May 29 2020 at 22:55):

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

view this post on Zulip Emily Bain (May 29 2020 at 22:56):

It all seems to be working for me now.

view this post on Zulip Bryan Gin-ge Chen (May 29 2020 at 22:56):

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

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

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

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

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

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