feat: lake update from unsupported manifest versions

[tydeu]

If the current manifest is from unsupported (or has errors), a bare lake update will now discard it and create a new one from scratch rather than erroring and requiring you to manually delete the manifest. Lake will produce warnings noting it is ignoring such invalid manifests.

[tydeu]

One design consideration here is whether this should be done on all lake update invocations, including ones asking to only update a single package (e.g., lake update std) or if this behavior should only occur on a bare lake update. This PR currently does the former.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-3149 has successfully built against this PR. (2024-01-08 18:54:15) View Log
• ✅ Mathlib branch lean-pr-testing-3149 has successfully built against this PR. (2024-01-08 19:29:00) View Log
• 🟡 Mathlib branch lean-pr-testing-3149 build against this PR was cancelled. (2024-01-10 03:37:24) View Log
• ✅ Mathlib branch lean-pr-testing-3149 has successfully built against this PR. (2024-01-10 04:40:05) View Log

[kim-em]

I think I'd personally prefer the more conservative behaviour (only start over on a bare lake update), as usually when I'm running lake update X I really want to be careful to not update the other dependencies, so it isn't helpful if this happens anyway because there was a merge conflict I missed that has borked the manifest.

But I don't think it's critical, this is a rare enough corner case.

[tydeu]

@semorrison Thanks for the input! I was really unsure myself, so I really appreciate it. I think you are right. The current behavior defaults an invalid manifest lake update foo to essentially a bare lake update, which is generally never the goal when running lake update foo.