adele refactor

Stream: FLT

[Kevin Buzzard]

I am proposing refactoring finite adeles in #23542 and this will probably break a lot of things, but I think it's for the best (because the route to local compactness will be easier). But I don't know how to start working on the FLT refactor based on this branch. I tried editing lake-manifest.json naively to the commit corresponding to the head of the branch but now lake exe cache get is unsurprisingly telling me

info: mathlib: checking out revision 'fcffe6d9c63287fd43720321f74855dd8901f353'
Dependency Mathlib uses a different lean-toolchain
  Project uses leanprover/lean4:v4.18.0
  Mathlib uses leanprover/lean4:v4.18.0-rc1

Is there a simple way to do this? FLT is close to up-to-date with mathlib and I can happily merge master in #23542 if necessary.

[Yaël Dillies]

Oh, that sounds like someone pinned your toolchain

[Yaël Dillies]

Ah no, sorry, you edited the lakefile manually. Don't do that :smile:

[Yaël Dillies]

Instead add the mathlib commit in your lakefile just after this line. I believe it should look like

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "fcffe6d9c63287fd43720321f74855dd8901f353"

or maybe

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "kbuzzard-finite-adele-ring-refactor"

will work too