v4.6.0 / v4.6.1 tagging

Stream: general

[Somo S.]

@Scott Morrison said:

there is a v4.6.0 tag in each repository if you would like to pin to a commit using this toolchain.

Is it possible for each of the maintainers of each of the dependent repositories to similarly add a v4.6.1 commit/tag to distinguish a snapshot of their project that depends on what is now the latest (known) stable version of lean (i.e. v4.6.1) from the one that is dependent on a release candidate (v4.7.0-rc1) ... is this perhaps unnecessary?

[Kim Morrison]

Technically no such snapshots exist for Std/Aesop/Mathlib, as the downstream repositories were never on v4.6.1. However, since in this case v4.6.1 is functionally identical to v4.6.0, I can just duplicate the v4.6.0 tags as v4.6.1 tags. No guarantees this will happen in future, however!

[Eric Wieser]

Scott Morrison said:

I can just duplicate the v4.6.0 tags as v4.6.1 tags.

this sounds pretty confusing, since the v4.6.1 tag of mathlib will point to a version using a lean-toolchain of 4.6.0

[Notification Bot]

3 messages were moved here from #announce > v4.6.0 by Scott Morrison.

[Kim Morrison]

Indeed.

Okay, in that case someone should make a branch of Mathlib from the v4.6.0 tag, change the toolchain, and push that tag. I think anyone with write access can do this.

[Kim Morrison]

I've push v4.6.1 tags for Std/Aesop/Mathlib

[Kim Morrison]

If someone could verify they work that would be great.

[Siddhartha Gadgil]

I tried this and it seems that the cache has not been built. I updated lean-toolchain to leanprover/lean4:v4.6.1 and my lakefile has a single direct dependency: require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"v4.6.1

I tried also deleting .lake/package, lake-manifest.json and running lake update. The cache was still not found.

[Peiran Wu]

I tried to bump the Lean toolchain to v4.6.1 without changing the Mathlib4 tag and noticed that running lake update seemed to be overwriting the lean-toolchain file back to v4.6.0:

wpr@laptop myproject % cat lean-toolchain
leanprover/lean4:v4.6.1
wpr@laptop myproject % elan show
installed toolchains
--------------------

leanprover/lean4:v4.6.0
leanprover/lean4:v4.6.1 (default)

active toolchain
----------------

leanprover/lean4:v4.6.1 (overridden by '/Users/wpr/Code/lean/tate/lean-toolchain')
Lean (version 4.6.1, aarch64-apple-darwin, commit dac66e47e32f, Release)

wpr@laptop myproject % lake update
warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'
mathlib: running post-update hooks
No files to download
Decompressing 4333 file(s)
unpacked in 143 ms
wpr@laptop myproject % cat lean-toolchain
leanprover/lean4:v4.6.0
wpr@laptop myproject % elan show
installed toolchains
--------------------

leanprover/lean4:v4.6.0
leanprover/lean4:v4.6.1 (default)

active toolchain
----------------

leanprover/lean4:v4.6.0 (overridden by '/Users/wpr/Code/lean/tate/lean-toolchain')
Lean (version 4.6.0, aarch64-apple-darwin, commit a5bc9013ab13, Release)

[Ruben Van de Velde]

Yeah, running lake update will copy mathlib's lean version

[Kim Morrison]

i.e. in your lakefile.lean you need to make sure the "require" line for Mathlib is obtaining a branch/tag/commit that is on the toolchain you intended to use. In this case I think

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.6.1."

[Siddhartha Gadgil]

Just to confirm, I did use the tagging as above and the cache does not work.

[Kim Morrison]

@Siddhartha Gadgil perhaps you could create a minimal repo showing this problem?

[Siddhartha Gadgil]

I will try. Have to be away but will do this in 2 hours.

[Siddhartha Gadgil]

@Scott Morrison A nearly empty repo showing this is at https://github.com/siddhartha-gadgil/Leantegration.git

[Kim Morrison]

@Siddhartha Gadgil, ah, I suspect that merely pushing a tag does not create oleans. I've pushed a branch made from the v4.6.1 tag. Let's see if things work better after https://github.com/leanprover-community/mathlib4/actions/runs/8183028836/job/22375278960

[Kim Morrison]

@Siddhartha Gadgil , that seems to have fixed things, can you confirm?

[Siddhartha Gadgil]

Scott Morrison said:

Siddhartha Gadgil , that seems to have fixed things, can you confirm?

Yes, the caching is fine. Thanks.

[Mario Carneiro]

@Scott Morrison said:

i.e. in your lakefile.lean you need to make sure the "require" line for Mathlib is obtaining a branch/tag/commit that is on the toolchain you intended to use. In this case I think

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.6.1."

I guess the . at the end of the tag is a typo

[Siddhartha Gadgil]

It looks like the same issue, cache not being built, has surfaced if I use "v4.8.0-rc1" in the lean-toolchain as well as the corresponding Mathlib cache.

[Mauricio Collares]

That's being discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/cache.20not.20working.20after.20bump.20to.20.20v4.2E8.2E0-rc1v.3F