Importing a repository in `lakefile.toml`

Stream: lean4

[Frédéric Dupuis]

I tried to create a new lean repo that depends on Batteries by adding the following snippet to lakefile.toml, as recommended on the Batteries reservoir page:

[[require]]
name = "batteries"
scope = "leanprover-community"
version = "main"

The result, when trying either lake update or lake build:

error: batteries unsupported dependency version format 'main' (should be "git#>rev>")

I just switched to lakefile.lean instead of investigating this, but I figured I should flag this bug here for the record.

[Julian Berman]

I think the bug is in the README, it should be rev = "main" not version for a git reservoir dep.

[Julian Berman]

https://github.com/leanprover-community/batteries/pull/1067