cannot upgrade from 4.3.0-rc1

Stream: general

[Filippo A. E. Nuccio]

So I have a project that I have not been opening for a couple of months based on 4.3.0-rc1. If I try to update it (from VSCode) I get the

c:\Users\nf51454h\Desktop\Lean\lean4\fae_mathlib> lake update mathlib
error: .\lake-packages\mathlib\lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: .\lake-packages\mathlib\lakefile.lean: package configuration has errors

error, which I cannot really understand. Is there any way I can try to move forward?

[Ruben Van de Velde]

I'm sure I've seen that error discussed here on zulip

[Filippo A. E. Nuccio]

Me too, but the Zulip search I tried did not bring me far...

[Ruben Van de Velde]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20add.20Mathlib

[Filippo A. E. Nuccio]

I tried that, but did not get far. Once I update the toolchain everything restarts but the error is still there.

[Filippo A. E. Nuccio]

I still have an out-of-date manifest (and obviously so, I have just changed the toolchain)

[Filippo A. E. Nuccio]

But once I try to update I get the non very informative

Cannot update dependency. Command error output: error: fae_mathlib: could not rename packages directory (.\lake-packages -> .\.lake\packages): no error (error code: 0)

[Filippo A. E. Nuccio]

I used to think that no error was a good news, but it does not seem so.

[Ruben Van de Velde]

Maybe remove .lake

[Filippo A. E. Nuccio]

You mean, delete the directory?

[Ruben Van de Velde]

Yeah

[Enrico Borba]

Also make sure to change your lean-toolchain file to the one used by the mathlib version you are upgrading to

[Filippo A. E. Nuccio]

Ruben Van de Velde said:

Yeah

Thanks! It worked.