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