Bug in Downloading

Stream: general

[Sian Carey]

Heya, I'm trying to download lean to start learning, and have a windows laptop. I followed the instructions on the website exactly and everything worked except I can't install the mathlib supporting tools. I have downloaded python however git bash can't seem to find it. The exact error message is:
Installing python dependencies (at user level)
which: no pip3 in (/c/Users/sian/.elan/bin:/c/Users/sian/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/sian/bin:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/iCLS:/c/Program Files/Intel/Intel(R) Management Engine Components/iCLS:/c/WINDOWS/system32:/c/WINDOWS:/c/WINDOWS/System32/Wbem:/c/WINDOWS/System32/WindowsPowerShell/v1.0:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/IPT:/c/Program Files/Intel/Intel(R) Management Engine Components/IPT:/c/WINDOWS/System32/OpenSSH:/c/Program Files/MATLAB/R2018a/bin:/cmd:/c/Users/sian/.elan/bin:/c/Users/sian/AppData/Local/Microsoft/WindowsApps:/c/texlive/2018/bin/win32:/c/Users/sian/AppData/Local/Programs/Microsoft VS Code/bin:/usr/bin/vendor_perl:/usr/bin/core_perl)
which: no apt-get in (/c/Users/sian/.elan/bin:/c/Users/sian/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/sian/bin:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/iCLS:/c/Program Files/Intel/Intel(R) Management Engine Components/iCLS:/c/WINDOWS/system32:/c/WINDOWS:/c/WINDOWS/System32/Wbem:/c/WINDOWS/System32/WindowsPowerShell/v1.0:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/IPT:/c/Program Files/Intel/Intel(R) Management Engine Components/IPT:/c/WINDOWS/System32/OpenSSH:/c/Program Files/MATLAB/R2018a/bin:/cmd:/c/Users/sian/.elan/bin:/c/Users/sian/AppData/Local/Microsoft/WindowsApps:/c/texlive/2018/bin/win32:/c/Users/sian/AppData/Local/Programs/Microsoft VS Code/bin:/usr/bin/vendor_perl:/usr/bin/core_perl)
which: no brew in (/c/Users/sian/.elan/bin:/c/Users/sian/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/sian/bin:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/iCLS:/c/Program Files/Intel/Intel(R) Management Engine Components/iCLS:/c/WINDOWS/system32:/c/WINDOWS:/c/WINDOWS/System32/Wbem:/c/WINDOWS/System32/WindowsPowerShell/v1.0:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/IPT:/c/Program Files/Intel/Intel(R) Management Engine Components/IPT:/c/WINDOWS/System32/OpenSSH:/c/Program Files/MATLAB/R2018a/bin:/cmd:/c/Users/sian/.elan/bin:/c/Users/sian/AppData/Local/Microsoft/WindowsApps:/c/texlive/2018/bin/win32:/c/Users/sian/AppData/Local/Programs/Microsoft VS Code/bin:/usr/bin/vendor_perl:/usr/bin/core_perl)
which: no choco in (/c/Users/sian/.elan/bin:/c/Users/sian/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/sian/bin:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/iCLS:/c/Program Files/Intel/Intel(R) Management Engine Components/iCLS:/c/WINDOWS/system32:/c/WINDOWS:/c/WINDOWS/System32/Wbem:/c/WINDOWS/System32/WindowsPowerShell/v1.0:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files/Intel/Intel(R) Management Engine Components/DAL:/c/Program Files (x86)/Intel/Intel(R) Management Engine Components/IPT:/c/Program Files/Intel/Intel(R) Management Engine Components/IPT:/c/WINDOWS/System32/OpenSSH:/c/Program Files/MATLAB/R2018a/bin:/cmd:/c/Users/sian/.elan/bin:/c/Users/sian/AppData/Local/Microsoft/WindowsApps:/c/texlive/2018/bin/win32:/c/Users/sian/AppData/Local/Programs/Microsoft VS Code/bin:/usr/bin/vendor_perl:/usr/bin/core_perl)
python3 and pip3 not found. First install python3 and pip3 and then install update-mathlib

How can I fix this?
Thanks!

[Floris van Doorn]

Please use the installation instructions I PR'd today: https://github.com/leanprover-community/mathlib/blob/windows/docs/install/windows.md

In particular:
If pip3 --version doesn't give any output, run the command python3 -m pip install --upgrade pip, which should fix it.

[Patrick Massot]

Great! If Sian manages to use these instructions I'll merge them right away.

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(sorry, I've forgotten how far we got)

[Kevin Buzzard]

OK the instructions work! Why is it so complicated? I guess that's another question. But Sian and I managed to follow them.

[Patrick Massot]

It's complicated because no Windows user made the effort to provide a shorter install procedure. Neil tried something at some point, but I don't think it was maintained

[Chris Hughes]

Do they work if you have a space in your username?

[Floris van Doorn]

Do they work if you have a space in your username?

I haven't tried that, but I don't see a step where it would go wrong.