Zulip Chat Archive

Stream: general

Topic: Bug in Downloading


Sian Carey (Jul 01 2019 at 11:52):

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 (Jul 01 2019 at 11:59):

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 (Jul 01 2019 at 12:16):

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

Kevin Buzzard (Jul 02 2019 at 11:13):

(deleted)

Kevin Buzzard (Jul 02 2019 at 11:14):

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

Kevin Buzzard (Jul 02 2019 at 12:04):

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 (Jul 02 2019 at 12:09):

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 (Jul 02 2019 at 12:10):

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

Floris van Doorn (Jul 02 2019 at 13:35):

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.


Last updated: Dec 20 2023 at 11:08 UTC