Zulip Chat Archive

Stream: general

Topic: mathlibtools fails to find local olean cache


view this post on Zulip Markus Himmel (May 23 2020 at 15:07):

When I locally create a commit and switch away from the branch, the git hooks create an olean cache. However, when I switch back to that branch, then those local oleans are not found. Looking at the contents of ~/.mathlib, the cache is there, but it has the extension .tar.bz2, and I think leanproject only looks for tar.xz and tar.gz.

view this post on Zulip Patrick Massot (May 23 2020 at 15:21):

Sorry about that. I think very very few people use these git hooks (I certainly don't use them) so it's very much untested.

view this post on Zulip Patrick Massot (May 23 2020 at 15:23):

Could you try adding the obvious item to the list at https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/lib.py#L149? If this is not enough then please open a GitHub issue.

view this post on Zulip Markus Himmel (May 23 2020 at 15:27):

That works! :)

view this post on Zulip Patrick Massot (May 23 2020 at 16:19):

Is this ok for you to use your locally patched version until 0.0.8 comes out? (this is pure lazyness from me, I already did a release today)

view this post on Zulip Markus Himmel (May 23 2020 at 16:36):

Sure, take your time. By the way, thank you for all the amazing work on leanproject.


Last updated: May 15 2021 at 23:13 UTC