Error when updating mathlib

Stream: general

[Wrenna Robson]

When I run lake update mathlib, I am suddenly getting this error:

info: mathlib: updating repository '././.lake/packages/mathlib' to revision '95197cb84e872a92da03d95c232e86b238eccdbb'
error: ././.lake/packages/mathlib/lakefile.lean:21:47: error: unknown identifier 'git'
error: ././.lake/packages/mathlib/lakefile.lean:21:51: error: unexpected token; expected command
error: ././.lake/packages/mathlib/lakefile.lean:22:40: error: unknown identifier 'git'
error: ././.lake/packages/mathlib/lakefile.lean:22:44: error: unexpected token; expected command
error: ././.lake/packages/mathlib/lakefile.lean:23:43: error: unknown identifier 'git'
error: ././.lake/packages/mathlib/lakefile.lean:23:47: error: unexpected token; expected command
error: ././.lake/packages/mathlib/lakefile.lean:24:50: error: unknown identifier 'git'
error: ././.lake/packages/mathlib/lakefile.lean:24:54: error: unexpected token; expected command
error: ././.lake/packages/mathlib/lakefile.lean:25:49: error: unknown identifier 'git'
error: ././.lake/packages/mathlib/lakefile.lean:25:53: error: unexpected token; expected command
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has error

My efforts to diagonose/fix this have not worked and I do not understand the issue.

[Wrenna Robson]

(I am also suddenly having some very odd performance issues with instance definitions where the last proof in the instance takes a long time to resolve, even if every proof is e.g. set to sorry.

[Wrenna Robson]

That one seemed to briefly fix itself after restarting my computer but then it returned - no idea what is going on there.

[Eric Wieser]

Have you tried updating to intermediate lean versions?

[Eric Wieser]

That is, change "master" in your lakefile to v4.9.0 or some other version between where you are and what you're updating to

[Eric Wieser]

You might need to lake clean or rm -rf .lake to recover from the state you're currently in first.

[Pietro Monticone]

This should work

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

[Pietro Monticone]

Is this the repository you're working on? If so, I have just tested it and it seems to work fine.

[Wrenna Robson]

It is, aye. I think it's a local machine issue.

[Wrenna Robson]

Thanks - this seems to be working...

[Yaël Dillies]

Yeah, the trick is always to update the toolchain manually before running lake update