pip install mathlibtools

Stream: general

[Patrick Massot]

I just created a python package for our mathlib supporting tools at https://pypi.org/project/mathlibtools/0.0.1/. We now need as many people as possible to try it in various settings. In order to help the community in this new adventure, you only need to:

• make sure your installation of update-mathlib (if any) gets out of the way. It probably means moving $HOME/.mathlib/bin/ somewhere your shell won't look at.
• Make sure you have some version of python (at least python 3.5) with a working pip command, preferably in a weird setup (windows, multiple versions of python installed in conflicting ways...)
• try pip install mathlibtools (or pip3 install ... or sudo pip install ... or pip install --user or whatever variation you can think of).
• go to the root folder of a lean project using lean-3.4.2 and mathlib and type update-mathlib (see this doc if you don't know how to make one)
• if you know what they are meant to do, you can also try cache-olean and setup-lean-git-hooks
• Report here.

[Kevin Buzzard]

I am an ideal candidate for this because I'm using Ubuntu which has python2 by default. But doesn't this mean that it just won't work? Do I need to go into some python3 environment first?

[Patrick Massot]

You probably need to use sudo pip3 install mathlib-tools.

[Patrick Massot]

or pip3 install --user mathlibtools

[Kevin Buzzard]

without any workon stuff?

[Patrick Massot]

You can also try in a virtualenv (ie. after workon) but this would be a different test case.

[Kevin Buzzard]

ooh I've never been in ~/.mathlib before. I seem to have 39 files called things like mathlib-olean-nightly-2019-05-23.tar.gz

[Kevin Buzzard]

oh man I also have my hooks for when I work on mathlib. Should I move them too?

[Patrick Massot]

If you intend to test setup-lean-git-hooks then you should also move that folder away, just to make sure.

[Kevin Buzzard]

Ok I'll just move all of .mathlib out of the way

[Patrick Massot]

Your 39 files are all the compiled versions of mathlib that update-mathlib ever downloaded for you. We could have a contest to see who is the greatest update-mathlib user.

[Patrick Massot]

I have 55 of them!

[Patrick Massot]

Who has more?

[Kevin Buzzard]

I typed pip3 install --user mathlibtools and now I have no command update-mathlib

[Kevin Buzzard]

I have update-motd -- will that do?

[Patrick Massot]

no

[Kevin Buzzard]

I have no ~/.mathlib

[Patrick Massot]

Could you try to sudo pip3 install mathlibtools version?

[Kevin Buzzard]

Before I do that, can you clarify if my PATH is supposed to have changed, or if I am now supposed to have a ~/.mathlib?

[Patrick Massot]

None of those.

[Kevin Buzzard]

Could you try to sudo pip3 install mathlibtools version?

Is this some trick to hack me?

[Kevin Buzzard]

$ sudo pip3 install mathlibtools
[sudo] password for buzzard:
The directory '/home/buzzard/.cache/pip/http' or its parent directory is not owned by the current user and the cache has been disabled. Please check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
The directory '/home/buzzard/.cache/pip' or its parent directory is not owned by the current user and caching wheels has been disabled. check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
Requirement already satisfied: mathlibtools in ./.local/lib/python3.6/site-packages
Requirement already satisfied: toml in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: certifi in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: gitpython in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: requests in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: PyGithub in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: gitdb2>=2.0.0 in ./.local/lib/python3.6/site-packages (from gitpython->mathlibtools)
Requirement already satisfied: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: idna<2.9,>=2.5 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: chardet<3.1.0,>=3.0.2 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: deprecated in ./.local/lib/python3.6/site-packages (from PyGithub->mathlibtools)
Requirement already satisfied: pyjwt in ./.local/lib/python3.6/site-packages (from PyGithub->mathlibtools)
Requirement already satisfied: six in ./.local/lib/python3.6/site-packages (from PyGithub->mathlibtools)
Requirement already satisfied: smmap2>=2.0.0 in ./.local/lib/python3.6/site-packages (from gitdb2>=2.0.0->gitpython->mathlibtools)
Requirement already satisfied: wrapt<2,>=1.10 in ./.local/lib/python3.6/site-packages (from deprecated->PyGithub->mathlibtools)
buzzard@bob:~$

[Etienne Laurin]

If you use pip3 with --user, the package gets installed in a different folder that might not be in your path. You can run python3 -c 'import site; print(site.USER_SITE)' to see where.

[Kevin Buzzard]

My python3 is Python 3.6.9, I notice

[Etienne Laurin]

once installed mathlibtools seems to work well for me

[Patrick Massot]

Hey, Kevin's pip still tried a user space install.

[Etienne Laurin]

$ virtualenv -p python3.7 .py
$ .py/bin/pip install mathlibtools
Successfully installed mathlibtools-0.0.1
$ .py/bin/update-mathlib
Querying GitHub...
Reusing cached olean archive
... successfully extracted olean archive.

[Kevin Buzzard]

This will all be Ubuntu's default set-up for python3.

$ dpkg -S /usr/bin/python3
python3-minimal: /usr/bin/python3
buzzard@bob:~$

because I have no idea how python2/3/whatever works, all I ever do is use the Ubuntu package manager to install python packages

[Patrick Massot]

Kevin, do you see anything in $HOME/.local/bin/?

[Kevin Buzzard]

OK so if I do workon format_lean (Patrick this is the set-up you explain in the format_lean docs) and then pip install mathlibtools then it seems to work

[Kevin Buzzard]

My python is now 3.7.1

[Patrick Massot]

Ok, this is good but not good enough. It should also work outside of a virtual env.

[Patrick Massot]

Do you see anything in $HOME/.local/bin/?

[Kevin Buzzard]

[I'm just actually testing update-mathlib, hang on]

[Kevin Buzzard]

(format_lean) buzzard@bob:~/lean-projects/test$ update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Error: no nightly archive found
no cache found

[Patrick Massot]

What is in you leanpkg.toml?

[Kevin Buzzard]

eew that's my fault

[Kevin Buzzard]

April 2018!

[Patrick Massot]

I would be easier to test that in a project where update-mathlib used to work.

[Kevin Buzzard]

$ more leanpkg.toml
[package]
name = "test"
version = "0.1"
lean_version = "nightly-2018-04-06"
path = "src"

[dependencies]
lean-lib = {git = "https://github.com/unitb/lean-lib", rev = "1ccbd0da9d71eac905559f8ca6768098f5ed617e"}
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "5df2ee70cfd576e6fa11359496a8a06c029151c9"}
(format_lean) buzzard@bob:~/lean-projects/test$

How did that happen??

[Kevin Buzzard]

oh I'm an idiot, all my fault. My "new" test repo already existed

[Patrick Massot]

lean-version has to be lean-3.4.2.

[Kevin Buzzard]

Yes! I think that test dir was there from years ago. It all works fine.

[Kevin Buzzard]

OK I'm now back out of the format_lean venv

[Patrick Massot]

and inspecting $HOME/.local/bin

[Kevin Buzzard]

buzzard@bob:~/.local/bin$ ls -l
total 292
-rwxr-xr-x 1 buzzard buzzard  3694 Dec 28 18:19 cache-olean
-rwxr-xr-x 1 buzzard buzzard   225 Dec 28 18:19 chardetect
-rwxr-xr-x 1 buzzard buzzard   234 Nov 16 21:40 easy_install
-rwxr-xr-x 1 buzzard buzzard   234 Nov 16 21:40 easy_install-3.6
-rwxr-xr-x 1 buzzard buzzard   212 Feb  9  2019 flask
-rwxr-xr-x 1 buzzard buzzard   235 Feb  9  2019 iptest
-rwxr-xr-x 1 buzzard buzzard   235 Feb  9  2019 iptest3
-rwxr-xr-x 1 buzzard buzzard   228 Feb  9  2019 ipython
-rwxr-xr-x 1 buzzard buzzard   228 Feb  9  2019 ipython3
-rwxr-xr-x 1 buzzard buzzard   236 Feb  9  2019 pbr
-rwxrwxr-x 1 buzzard buzzard   214 Apr 14  2018 pip
-rwxrwxr-x 1 buzzard buzzard   214 Apr 14  2018 pip2
-rwxrwxr-x 1 buzzard buzzard   214 Apr 14  2018 pip2.7
-rwxr-xr-x 1 buzzard buzzard   219 Feb  9  2019 pygmentize
-rwxr-xr-x 1 buzzard buzzard   215 Dec 28 18:19 pyjwt
-rwxr-xr-x 1 buzzard buzzard   685 Dec 28 18:19 setup-lean-git-hooks
-rwxr-xr-x 1 buzzard buzzard  1341 Dec 28 18:19 update-mathlib
-rwxr-xr-x 1 buzzard buzzard   234 Feb  9  2019 virtualenv
-rwxr-xr-x 1 buzzard buzzard   239 Feb  9  2019 virtualenv-clone
-rwxr-xr-x 1 buzzard buzzard  2210 Feb  9  2019 virtualenvwrapper_lazy.sh
-rwxr-xr-x 1 buzzard buzzard 41697 Feb  9  2019 virtualenvwrapper.sh
buzzard@bob:~/.local/bin$

[Patrick Massot]

Ok, so the issue is that .local/bin in not in your path, but this is where pip3 install --user puts its executable files.

[Kevin Buzzard]

It's not in my PATH though

[Kevin Buzzard]

Ubuntu says

buzzard@bob:~$ echo $PATH
/home/buzzard/.pyenv/bin:/home/buzzard/.mathlib/bin:/home/buzzard/.mathlib/bin:/home/buzzard/.elan/bin:/home/buzzard/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/usr/local/java/jdk1.8.0_77/bin:/usr/local/java/jdk1.8.0_77/jre/bin:/home/buzzard/Encfs/bin:/home/buzzard/Dropbox/bin

(I put the last two or three there myself)

[Patrick Massot]

The fact that the sudo version doesn't work is probably pyenv messing up things.

[Patrick Massot]

The --user issue seems to be a known but unfixed issue: https://github.com/pypa/pip/issues/3813

[Patrick Massot]

can you try a bare pip install mathlibtools?

[Patrick Massot]

and then which update-mathlib

[Kevin Buzzard]

$ pip
Traceback (most recent call last):
  File "/usr/bin/pip", line 9, in <module>
    from pip import main
ImportError: cannot import name main

This doesn't bode well, right?

[Etienne Laurin]

@Patrick Massot This new update-mathlib seems to overwrite ./src instead of _target/deps/mathlib/src

[Etienne Laurin]

@Kevin Buzzard What does the which pip command say?

[Kevin Buzzard]

I think I once did something which nobody should do with pip. I once googled this. This will be a python2 pip and I never use python2.

[Kevin Buzzard]

pip3 install mathlibtools works fine (but doesn't put update-mathlib anywhere where my path spots it)

[Etienne Laurin]

What does the which pip3 command report? It looks like you may be using a non-system pip3 from /home/buzzard/.pyenv/bin

[Patrick Massot]

Oops, this src issue is a bug I introduced while refactoring a bit. I shouldn't have done that at the same time.

[Patrick Massot]

@Etienne Laurin I pushed a fix to pypi, thanks!

[Patrick Massot]

Étienne, can you confirm that installation worked for you without fiddling with PATH?

[Etienne Laurin]

Yes, but I used a virtualenv and invoke update-mathlib using a relative path.

[Patrick Massot]

What if you try a system install?

[Etienne Laurin]

sudo pip3 install mathlibtools installs to my path but pip3 install mathlib doesn't.

[Patrick Massot]

And can you see where pip3 install puts it? Is it in $HOME/.local/bin?

[Etienne Laurin]

Yep, that's where.

[Patrick Massot]

Do you think this is still an improvement over the current situation? We currently need to tweak the path, but had control to where the script ended up. Now we loose control but it should end up in a more standard place.

[Etienne Laurin]

I like that it's more universal, I don't have Ubuntu or Windows, the pip package makes it easier to use for me.

[Patrick Massot]

Good. Thank you very much for testing this. I wish more people could try...