Print current mathlib version (tag, build date, etc.)

Stream: Is there code for X?

[Adomas Baliuka]

Is there a way to get the version of Mathlib that is being used within the code? I was thinking of adding it to the mathlib4-tactics page but didn't find any way to do it.

Is there something analogous to Lean.versionString?

I guess one very often uses versions of Mathlib without tags and they do not have a semantic version-string at all. Maybe having access to the git-sha1, date of commit, output of a suitable call togit describe?

[Michael Rothgang]

The lakefile.lean in the that repository contains the mathlib version, right? So, could you extract that information instead?

[Kim Morrison]

I think parsing lake-manifest.json might be the most plausible approach right now.

[Adomas Baliuka]

How should one find the path of this file in the most robust way? Does it make sense to add this as a definition to Mathlib?

[Adomas Baliuka]

I could also do something like this, not sure if parsing the manifest is more robust or not...

import Lean
import Lake.Util.Git

open Lake
-- could use better way to get to the directory
def repo : GitRepo := ⟨"./.lake/packages/mathlib"⟩


/-
some "v4.11.0-rc1-389-gf904bf86ab"
-/
#eval captureProc? {
  cmd := "git",
  args:=#["describe", "--always", "--tags", "--dirty"], cwd := repo.dir
}

[Adomas Baliuka]

I'm also looking at doing something like this (though using the CLI is probably not a good idea)

def tmp : CliM PUnit := do
  let config ← mkLoadConfig (← getThe LakeOptions)
  let workspace ← loadWorkspace config
  dbg_trace "{workspace.root.dir}"
  pure ()

/--
Lean server printed an error:
libc++abi: terminating due to uncaught exception of type lean::exception:
Could not find native implementation of external declaration
'_private.Lake.Load.Lean.Elab.0.Lake.addToEnv'
(symbols 'l___private_Lake_Load_Lean_Elab_0__Lake_addToEnv___boxed'
or
'l___private_Lake_Load_Lean_Elab_0__Lake_addToEnv').

For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true`
in the relevant `lean_exe` statement in your `lakefile.lean`.
-/
-- #eval CliM.run tmp []