Zulip Chat Archive

Stream: general

Topic: donating olean files


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Simon Hudon (Aug 22 2019 at 16:19):

https://www.maketecheasier.com/create-symbolic-links-windows10/


Last updated: May 10 2021 at 19:16 UTC