lean4
lean4 copied to clipboard
leanprover
refactor: lake: manifest semver & code cleanup
Switches the manifest format to use major.minor.patch semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after 0.x) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifest with numeric versions. It will treat the numeric version N as semantic version 0.N.0. Lake will also accept manifest versions with - suffixes (e.g., x.y.z-foo) and then ignore the suffix.
This change also includes the general cleanup/refactoring of the manifest code and data structures that was part of #3174.
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-06 23:29:54) View Log
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-07 00:12:29) View Log
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-07 04:03:40) View Log
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-07 19:07:35) View Log
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-07 21:18:38) View Log
- ✅ Mathlib branch lean-pr-testing-4083 has successfully built against this PR. (2024-05-07 22:56:23) View Log
Just a minor comment about PR labelling: I think you might be overusing the "draft" status, or at least I don't think anything should ever be both a draft and will-merge-soon, which have opposite implications for reviewing urgency!
I don't think anything should ever be both a draft and will-merge-soon,
@semorrison Definitely! That was just me forgetting to mark it ready for review. 🤦♂️