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
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.
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.
Markus Himmel (May 23 2020 at 15:27):
That works! :)
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)
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