Zulip Chat Archive

Stream: general

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

After running 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: Dec 20 2023 at 11:08 UTC