Stream: maths

Topic: cache-olean

Kevin Buzzard (Feb 12 2020 at 21:56):

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 (Feb 12 2020 at 21:57):

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

Gabriel Ebner (Feb 12 2020 at 22:00):

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 (Feb 12 2020 at 22:02):

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.

Last updated: May 09 2021 at 10:11 UTC