donating olean files

Stream: general

[Kevin Buzzard]

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]

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]

After running cache-olean you can check the _cache folder to see the archive that was created, named after the commit hash.

[Rob Lewis]

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]

If I'm sending tarballs to a student I may as well just tar up the olean files directly.

[Simon Hudon]

If you have DropBox, you could make _cache a symbolic link to a drop box directory and sync it that way

[Simon Hudon]

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]

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]

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