Topic: donating olean files
Kevin Buzzard (Aug 22 2019 at 08:08):
I'm working on a branch of mathlib with a student. I just merged master into our branch, fixed up some conflicts, and compiled. I hence have a bunch of working olean files. Can I somehow pass these to the student with
cache-olean? Another approach which will probably work is to stop git ignoring olean files and then just push all the olean files onto the branch, but this seems like an inappropriate use of github.
Patrick Massot (Aug 22 2019 at 09:06):
You should be able to git commit (to your branch) and then run
cache-olean. Then you can checkout another branch, mess up everything, checkout back your student branch, run
cache-olean --fetch and get back your oleans. This is exactly what
cache-olean is meant to do.
Patrick Massot (Aug 22 2019 at 09:08):
cache-olean you can check the
_cache folder to see the archive that was created, named after the commit hash.
Rob Lewis (Aug 22 2019 at 09:14):
I guess it should work for you to send the right archive to your student and have them put it in their
_cache folder. But I've never tried.
Kevin Buzzard (Aug 22 2019 at 09:16):
If I'm sending tarballs to a student I may as well just tar up the olean files directly.
Simon Hudon (Aug 22 2019 at 14:14):
If you have DropBox, you could make
_cache a symbolic link to a drop box directory and sync it that way
Simon Hudon (Aug 22 2019 at 15:34):
Last winter, I was working on an extension to
sccache that would have allowed sharing compilation caches. Maybe I should get back to it
Kevin Buzzard (Aug 22 2019 at 16:13):
The symbolic link idea is nice. I'm assuming that this sort of thing is possible in Win10? I don't know the equivalent of
ln -s. It's just a bore for a student to have to compile stuff after I've pushed to a branch and compiled myself. Thanks!
Simon Hudon (Aug 22 2019 at 16:19):
Last updated: May 10 2021 at 19:16 UTC