lean4
lean4 copied to clipboard
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.