Need help fixing dependency

Stream: new members

[Kevin Cheung]

I issued "update project dependencies" in VSCode and it ended in error (see below). I am on macOS. Is there a way to fix this?

> lean --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)
> lake --version
Lake version 5.0.0-b614ff1 (Lean version 4.5.0-rc1)
> lake update mathlib
error: ./.lake/packages/mathlib/lakefile.lean:10:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:11:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:12:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:13:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:14:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:15:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:16:7: error: unexpected token; expected identifier
error: ./.lake/packages/mathlib/lakefile.lean:52:2: error: 'testDriver' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors
mathlib: updating repository './.lake/packages/mathlib' to revision 'bb0575e329e059f7ec31c43337a2094282f6be3c'
=> Operation failed. Exit code: 1.
info: mathlib: updating repository './.lake/packages/mathlib' to revision '9c832bc4b73e31853dbfe8351424d2829b881b2c'

[Kevin Buzzard]

Try this https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#from-the-command-line

[Kevin Cheung]

I tried it and now I have the following error:

info: downloading component 'lean'
Total: 245.7 MiB Speed: 733.2 KiB/s
info: installing component 'lean'
error: toolchain 'leanprover/lean4:v4.15.0-rc1' does not have the binary `/Users/kcheung/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/bin/lake`

[Kevin Cheung]

Doing an elan update seems to have solved the problem.

[Kevin Cheung]

Actually, it didn't.