cache-olean

Stream: maths

[Kevin Buzzard]

I am trying to make a mathlib PR. I would like a cheap method of getting the olean files onto my system. If I use cache-olean --fetch then I have to be on the 3.4.2 branch, right? Does that still track master even though master uses 3.5.1? Did I miss instructions on how to use cache-olean now that we switched to 3.5.1?

[Rob Lewis]

You can be on the 3.5.1 branch and get the newest nightly.

[Gabriel Ebner]

You need to be on the 3.5.1 branch to get the latest nightly. The 3.4.2 nightlies haven't been updated for 8 days.

[Kevin Buzzard]

I didn't even know that the lean-3.5.1 branch existed until just now -- I didn't have it locally. I think I'm up to speed now. Thanks.