Errors upgrading Mathlib

Stream: new members

[Arien Malec]

trying to update a project with a Mathlib dependency:

% lake clean
% lake update
mathlib: updating repository './.lake/packages/mathlib' to revision '01ef982a4a351333dd04533573c4d489cd2164a3'
error: ./.lake/packages/mathlib/lakefile.lean:79:2: error: unknown attribute [test_runner]
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors

[Ruben Van de Velde]

Copy .lake/packages/mathlib/lean-toolchain over yours and try again

[Arien Malec]

So simple! No automated way to keep them in synch?

[Ruben Van de Velde]

It is automatic (when updating mathlib) - but only if the lean version you were using can interpret the lakefile.lean from the new mathlib

[Ruben Van de Velde]

That's one of the disadvantages of writing your build configuration in a full lean file