v4.13.0-rc1

Stream: batteries

[Kim Morrison]

Just a heads up that after I merge batteries#978 into bump/v4.13.0, Batteries will be ready to move to v4.13.0-rc1 (being released now), and I will make a PR merging bump/v4.13.0 into main.

[François G. Dorais]

We're now on v4.13.0-rc3 (batteries#981) which is actually exactly the same as v4.13.0-rc1. (v4.13.0-rc2 was a brief blip in between.)

[Matthew Fairtlough]

as a novice, I'm still on v4.12.0 and lake is pulling in the latest version to work with v4.13.0 and stuff breaks badly. A pointer to how to specify the last version that worked with 4.12.0 and include that in my lakefile.lean/manifest/whatever else is needed, would be much appreciated! Can I use lake update to specify what not to change perhaps?

[Daniil Kisel]

batteries repository has tags for different toolchain versions.

In lakefile.lean when requiring from git you can specify branch, commit or tag:
require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"

Similarly for lakefile.toml:

[[require]]
name = "batteries"
git = "https://github.com/leanprover-community/batteries"
rev = "v4.12.0"

[Matthew Fairtlough]

thanks so much. I've done this, but now need to update the manifest, which I did by lake update batteries and now I have Lake version 5.0.0-01d414a (Lean version 4.13.0-rc3) which is the version that exactly won't work with the version I need. How do I stop lake update <anything> from also updating my lean-toolchain? My workaround is to revert lean-toolchain but surely there's a better way?

[Ruben Van de Velde]

As far as I'm aware, lake update only changes your lean-toolchain if you depend on mathlib

[Shreyas Srinivas]

(deleted)

[Matthew Fairtlough]

oh right. But I do depend on mathlib. But requiring a specific version eg 4.12.0 means it doesn't self-update the toolchain, which is great.

[Eric Wieser]

If you depend on mathlib, then you should not put batteries in your lakefile

[Ruben Van de Velde]

Oh, that's a good point as well