Zulip Chat Archive

Stream: general

Topic: leanproject hooks


view this post on Zulip Scott Morrison (Jul 10 2020 at 06:14):

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

view this post on Zulip Scott Morrison (Jul 10 2020 at 06:15):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 10 2020 at 06:16):

I've noticed that too!

view this post on Zulip Patrick Massot (Jul 10 2020 at 08:14):

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

view this post on Zulip Scott Morrison (Jul 10 2020 at 11:05):

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.

view this post on Zulip Scott Morrison (Jul 10 2020 at 11:06):

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.

view this post on Zulip Scott Morrison (Jul 10 2020 at 11:06):

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

view this post on Zulip Oliver Nash (Jul 10 2020 at 13:07):

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?

view this post on Zulip Scott Morrison (Jul 11 2020 at 01:24):

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.

view this post on Zulip Bhavik Mehta (Jul 11 2020 at 01:54):

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

view this post on Zulip Patrick Stevens (Jul 11 2020 at 06:36):

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

view this post on Zulip Patrick Stevens (Jul 11 2020 at 06:36):

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

view this post on Zulip Patrick Stevens (Jul 11 2020 at 06:36):

Carry on :P

view this post on Zulip Scott Morrison (Jul 11 2020 at 09:00):

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

view this post on Zulip Scott Morrison (Jul 11 2020 at 09:02):

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.

view this post on Zulip Scott Morrison (Jul 11 2020 at 09:02):

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

view this post on Zulip Kenny Lau (Jul 11 2020 at 09:02):

or commit before checkout

view this post on Zulip Scott Morrison (Jul 11 2020 at 09:04):

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.

view this post on Zulip Scott Morrison (Jul 11 2020 at 09:04):

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 09:26):

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.

view this post on Zulip Patrick Massot (Jul 11 2020 at 09:29):

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.

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 10:38):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 10:43):

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 12:07):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:56):

What works?

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:56):

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 12:56):

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 12:57):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:57):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:58):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:58):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:58):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 12:59):

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

view this post on Zulip Johan Commelin (Jul 11 2020 at 12:59):

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

view this post on Zulip Patrick Stevens (Jul 11 2020 at 13:02):

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:08):

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

view this post on Zulip Patrick Massot (Jul 11 2020 at 13:09):

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.

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 13:17):

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

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 13:44):

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

view this post on Zulip Scott Morrison (Jul 12 2020 at 05:32):

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

view this post on Zulip Patrick Massot (Jul 12 2020 at 10:58):

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.

view this post on Zulip Patrick Massot (Jul 12 2020 at 11:00):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 11:08):

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 :-(

view this post on Zulip Patrick Massot (Jul 12 2020 at 11:25):

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

view this post on Zulip Patrick Massot (Jul 12 2020 at 11:28):

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

view this post on Zulip Patrick Massot (Jul 12 2020 at 11:29):

And it's lunch time here.

view this post on Zulip Scott Morrison (Jul 12 2020 at 12:13):

Upgrades fine in my Ubuntu 20.04 VM, sorry.

view this post on Zulip Scott Morrison (Jul 12 2020 at 12:13):

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

view this post on Zulip Alex J. Best (Jul 12 2020 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 20:54):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 20:55):

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

view this post on Zulip Rob Lewis (Jul 12 2020 at 20:56):

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

view this post on Zulip Rob Lewis (Jul 12 2020 at 20:57):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 20:59):

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

view this post on Zulip Patrick Massot (Jul 12 2020 at 21:02):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 21:02):

I upgraded pip3

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 21:03):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 21:04):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 21:05):

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 21:05):

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

view this post on Zulip Patrick Massot (Jul 12 2020 at 21:08):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 07:26):

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


Last updated: May 15 2021 at 22:14 UTC