Skip to content

fix: workaround for invalid lake version in v4.21.0-rc1#618

Merged
mhuisi merged 1 commit intomasterfrom
mhuisi/invalid-lake-version
Jun 3, 2025
Merged

fix: workaround for invalid lake version in v4.21.0-rc1#618
mhuisi merged 1 commit intomasterfrom
mhuisi/invalid-lake-version

Conversation

@mhuisi
Copy link
Copy Markdown
Collaborator

@mhuisi mhuisi commented Jun 3, 2025

This PR fixes the fallout of a small ticking time bomb that exploded in v4.21.0-rc1.

Lake reports its version strings as follows, where 77cfc4d is the commit ID of the corresponding release:

[mhuisi@fedora ~]$ lake --version
Lake version 5.0.0-77cfc4d (Lean version 4.20.0)

In v4.21.0-rc1, the commit ID is 0168680, so Lake reports the following version string:

[mhuisi@fedora ~]$ lake --version
Lake version 5.0.0-0168680 (Lean version 4.21.0-rc1)

Unfortunately, 5.0.0-0168680 is not a valid semantic version, since it both contains a 0 at the start and only numbers. This is fairly rare, but it now happened on v4.21.0-rc1 for the first time.
The VS Code extension parses this version as part of its precondition checks, which now fails because the version is not a valid semantic version.

The workaround for this issue is to remove the step that parses the version. The extension only parsed it for consistency with other precondition checks and doesn't actually do anything interesting with the version, so removing it doesn't lose us anything.

@mhuisi mhuisi merged commit 59d6669 into master Jun 3, 2025
2 checks passed
@mhuisi mhuisi deleted the mhuisi/invalid-lake-version branch October 21, 2025 12:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant