feat: version information API

src/CMakeLists.txt

@@ -373,7 +373,7 @@ endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
 # Version
-configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
+configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if (${STAGE} EQUAL 0)
   set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 1")
 else()

src/Init/Meta.lean

@@ -9,6 +9,33 @@ prelude
 import Init.Data.Array.Basic
 
 namespace Lean
+
+@[extern c inline "lean_box(LEAN_VERSION_MAJOR)"]
+private constant version.getMajor (u : Unit) : Nat
+def version.major : Nat := version.getMajor ()
+
+@[extern c inline "lean_box(LEAN_VERSION_MINOR)"]
+private constant version.getMinor (u : Unit) : Nat
+def version.minor : Nat := version.getMinor ()
+
+@[extern c inline "lean_box(LEAN_VERSION_PATCH)"]
+private constant version.getPatch (u : Unit) : Nat
+def version.patch : Nat := version.getPatch ()
+
+-- @[extern c inline "lean_mk_string(LEAN_GITHASH)"]
+-- constant getGithash (u : Unit) : String
+-- def githash : String := getGithash ()
+
+@[extern c inline "LEAN_VERSION_IS_RELEASE"]
+constant version.getIsRelease (u : Unit) : Bool
+def version.isRelease : Bool := version.getIsRelease ()
+
+/-- Additional version description like "nightly-2018-03-11" -/
+@[extern c inline "lean_mk_string(LEAN_SPECIAL_VERSION_DESC)"]
+constant version.getSpecialDesc (u : Unit) : String
+def version.specialDesc : String := version.getSpecialDesc ()
+
+
 /- Valid identifier names -/
 def isGreek (c : Char) : Bool :=
   0x391 ≤ c.val && c.val ≤ 0x3dd

src/config.h.in

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <lean/version.h>
+
 @LEAN_SMALL_ALLOCATOR@
 @LEAN_LAZY_RC@
 @LEAN_COMPRESSED_OBJECT_HEADER@

src/library/util.cpp

@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 #include "library/projection.h"
 #include "library/replace_visitor.h"
 #include "library/num.h"
-#include "version.h"
+#include <lean/version.h>
 #include "githash.h" // NOLINT
 
 namespace lean {

src/version.h.in

@@ -1,6 +1,8 @@
+#pragma once
 #define LEAN_VERSION_MAJOR @LEAN_VERSION_MAJOR@
 #define LEAN_VERSION_MINOR @LEAN_VERSION_MINOR@
 #define LEAN_VERSION_PATCH @LEAN_VERSION_PATCH@
+#define LEAN_VERSION_IS_RELEASE @LEAN_VERSION_IS_RELEASE@
 
 // Additional version description like "nightly-2018-03-11"
 #define LEAN_SPECIAL_VERSION_DESC "@LEAN_SPECIAL_VERSION_DESC@"