From b5e7b2ab6eb7027f2b09801e4e31be5a355917c2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 2 Nov 2021 15:25:24 +0100
Subject: [PATCH] feat: Lean.githash

---
 src/Init/Meta.lean       | 6 +++---
 src/runtime/platform.cpp | 3 +++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 29b98bcbbd..9f91448da8 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -22,9 +22,9 @@ def version.minor : Nat := version.getMinor ()
 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 "lean_get_githash"]
+constant getGithash (u : Unit) : String
+def githash : String := getGithash ()
 
 @[extern c inline "LEAN_VERSION_IS_RELEASE"]
 constant version.getIsRelease (u : Unit) : Bool
diff --git a/src/runtime/platform.cpp b/src/runtime/platform.cpp
index e992c74f67..129dbc214a 100644
--- a/src/runtime/platform.cpp
+++ b/src/runtime/platform.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "runtime/object.h"
+#include "githash.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT obj_res lean_system_platform_nbits(obj_arg) {
@@ -38,4 +39,6 @@ extern "C" LEAN_EXPORT uint8 lean_system_platform_emscripten(obj_arg) {
     return 0;
 #endif
 }
+
+extern "C" object * lean_get_githash() { return lean_mk_string(LEAN_GITHASH); }
 }