Issue with git bash and python on Windows 10

Stream: new members

[Emily Bain]

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]

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

[Patrick Lutz]

Add to the lean installation guide I mean

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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

[Emily Bain]

It all seems to be working for me now.

[Bryan Gin-ge Chen]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

Emily Bain said:

It all seems to be working for me now.

So just using a different shell made everything work fine?

[Emily Bain]

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]

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.