Batteries releases and Batteries template for lake

Stream: batteries

[Shreyas Srinivas]

I started a batteries only project and had a lot of build errors. Then I pinned the toolchain to v4.13.0-rc3 and found out that there was no rc3 for batteries

[Shreyas Srinivas]

How do I get batteries to build and (RFC) could we have a project template for batteries with nice defaults?

[Shreyas Srinivas]

Currently I am falling back to 4.12.0

[Ruben Van de Velde]

Batteries' main branch is on rc3, so you can use that

[Shreyas Srinivas]

That was my first attempt. It failed

[Shreyas Srinivas]

Got masses of build errors

[Ruben Van de Velde]

How?

[Ruben Van de Velde]

With what in your lean-toolchain?

[Shreyas Srinivas]

leanprover/lean4:v4.13.0-rc3

[Ruben Van de Velde]

And what commit of batteries?

[Shreyas Srinivas]

The lakefile.toml was:

name = "<redacted>"
defaultTargets = ["<redacted>"]

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

[[lean_lib]]
name = "<redacted>"

[[lean_exe]]
name = "<redacted>"
root = "Main"

[Shreyas Srinivas]

except those <redacted> bits of course

[Shreyas Srinivas]

Update : got it working by clearing out lake-manifest and ./.lake and re-running everything again

[Shreyas Srinivas]

But it seems I can't pin Batteries to 4.13.0-rc3 because there is no tag

[Ruben Van de Velde]

Probably just forgotten, cc @Kim Morrison

[Ruben Van de Velde]

You can use a commit hash like daf1ed9 instead of main in your lakefile.toml

[Shreyas Srinivas]

Sounds good. In the long run, it would be nice if we could lake add Batteries and get the correct revision automatically added

[Eric Wieser]

Ruben Van de Velde said:

You can use a commit hash like daf1ed9 instead of main in your lakefile.toml

Isn't this what lake-manifest.json is for?

[Mario Carneiro]

lake-manifest.json is for saying what the current version of the project is building with, the rev = in lakefile.toml is for saying what you want to happen when you next run lake update.

[Mario Carneiro]

using a hash or tag there is opting out of automatic updates

[Kim Morrison]

I've now pushed a v4.13.0-rc3 tag. (François did the bump while I was on holiday.)