Question about Lean versions

Stream: new members

[Ching-Tsun Chou]

Today I saw that Lean versions v4.17.0 and v4.18.0-rc1 were released. In general, what is relationship between versions r<N> and r<N+1>-rc1?

[Marc Huisinga]

v4.17.0 is the current stable release, whereas v4.18.0-rc1 is the current release candidate for the next stable release (v4.18.0).

[Ching-Tsun Chou]

In one of my Lean projects, I updated the lean-toolchain to point to lean4:v4.17.0. But after I ran "lake update", I found that lean-toolchain now points to lean4:v4.18.0-rc1. Why did that happen?

[Henrik Böving]

Ching-Tsun Chou said:

In one of my Lean projects, I updated the lean-toolchain to point to lean4:v4.17.0. But after I ran "lake update", I found that lean-toolchain now points to lean4:v4.18.0-rc1. Why did that happen?

Does your project depend on some library?

[Ching-Tsun Chou]

It depends on mathlib and perhaps others. I simply followed the instructions in the section "Creating a Lean project" of the following webpage to set it up:

https://leanprover-community.github.io/install/project.html

You can see the project here:

https://github.com/ctchou/my_lean

[Eric Wieser]

The trick is to change your mathlib version, not the toolchain version

[Eric Wieser]

See #general > v4.17.0

[Ching-Tsun Chou]

I was just following instructions given in https://leanprover-community.github.io/install/project.html. Perhaps that page should be updated?

[Eric Wieser]

That gives instructions for updating to the latest version, not a particular version

[Eric Wieser]

I guess it would be good to explain both

[Ching-Tsun Chou]

Apparently there are always a "latest stable" and a "latest release candidate". Both should be explained.

Also, I don't see a lakefile.toml. I have only a lakefile.lean from setting up the project by following the instructions.