leanproject hooks

Stream: general

[Scott Morrison]

The post-checkout hook the leanproject hooks installs says:

if [ "$CHANGED_BRANCH" -eq "1" ]; then
    if /usr/bin/env python3 -c ""; then
                echo "Trying to fetch cached olean"
                leanproject get-cache
                leanproject get-mathlib-cache
                leanproject delete-zombies
    else
        echo "'env python3' failed; not running post-checkout hook"
    fi
fi

[Scott Morrison]

it seems that when working on mathlib itself, this results in two separate rounds of attempting to download oleans, once from get-cache and once from get-mathlib-cache.

[Bryan Gin-ge Chen]

I've noticed that too!

[Patrick Massot]

I never used any of those hooks so feel free to modify them to whatever pleases you.

[Scott Morrison]

okay. Can we also arrange that the cache only contains olean files, and no lean files? To often I clobber my local changes by loading from the cache.

[Scott Morrison]

I think it used to be necessary to have to lean files, because of how timestamps were used, but now it is probably completely unnecessary.

[Scott Morrison]

Perhaps removing them entirely, if that's viable, would also reduce the size of the downloads.

[Oliver Nash]

Scott Morrison said:

okay. Can we also arrange that the cache only contains olean files, and no lean files? To often I clobber my local changes by loading from the cache.

Is this not protected against by the dirty repo check?

[Scott Morrison]

Yesterday I lost some work --- I think what was happening was that I was just hacking on master, then I ran git checkout -b new_branch (without any commit or stash), and some files disappeared. I agree that doesn't sound explicable, so perhaps I did something dumber. If it happens again I'll note more carefully what I'd done.

[Bhavik Mehta]

I've also lost some work from hooks by doing something similar to this

[Patrick Stevens]

A mere git checkout -b will not lose any work - I assert that this is completely impossible

[Patrick Stevens]

Ah, hooks - it is possible, I take it all back, but you'll need a hook that deletes files

[Patrick Stevens]

Carry on :P

[Scott Morrison]

The problem is that it is a hook that unzips a zip files, containing potentially old copies of files in the repo!

[Scott Morrison]

I've confirmed this happens again. The problem is when running both

        leanproject get-cache
        leanproject get-mathlib-cache

from post-checkout, if you're in a copy of mathlib itself it seems the get-mathlib-cache doesn't correctly check for a dirty repository, and just clobbers the files.

[Scott Morrison]

We should kill two birds with one stone and just not do the get-mathlib-cache if we're in a copy of mathlib!

[Kenny Lau]

or commit before checkout

[Scott Morrison]

The problem is I always find myself on the wrong branch, and want to use git checkout -b XXX to make a new branch. The current behaviour makes this impossible.

[Scott Morrison]

(Or rather, I have to git stash in order to do it safely.)

[Patrick Massot]

I'm sorry about that Scott. Really someone who cares about those hooks should work on them. In the mean time I pushed a tweak that reroutes get-mathlib-cache to get-cache (which does check the repo is clean) when ran inside mathlib.

[Patrick Massot]

I also merged the command prefix. It would be very nice to have couple of people installing the current master of mathlibtools and test in real conditions today so that I can release a new version before the workshop.

[Kevin Buzzard]

The big problem I have with mathlibtools is that I even m never know what to do when my collaborator changes leanpkg.toml . I'm not sure I can deal with this within the leanproject framework, I always have to fix things up by hand

[Kevin Buzzard]

The problem with using leanproject is that if people have actually changed eg linarith.lean to linarith/basic.lean then I can't get leanproject to tidy up correctly

[Johan Commelin]

Weird... I don't recognise the problem. For me it works like a charm.

[Kevin Buzzard]

What works?

[Kevin Buzzard]

The question is how to update my local mathlib to the version which my collaborator wants, which might not be the current mathlib

[Johan Commelin]

If people move files around or change tomls, leanproject up just gives me a project that I can work with.

[Johan Commelin]

leanproject get-mathlib-cache should do that, if you are working on a project that is not mathlib.

[Kevin Buzzard]

I think leanproject up will update mathlib. I don't want to bump mathlib to master though, I want to bump it to the commit in the toml

[Kevin Buzzard]

Right, and get-mathlib-cache is exactly what I'm saying doesn't always work

[Kevin Buzzard]

Because then imports can become ambiguous if there are structural changes to mathlib

[Kevin Buzzard]

I'll make an issue. I've seen it several times now.

[Kevin Buzzard]

By structural changes I mean that foo.lean becomes foo/basic.lean

[Johan Commelin]

Aha... I guess I've not been in that spot often enough to have noticed the problems.

[Patrick Stevens]

Scott Morrison said:

The problem is I always find myself on the wrong branch, and want to use git checkout -b XXX to make a new branch. The current behaviour makes this impossible.

You could always commit, then git checkout -b, then git checkout -, then git reset --hard HEAD^.

[Patrick Massot]

Kevin, I have no idea what you are talking about.

[Patrick Massot]

If you open an issue then please list precise steps reproducing your problem. Opening an issue with what you wrote above would be useless since we wouldn't have any action we could take.

[Kevin Buzzard]

@Patrick Stevens yes I know I can fix it, the point is that I can't fix it solely by using leanproject. @Patrick Massot I'll make an example.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib-tools/issues/70 Patrick M I've attempted to explain the problem I'm seeing.

[Scott Morrison]

Patrick Massot said:

I'm sorry about that Scott. Really someone who cares about those hooks should work on them. In the mean time I pushed a tweak that reroutes get-mathlib-cache to get-cache (which does check the repo is clean) when ran inside mathlib.

Fixed in https://github.com/leanprover-community/mathlib-tools/pull/71

[Patrick Massot]

Ok, I merged all this, and hopefully fixed Kevin's issue as well. And I pushed to pypi (after messing up with my git workflow, hence the version 0.0.9b). I wanted to do all this at least a couple of days before the workshop but it didn't happen, I'm sorry. I'd be really really grateful if many people could pip install --upgrade mathlibtools and use it today in order to catch any potential regression.

[Patrick Massot]

@Kevin Buzzard could you try to update and see if you still see issues?

[Kevin Buzzard]

grr I get a segfault on Ubuntu 18.04LTS

buzzard@bob:~/crap$ pip3 install -U mathlibtools
Collecting mathlibtools
  Using cached https://files.pythonhosted.org/packages/85/27/ce65b7f36a5a387b4e6efb9b2ba42f6092bdfd77d076068114065a443787/mathlibtools-0.0.9-py3-none-any.whl
Collecting requests (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/45/1e/0c169c6a5381e241ba7404532c16a21d86ab872c9bed8bdcd4c423954103/requests-2.24.0-py2.py3-none-any.whl
Collecting gitpython>=2.1.11 (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/ef/bc/574a066bd8b61ae3c01ce5cd3eeb89aa0b1b4c0eb9fb137cd5b1cf8596be/GitPython-3.1.5-py3-none-any.whl
Collecting networkx (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/41/8f/dd6a8e85946def36e4f2c69c84219af0fa5e832b018c970e92f2ad337e45/networkx-2.4-py3-none-any.whl
Collecting toml>=0.10.0 (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/9f/e1/1b40b80f2e1663a6b9f497123c11d7d988c0919abbf3c3f2688e448c5363/toml-0.10.1-py2.py3-none-any.whl
Collecting Click (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/d2/3d/fa76db83bf75c4f8d338c2fd15c8d33fdd7ad23a9b5e57eb6c5de26b430e/click-7.1.2-py2.py3-none-any.whl
Collecting pydot (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/33/d1/b1479a770f66d962f545c2101630ce1d5592d90cb4f083d38862e93d16d2/pydot-1.4.1-py2.py3-none-any.whl
Collecting certifi (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/5e/c4/6c4fe722df5343c33226f0b4e0bb042e4dc13483228b4718baf286f86d87/certifi-2020.6.20-py2.py3-none-any.whl
Collecting PyYAML>=3.13 (from mathlibtools)
Collecting PyGithub (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/e9/47/193780145caa381e9900991c03764506bdd472a64b0a60df1562dd9ac308/PyGithub-1.51-py3-none-any.whl
Collecting paramiko>=2.7.0 (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/06/1e/1e08baaaf6c3d3df1459fd85f0e7d2d6aa916f33958f151ee1ecc9800971/paramiko-2.7.1-py2.py3-none-any.whl
Collecting tqdm (from mathlibtools)
  Using cached https://files.pythonhosted.org/packages/46/62/7663894f67ac5a41a0d8812d78d9d2a9404124051885af9d77dc526fb399/tqdm-4.47.0-py2.py3-none-any.whl
Collecting urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 (from requests->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/e1/e5/df302e8017440f111c11cc41a6b432838672f5a70aa29227bf58149dc72f/urllib3-1.25.9-py2.py3-none-any.whl
Collecting idna<3,>=2.5 (from requests->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/a2/38/928ddce2273eaa564f6f50de919327bf3a00f091b5baba8dfa9460f3a8a8/idna-2.10-py2.py3-none-any.whl
Collecting chardet<4,>=3.0.2 (from requests->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/bc/a9/01ffebfb562e4274b6487b4bb1ddec7ca55ec7510b22e4c51f14098443b8/chardet-3.0.4-py2.py3-none-any.whl
Collecting gitdb<5,>=4.0.1 (from gitpython>=2.1.11->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/48/11/d1800bca0a3bae820b84b7d813ad1eff15a48a64caea9c823fc8c1b119e8/gitdb-4.0.5-py3-none-any.whl
Collecting decorator>=4.3.0 (from networkx->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/ed/1b/72a1821152d07cf1d8b6fce298aeb06a7eb90f4d6d41acec9861e7cc6df0/decorator-4.4.2-py2.py3-none-any.whl
Collecting pyparsing>=2.1.4 (from pydot->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/8a/bb/488841f56197b13700afd5658fc279a2025a39e22449b7cf29864669b15d/pyparsing-2.4.7-py2.py3-none-any.whl
Collecting deprecated (from PyGithub->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/76/a1/05d7f62f956d77b23a640efc650f80ce24483aa2f85a09c03fb64f49e879/Deprecated-1.2.10-py2.py3-none-any.whl
Collecting pyjwt (from PyGithub->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/87/8b/6a9f14b5f781697e51259d81657e6048fd31a113229cf346880bb7545565/PyJWT-1.7.1-py2.py3-none-any.whl
Collecting cryptography>=2.5 (from paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/58/95/f1282ca55649b60afcf617e1e2ca384a2a3e7a5cf91f724cf83c8fbe76a1/cryptography-2.9.2-cp35-abi3-manylinux1_x86_64.whl
Collecting bcrypt>=3.1.3 (from paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/8b/1d/82826443777dd4a624e38a08957b975e75df859b381ae302cfd7a30783ed/bcrypt-3.1.7-cp34-abi3-manylinux1_x86_64.whl
Collecting pynacl>=1.0.1 (from paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/9d/57/2f5e6226a674b2bcb6db531e8b383079b678df5b10cdaa610d6cf20d77ba/PyNaCl-1.4.0-cp35-abi3-manylinux1_x86_64.whl
Collecting smmap<4,>=3.0.1 (from gitdb<5,>=4.0.1->gitpython>=2.1.11->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/b0/9a/4d409a6234eb940e6a78dfdfc66156e7522262f5f2fecca07dc55915952d/smmap-3.0.4-py2.py3-none-any.whl
Collecting wrapt<2,>=1.10 (from deprecated->PyGithub->mathlibtools)
Collecting cffi!=1.11.3,>=1.8 (from cryptography>=2.5->paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/f1/c7/72abda280893609e1ddfff90f8064568bd8bcb2c1770a9d5bb5edb2d1fea/cffi-1.14.0-cp36-cp36m-manylinux1_x86_64.whl
Collecting six>=1.4.1 (from cryptography>=2.5->paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/ee/ff/48bde5c0f013094d729fe4b0316ba2a24774b3ff1c52d924a8a4cb04078a/six-1.15.0-py2.py3-none-any.whl
Collecting pycparser (from cffi!=1.11.3,>=1.8->cryptography>=2.5->paramiko>=2.7.0->mathlibtools)
  Using cached https://files.pythonhosted.org/packages/ae/e7/d9c3a176ca4b02024debf82342dab36efadfc5776f9c8db077e8f6e71821/pycparser-2.20-py2.py3-none-any.whl
Installing collected packages: urllib3, idna, chardet, certifi, requests, smmap, gitdb, gitpython, decorator, networkx, toml, Click, pyparsing, pydot, PyYAML, wrapt, deprecated, pyjwt, PyGithub, pycparser, cffi, six, cryptography, bcrypt, pynacl, paramiko, tqdm, mathlibtools
Segmentation fault (core dumped)

and I'm still on 0.0.8 :-(

[Patrick Massot]

Do you have any idea what segfaults? I don't see any indication in your code block.

[Patrick Massot]

I just tried in my VM, everything works fine (using pipx upgrade mathlibtools since we switched to pipx in the install instructions).

[Patrick Massot]

And it's lunch time here.

[Scott Morrison]

Upgrades fine in my Ubuntu 20.04 VM, sorry.

[Scott Morrison]

Maybe just try again? We might get fewer messages, and so a better idea where it's hitting trouble.

[Alex J. Best]

Or try pip3 install -U urllib3 idna chardet certifi requests smmap gitdb gitpython decorator networkx toml Click pyparsing pydot PyYAML wrapt deprecated pyjwt PyGithub pycparser cffi six cryptography bcrypt pynacl paramiko tqdm on its own first

[Kevin Buzzard]

$ pip3 install -U cffi
Collecting cffi
  Using cached https://files.pythonhosted.org/packages/f1/c7/72abda280893609e1ddfff90f8064568bd8bcb2c1770a9d5bb5edb2d1fea/cffi-1.14.0-cp36-cp36m-manylinux1_x86_64.whl
Collecting pycparser (from cffi)
  Using cached https://files.pythonhosted.org/packages/ae/e7/d9c3a176ca4b02024debf82342dab36efadfc5776f9c8db077e8f6e71821/pycparser-2.20-py2.py3-none-any.whl
Installing collected packages: pycparser, cffi
Successfully installed cffi-1.14.0 pycparser-2.20
Segmentation fault (core dumped)
buzzard@bob:~/Downloads$

[Kevin Buzzard]

$ pip3 install -U cryptography
Collecting cryptography
  Using cached https://files.pythonhosted.org/packages/58/95/f1282ca55649b60afcf617e1e2ca384a2a3e7a5cf91f724cf83c8fbe76a1/cryptography-2.9.2-cp35-abi3-manylinux1_x86_64.whl
Collecting six>=1.4.1 (from cryptography)
  Using cached https://files.pythonhosted.org/packages/ee/ff/48bde5c0f013094d729fe4b0316ba2a24774b3ff1c52d924a8a4cb04078a/six-1.15.0-py2.py3-none-any.whl
Collecting cffi!=1.11.3,>=1.8 (from cryptography)
  Using cached https://files.pythonhosted.org/packages/f1/c7/72abda280893609e1ddfff90f8064568bd8bcb2c1770a9d5bb5edb2d1fea/cffi-1.14.0-cp36-cp36m-manylinux1_x86_64.whl
Collecting pycparser (from cffi!=1.11.3,>=1.8->cryptography)
  Using cached https://files.pythonhosted.org/packages/ae/e7/d9c3a176ca4b02024debf82342dab36efadfc5776f9c8db077e8f6e71821/pycparser-2.20-py2.py3-none-any.whl
Installing collected packages: six, pycparser, cffi, cryptography
Successfully installed cffi-1.14.0 cryptography-2.9.2 pycparser-2.20 six-1.15.0
Segmentation fault (core dumped)
buzzard@bob:~/Downloads$

[Rob Lewis]

https://stackoverflow.com/questions/26494324/python-pip-segfault-when-installing-package ?

[Rob Lewis]

That's python2, dunno if it's relevant. (edit - the answer is from 2019 so could be python3)

[Kevin Buzzard]

It's got me over the line. Thanks. I've got leanproject 0.0.9 installed :D

[Patrick Massot]

Could you share any insight about how you solved the issue?

[Kevin Buzzard]

I upgraded pip3

[Kevin Buzzard]

I tried the problematic mathlibtools issue I reported, and it now works fine

[Kevin Buzzard]

I can't guarantee that the issue won't show up again though

[Kevin Buzzard]

I'm not sure when finset.lean is being deleted and replaced by finset/basic.lean but if there's a point when they're both there then import data.finset will fail

[Kevin Buzzard]

Let's not worry about it now though, we have lftcm to worry about and you might well have fixed it. Thanks!

[Patrick Massot]

Oh nice, "I upgraded pip3" is a very reproducible fix.

[Bryan Gin-ge Chen]

@Patrick Massot The edits to the post-checkout hook that @Scott Morrison made in mathlib-tools#71 aren't included in 0.0.9 for some reason. You can confirm this by downloading and untarring mathlibtools-0.0.9.tar.gz on pypi, and noticing that the post-checkout script there doesn't match the one currently in the mathlib-tools repo.