difficult installation

[hmijail]

When I opened the project in VSCode or tried running lean update I kept getting errors. I suspect that the "batteries" package got installed automatically (?) but was out of sync with the lean installation (which AFAIK was the "stable" one), and was at an impasse.

I had to copy .lake/packages/batteries/lean-toolchain to lean-toolchain, which unstuck both VSCode and the lake commands in the README.

Note that the batteries README says

Don't run lake update again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.

So sounds like maybe one should pin the "batteries"' and compiler's versions down, and not run lake update anymore?