Package version from git tag?

Stream: lean4

[Miles Sabin]

It seems that the package command only supports pure values ... is there any mechanism for deriving a package version from git info in a lakefile.lean?

The motivation is to have a package release process which is driven by tagging in git. Something similar is possible in Haskell with a cabal Setup.hs using a confHook.

[Kim Morrison]

I think this is a question for @Mac Malone.

[Mac Malone]

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

[Miles Sabin]

@Mac Malone very belated thanks ... that works perfectly.