From 6e33020da495ec8cf221bdf375debdce10708e15 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 29 Dec 2020 15:07:33 +0100
Subject: [PATCH] feat: version information API

---
 src/CMakeLists.txt   |  2 +-
 src/Init/Meta.lean   | 27 +++++++++++++++++++++++++++
 src/config.h.in      |  2 ++
 src/library/util.cpp |  2 +-
 src/version.h.in     |  2 ++
 5 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6a26bafba7..93451d9789 100644
--- a/src/CMakeLists.txt
+++ b/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()
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 3d254a3de8..454b2cc4fb 100644
--- a/src/Init/Meta.lean
+++ b/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
diff --git a/src/config.h.in b/src/config.h.in
index 0fec0771e5..f109cc37a6 100644
--- a/src/config.h.in
+++ b/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@
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 656c79edab..ed84e951b1 100644
--- a/src/library/util.cpp
+++ b/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 {
diff --git a/src/version.h.in b/src/version.h.in
index 34fc743945..65ea409c0c 100644
--- a/src/version.h.in
+++ b/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@"