lake update package

Stream: lean4

[Adam Topaz]

Is it possible to use lake to update a specific dependency? lake update updates everything. Of course, I could git pull in the correct folder and manually change the lake manifest, but this can't be the preferred workflow.

[Mac Malone]

You can specify exact commits in your lakefile require statement if you do not want the package updating. This feature is also on the TODO list as lake#148 (feel free to give it an upvote).

[Wojciech Nawrocki]

Fwiw I strongly disliked this behaviour of Lake originally but as Mac says, lakefiles should really be pointing at a specific version of a dependency rather than master. The only missing feature, I think, is a versioning scheme so we can point at a range of semver-compatible versions rather than a particular commit or git tag.

[Mario Carneiro]

well doing that would basically make lake update impossible unless it starts rewriting lean files

[Wojciech Nawrocki]

Sorry, I don't understand @Mario Carneiro .

[Mario Carneiro]

if you have require foo from git "bla" @ "1234abcd", then in order for an automated "update" action to work it would have to replace the text "1234abcd" in the lakefile with the new version

[Mario Carneiro]

I assumed that was the point of having a json manifest in the first place, since lake can rewrite it

[Mac Malone]

@Mario Carneiro Even in NPM, which has Json package configuration, npm update does not rewrite the configuration.

[Mac Malone]

(It only updates the package lockfile within the range of specified permitted versions in the configuration.)

[Wojciech Nawrocki]

Mario Carneiro said:

if you have require foo from git "bla" @ "1234abcd", then in order for an automated "update" action to work it would have to replace the text "1234abcd" in the lakefile with the new version

Yes exactly, if you have require foo from git "bla" @ "0.2.*" then lake update can rewrite lake-manifest to any new version of bla within the range 0.2.*. Also you are guaranteed no breaking changes (assuming semver correctness etc) on lake update in that case, which would be better than the current case of 'anything goes because we point at master'.

[Wojciech Nawrocki]

Then if you want to bump in a breaking way, you edit the lakefile to 0.3.* or something and manually fix your files.

[Mario Carneiro]

right, so that would suggest that the current way we are doing it is correct

[Mac Malone]

Lake also already sort of supports this, the project just needs to make 0.2.*a branch (potentially using the more standard branch name of v0.2.x).

[Wojciech Nawrocki]

It's correct insofar as there is no semver that we could use instead of the current approach, sure.

[Mario Carneiro]

with "master" in the lakefile and lake update determining the exact commit

[Mario Carneiro]

because we have no semver

[Wojciech Nawrocki]

Mac said:

Lake also already sort of supports this, the project just needs to make 0.2.*a branch (potentially using the more standard branch name of v0.2.x).

Is this anything more than a purely syntactic match against a branch name? Because with semver you can specify all kinds of constraints.

[Mario Carneiro]

and by that token you could read "master" as another way to spell vx.y.z

[Mario Carneiro]

Is this anything more than a purely syntactic match against a branch name? Because with semver you can specify all kinds of constraints.

it's just a syntactic match, but mac is pointing out that you can encode semver in branch update policies

[Mac Malone]

@Wojciech Nawrocki Yeah, it is just using the branch as a semver channel. While it is true semver supports many more constraints, ^x.y and exact versions are definitely the most common (both of which Lake can currently support via branchs, tags, and/or exact commits).

[Mac Malone]

Mario Carneiro said:

and by that token you could read "master" as another way to spell vx.y.z

The key difference is that it does not differentiated between significant breaking changes and backwards-compatible patches (which some level of semvar in the later would provide).