add vs dev for local path

[fonsp]

Hello!

When adding a package from a local path, you can either add or dev the package. They seem to have similar effect, but dev is able to pick up changes to the package made later. Would it not make more sense to always dev when the source is a local path? i.e. that the command add ~/Hello.jl would act like dev ~/Hello.jl.

Related: I was looking into [sources]. When instantiating a Project.toml with a path specified in [sources], the package will currently get deved, not added. Is this intentional? (I like it!)

Thanks!

[KristofferC]

add URL works the same as add path in that it will give you a reproducible state (a git-tree-sha1 entry in the manifest).

My idea with keeping this separate is that if you only use add you always have a reproducible manifest (as long as you have access to the repos) while with dev you are tracking something mutable. But I have thought about if add path should have worked like dev as well many times...

When instantiating a Project.toml with a path specified in [sources], the package will currently get deved, not added. Is this intentional? (I like it!)

Yes, do get the add path behavior you would (slightly awkwardly) use a url = entry to the local path.

[fonsp]

Aha, thanks for clarifying!

if you only use add you you always have a reproducible manifest

Reproducible as in, you could reconstruct it by hand, right? By cloning the repos and searching for the right commit?