Zulip Chat Archive

Stream: general

Topic: pip install mathlibtools


view this post on Zulip Patrick Massot (Dec 28 2019 at 18:13):

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.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:14):

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?

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:15):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:15):

or pip3 install --user mathlibtools

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:15):

without any workon stuff?

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:16):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:17):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:17):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:18):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:18):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:19):

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.

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:19):

I have 55 of them!

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:19):

Who has more?

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:19):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:21):

I have update-motd -- will that do?

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:21):

no

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:21):

I have no ~/.mathlib

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:21):

Could you try to sudo pip3 install mathlibtools version?

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:22):

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?

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:22):

None of those.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:22):

Could you try to sudo pip3 install mathlibtools version?

Is this some trick to hack me?

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:23):

$ 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:~$

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:23):

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.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:23):

My python3 is Python 3.6.9, I notice

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:24):

once installed mathlibtools seems to work well for me

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:24):

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

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:24):

$ 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.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:26):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:27):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:28):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:28):

My python is now 3.7.1

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:28):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:29):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:29):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:30):

(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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:30):

What is in you leanpkg.toml?

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:30):

eew that's my fault

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:30):

April 2018!

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:31):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:31):

$ 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??

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:31):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:32):

lean-version has to be lean-3.4.2.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:32):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:33):

OK I'm now back out of the format_lean venv

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:33):

and inspecting $HOME/.local/bin

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:33):

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$

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:34):

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

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:34):

It's not in my PATH though

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:35):

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)

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:39):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:39):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:42):

can you try a bare pip install mathlibtools?

view this post on Zulip Patrick Massot (Dec 28 2019 at 18:42):

and then which update-mathlib

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:51):

$ 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?

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:51):

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

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:54):

@Kevin Buzzard What does the which pip command say?

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:55):

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.

view this post on Zulip Kevin Buzzard (Dec 28 2019 at 18:56):

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

view this post on Zulip Etienne Laurin (Dec 28 2019 at 18:57):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 19:15):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 19:25):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 19:33):

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

view this post on Zulip Etienne Laurin (Dec 28 2019 at 19:49):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 20:15):

What if you try a system install?

view this post on Zulip Etienne Laurin (Dec 28 2019 at 21:42):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 21:49):

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

view this post on Zulip Etienne Laurin (Dec 28 2019 at 21:51):

Yep, that's where.

view this post on Zulip Patrick Massot (Dec 28 2019 at 21:53):

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.

view this post on Zulip Etienne Laurin (Dec 28 2019 at 22:02):

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

view this post on Zulip Patrick Massot (Dec 28 2019 at 22:07):

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


Last updated: May 16 2021 at 21:11 UTC