Cannot parse 'lake-manifest.json'

Stream: general

[Dagur Asgeirsson]

I'm trying to bump mathlib in a project using the VSCode interface, but I get the following error:

Cannot parse 'lake-manifest.json' file at /Users/cdh714/lean4-projects/LeanCondensed/lake-manifest.json to determine dependencies.

I haven't touched the lake-manifest file. Does anyone know what's going on?

[Marc Huisinga]

The manifest version format changed and I haven't updated the VS Code extension so that it is capable of parsing the new format yet. You'll have to use lake in the terminal for the time being.

[Marc Huisinga]

I'll see if I can update the VS Code extension tomorrow.

[Marc Huisinga]

0.0.160 is released now and supports the new Manifest format.