lake update/cache errors : Unknown manifest version

Stream: lean4

[Shreyas Srinivas]

I want to bring up two errors on current toolchains:

1. When creating a new math project and then changing lakefile.lean's mathlib dep branch to "stable", one gets this error error: ././lake-manifest.json: unknown manifest version '"1.0.0"'. Fixed it by deleting lake-manifest.json
2. In another lake new <project> math without any modification of mathlib dependency, after successfully getting cache on toolchain 4.9.0-rc2, and opening the project on vscode, as soon as I imported Mathlib.Tactic, vscode said I need to restart my file and when I did that, vscode was compiling some aesop files.

[Ruben Van de Velde]

For 2, update your mathlib to a version that is at most 15 minutes old

[Shreyas Srinivas]

Okay. I assume by lake update mathlib

[Ruben Van de Velde]

Yes

[Shreyas Srinivas]

Wait 15 minutes old?

[Ruben Van de Velde]

Yes

[Ruben Van de Velde]

You need #13835

[Shreyas Srinivas]

I think I'll downgrade to stable for now. This is a project that is meant to be shared with a lean newbie and I don't want to bother them with bugs.