feat(shell/lean): add git hash to executable

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -136,6 +136,15 @@ endif()
 
 include_directories(${LEAN_SOURCE_DIR})
 
+add_custom_command(
+  OUTPUT ${LEAN_BINARY_DIR}/githash.h
+  COMMAND ${LEAN_SOURCE_DIR}/cmake/mk_githash_dot_h.sh ${LEAN_BINARY_DIR}
+  DEPENDS ${LEAN_SOURCE_DIR}/../.git/HEAD ${LEAN_SOURCE_DIR}/../.git/index
+)
+add_custom_target(githash
+  DEPENDS ${LEAN_BINARY_DIR}/githash.h ${LEAN_SOURCE_DIR}/../.git/HEAD ${LEAN_SOURCE_DIR}/../.git/index
+)
+
 add_subdirectory(util)
 set(LEAN_LIBS ${LEAN_LIBS} util)
 add_subdirectory(util/numerics)

src/cmake/mk_githash_dot_h.sh

@@ -0,0 +1,6 @@
+#!/bin/sh
+Hash=`git rev-parse HEAD`
+cat > $1/githash.h <<EOF
+// Automatically generated file, DO NOT EDIT
+char const * g_githash = "$Hash";
+EOF

src/shell/CMakeLists.txt

@@ -1,6 +1,7 @@
 configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/version.h")
 include_directories("${LEAN_BINARY_DIR}")
 add_executable(lean lean.cpp)
+add_dependencies(lean githash)
 target_link_libraries(lean ${EXTRA_LIBS})
 add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
 add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex2.lean")

src/shell/lean.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <signal.h>
 #include <cstdlib>
 #include <getopt.h>
+#include <string>
 #include "util/stackinfo.h"
 #include "util/debug.h"
 #include "util/interrupt.h"
@@ -18,6 +19,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/frontend.h"
 #include "frontends/lua/register_modules.h"
 #include "version.h"
+#include "githash.h" // NOLINT
 
 using lean::shell;
 using lean::frontend;
@@ -34,7 +36,7 @@ static void on_ctrl_c(int ) {
 }
 
 static void display_header(std::ostream & out) {
-    out << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
+    out << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ", commit " << std::string(g_githash).substr(0, 12) << ")\n";
 }
 
 static void display_help(std::ostream & out) {
@@ -46,6 +48,7 @@ static void display_help(std::ostream & out) {
     std::cout << "Miscellaneous:\n";
     std::cout << "  --help -h      display this message\n";
     std::cout << "  --version -v   display version number\n";
+    std::cout << "  --githash      display the git commit hash number used to build this binary\n";
     std::cout << "  --luahook=num  how often the Lua interpreter checks the interrupted flag,\n";
     std::cout << "                 it is useful for interrupting non-terminating user scripts,\n";
     std::cout << "                 0 means 'do not check'.\n";
@@ -71,6 +74,7 @@ static struct option g_long_options[] = {
     {"lean",       no_argument,       0, 'l'},
     {"lua",        no_argument,       0, 'u'},
     {"luahook",    required_argument, 0, 'c'},
+    {"githash",    no_argument,       0, 'g'},
     {0, 0, 0, 0}
 };
 
@@ -79,13 +83,16 @@ int main(int argc, char ** argv) {
     lean::register_modules();
     input_kind default_k = input_kind::Lean; // default
     while (true) {
-        int c = getopt_long(argc, argv, "vhc:012", g_long_options, &optind);
+        int c = getopt_long(argc, argv, "gvhc:012", g_long_options, &optind);
         if (c == -1)
             break; // end of command line
         switch (c) {
         case 'v':
             display_header(std::cout);
             return 0;
+        case 'g':
+            std::cout << g_githash << "\n";
+            return 0;
         case 'h':
             display_help(std::cout);
             return 0;