Error in `lake update`

Stream: general

[Riccardo Brasca]

I wanted to bump mathlib in the flt-regular project but I get the error

lake update

mathlib: updating repository './.lake/packages/mathlib' to revision '4e159e0ef38e6e7894342429440ec9b4f5011bfd'
std: updating repository './.lake/packages/std' to revision '3025cb124492b423070f20cf0a70636f757d117f'
aesop: updating repository './.lake/packages/aesop' to revision '0a21a48c286c4a4703c0be6ad2045f601f31b1d0'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'fe1eff53bd0838c657aa6126fe4dd75ad9939d9a'
Cli: updating repository './.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
importGraph: updating repository './.lake/packages/importGraph' to revision '188eb34fcf1125e89d651ad462d02598219718ca'
warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
error: ./.lake/packages/proofwidgets/lakefile.lean:35:4: error: function expected at
  FetchM
term has type
  ?m.2162
error: ./.lake/packages/proofwidgets/lakefile.lean:70:4: error: function expected at
  FetchM
term has type
  ?m.2226
warning: ./.lake/packages/proofwidgets/lakefile.lean:82:7: warning: declaration uses 'sorry'
warning: ./.lake/packages/proofwidgets/lakefile.lean:85:7: warning: declaration uses 'sorry'
error: ./.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

It seems it's because of my installation (@Chris Birkbeck has the same error).

What is going wrong?

[Patrick Massot]

Very probably this is a toolchain mismatch.

[Patrick Massot]

I would copy the mathlib lean-toolchain file into the project.

[Rida Hamadani]

I had this same error today in a brand new project.

[Rida Hamadani]

I noticed that the date in https://leanprover-community.github.io/install/project.html has been changed, I was using the old commands (by pressing the up arrow in my terminal). Using the new date has fixed my issue.