lakefileの中でgitタグを取得できる

[Seasawher]

You can run arbitrary IO in a lakefile.lean via the run_io syntax. For example, you could derive the version of a package from a Git tag like so:

def getVersion : IO StdVer := do
  let repo := GitRepo.mk __dir__
  let some tag ← repo.findTag?
    | return v!"0.0.0"
  let .ok ver := StdVer.parse tag
    | return v!"0.0.0"
  return ver

package mypkg where
  version := run_io getVersion

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Package.20version.20from.20git.20tag.3F/near/566460301