lake failure to bump mathlib

Stream: FLT

[Kevin Buzzard]

buzzard@buster:~/lean-projects/FLT$ lake update -R -Kenv=dev mathlib
info: doc-gen4: updating repository '././.lake/packages/doc-gen4' to revision 'c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53'
error: ././.lake/packages/mathlib/lakefile.lean:86:2: error: unknown attribute [test_driver]
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors
buzzard@buster:~/lean-projects/FLT$ lake update -R -Kenv=dev
info: doc-gen4: updating repository '././.lake/packages/doc-gen4' to revision '1f51169609a3a7c448558c3d3eb353fb355c7025'
error: ././.lake/packages/mathlib/lakefile.lean:86:2: error: unknown attribute [test_driver]
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors
buzzard@buster:~/lean-projects/FLT$

Can someone remind me how I'm supposed to do this? That command worked last time according to my notes. I'm sorry I have to keep asking, I have no understanding of lakefiles, I'm just hoping the system becomes stable and I can type the same thing week in week out.

[Kevin Buzzard]

Same error if I try using VS Code upside-down A point and click solution.

[Ruben Van de Velde]

Copy the lean toolchain file from mathlib - unfortunately lake update doesn't always work across lean version changes, because you also need to update lake itself

[Kevin Buzzard]

I hadn't internalised that I also had to do this for projects which depended on mathlib (other people have been bumping mathlib for me, i.e. you!)

[Yaël Dillies]

This is the script I use, for reference:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -R -Kenv=dev update

[Ruben Van de Velde]

(that is, it doesn't always work - lake update tries to do this on its own)

[Kevin Buzzard]

Not lake -R -Kenv=dev update mathlib?

[Ruben Van de Velde]

Either