bumping mathlib

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

How does one bump mathlib on a project such as this? I tried randomly editing the json but always failed to get working oleans. I wanted to switch to a random mathlib commit corresponding to a PR, and for which there were oleans on azure, and it just be painless.

[Jon Eugster]

what I would do is changing the lakefile to require mathlib from git "https...yadayada" @ "commit-hash" and then call

lake update
lake exe cache get

but even just these two commands should work if you just want newest master, dont they?

The thing I dont know is if adams find_with_gpt works with a new lean version, I think it caused some problems for me a few days ago.

[Kevin Buzzard]

Thanks!

[Jon Eugster]

I think the problem about editing the json manually is that you'd need all the correct hashes for mathlibs dependencies Std etc. too. otherwise the cache is not applied

[Adam Topaz]

Do you have some reason not to update to master for mathlib? If not, just do the two commands above, no need to edit the lakefile

[Adam Topaz]

You may have to copy over the toolchain file as well

[Kevin Buzzard]

I was just interested in the procedure. I wanted to include the PR I wrote yesterday