Print the version of lean that is running

Question

In python, I can get the version of python I am using like this:

import sys
print(sys.version)

3.11.0 (main, May 25 2023, 12:06:07) [GCC 12.2.0]

How do I do the equivalent thing in Lean?

Answer 1

Try this:

#eval Lean.versionString

Alternatively, from the command line, you can invoke lean -v to print the version.

In Lake projects, there is a a file lean-toolchain that sets the version of Lean.