Latest Lean Stable on Reservoir

Stream: general

[Utensil Song]

Is this expected? I assume that an rc releases are not stable.

image.png

[Sebastian Ullrich]

I set the release to pre-release now, ideally we should automate that /cc @Kim Morrison

[Utensil Song]

Another unrelated observation:

image.png

This is due to

image.png

@Mac Malone Is there a better mechanism to determine the package name? Names like these make me worry about more serious package naming confliction issues than other package registries.

[Utensil Song]

I have also seen names like examples, render, workshop, Game where the repo is more seriously named but the package is named very casually.

image.png

[Utensil Song]

And a third unrelated observation is that https://github.com/leanprover-community/repl is not on Reservoir , which is a surprise.

[Jon Eugster]

Utensil Song said:

Is there a better mechanism to determine the package name? Names like these make me worry about more serious package naming confliction issues than other package registries.

I asked this recently here reservoir#34 and I guess something I figured from the answer is that all these marked entries should eventually vanish from reservoir in a future update of reservoir as they aren't really providing packages one can import.

Regarding repl, I think it misses a License file and therefore cannot be included.

[Utensil Song]

In that case, maybe in future there would be a linter for package naming so we would not be seeing this scene on the front page of reservor.

Scoped naming maybe a good approach, as npm is also using it.

[Mac Malone]

@Utensil Song package names are scoped by owner, so Reservoir conflicts can only occur within one. A linter seems like a good diea, but creating good heuristic is hard. Things like lib and examples are easy to mark, render less so.

It is also worth noting that these names would also make the package difficult to require as downstreams users can only require one package with each distinct name.

[Utensil Song]

Yes, I actually mean being able to require packages in a scoped way to avoid name confliction.

[Jens Petersen]

Back to the original topic...
(actually, how about a reservoir or package channel?)
What is the significance of the stable version listed on Reservoir - is it just informational? Perhaps it is updated periodically?
Just asking since I noticed it took some days for it to change to 4.11.

[Mac Malone]

Yes, it is informational and updated periodically. The periodic update was not always reliable, but Reservoir has had a major update and should be more consistent in the future.