Something like `Lean.versionString` but for Mathlib?

Stream: new members

[Louis Cabarion]

How can I obtain the version string of Mathlib from within Lean?

I'm looking for something analogous to:

#eval Lean.versionString
-- "4.20.0-rc5"

… but for the version of Mathlib.

Additionally, is there a way to retrieve the commit hash of the currently running Lean and Mathlib versions from within Lean itself (i.e., without shelling out or relying on external tools)?

[Eric Wieser]

Regarding the commit, docs#Lean.githash

[Eric Wieser]

For mathlib the best you can do is invoke git in the directory containing the oleans, but in the extreme case there's no guarantee that git is even installed

[Louis Cabarion]

Thanks @Eric Wieser. The combination of Lean.versionString and Lean.githash is exactly what I needed for the Lean side.

Is there any particular reason why the corresponding Mathlib.versionString and Mathlib.githash would be undesirable or problematic to add, or has it simply not been implemented yet?

[Eric Wieser]

Those features exist in lean because it has a release process that involves releasing compiled binaries into which those strings are embedded. Mathlib releases no such compiled binary, and the release process is simply to make a git tag without running any other commands.

[Eric Wieser]

Maybe a better answer is "read the lake manifest (via the lake API) to discover what versions of things you are using"

[Jz Pan]

Maybe you can read the version from lake-manifest.json?