mathlibtools fails to find local olean cache

Stream: general

[Markus Himmel]

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.

[Patrick Massot]

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.

[Patrick Massot]

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.

[Markus Himmel]

That works! :)

[Patrick Massot]

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)

[Markus Himmel]

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