From ca163818927aafa714d25b0ee62d0710cd3552c1 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 4 Feb 2015 15:58:29 -0500
Subject: [PATCH] feat(bin): add linja.in and LEAN_BIN_DEP cmake option

see the discussion in issue #422
---
 .gitignore              | 2 --
 bin/.gitignore          | 3 +++
 bin/{linja => linja.in} | 8 ++++++--
 src/CMakeLists.txt      | 5 +++++
 4 files changed, 14 insertions(+), 4 deletions(-)
 rename bin/{linja => linja.in} (98%)

diff --git a/.gitignore b/.gitignore
index 384e4fefe..72646e979 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,5 +22,3 @@ CMakeFiles/
 doc/html
 make.deps
 src/emacs/dependencies
-bin/leanemacs
-bin/leanemacs.bat
\ No newline at end of file
diff --git a/bin/.gitignore b/bin/.gitignore
index 5b9b1653d..f9cd55816 100644
--- a/bin/.gitignore
+++ b/bin/.gitignore
@@ -1,4 +1,7 @@
 lean
 lean.exe
+leanemacs
+leanemacs.bat
+linja
 python_lib/six.pyc
 python_lib/__init__.pyc
diff --git a/bin/linja b/bin/linja.in
similarity index 98%
rename from bin/linja
rename to bin/linja.in
index afd64badf..52ce63d02 100755
--- a/bin/linja
+++ b/bin/linja.in
@@ -102,6 +102,7 @@ g_leantags_path    = "USE DEFAULT" # System will search automatically
 g_ninja_path       = "USE DEFAULT" # System will search automatically
 g_flycheck_header  = "FLYCHECK_BEGIN"
 g_flycheck_footer  = "FLYCHECK_END"
+g_lean_bin_dep_flag= "@LEAN_BIN_DEP@" == "ON"
 
 g_logger = logging.getLogger('linja_logger')
 g_debug_mode = False
@@ -609,9 +610,12 @@ def clear_cache(args):
 def build_olean(lean, olean, clean, dlean, ilean, base):
     (lean, olean, clean, dlean, ilean, base) = list(map(escape_ninja_char, (lean, olean, clean, dlean, ilean, base)))
     if clean.startswith(base):
-        str = """build %s %s %s: LEAN %s | %s\n""" % (olean, ilean, clean, lean, dlean)
+        str = """build %s %s %s: LEAN %s | %s""" % (olean, ilean, clean, lean, dlean)
     else:
-        str = """build %s %s: LEAN %s | %s\n""" % (olean, ilean, lean, dlean)
+        str = """build %s %s: LEAN %s | %s""" % (olean, ilean, lean, dlean)
+    if g_lean_bin_dep_flag:
+        str += " %s" % g_lean_path
+    str += "\n"
     str += "  DLEAN_FILE=%s\n" % dlean
     str += "  OLEAN_FILE=%s\n" % olean
     str += "  CLEAN_FILE=%s\n" % clean
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3c6e70fe1..1730a6efb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -33,6 +33,8 @@ option(CROSS_COMPILE      "CROSS_COMPILE"     OFF)
 option(CONSERVE_MEMORY    "CONSERVE_MEMORY"   OFF)
 # Include MSYS2 required DLLs and binaries in the binary distribution package
 option(INCLUDE_MSYS2_DLLS "INCLUDE_MSYS2_DLLS" OFF)
+# When ON we add lean binary dependency to standard and HOTT libraries
+option(LEAN_BIN_DEP       "LEAN_BIN_DEP"      ON)
 # Directory that include lean emacs mode dependecies
 set(EMACS_DEPENDENCIES "${CMAKE_SOURCE_DIR}/emacs/dependencies")
 
@@ -299,6 +301,9 @@ configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
 configure_file("${LEAN_SOURCE_DIR}/../bin/leanemacs.in" "${LEAN_SOURCE_DIR}/../bin/leanemacs")
 configure_file("${LEAN_SOURCE_DIR}/../bin/leanemacs.bat.in" "${LEAN_SOURCE_DIR}/../bin/leanemacs.bat")
 
+# linja
+configure_file("${LEAN_SOURCE_DIR}/../bin/linja.in" "${LEAN_SOURCE_DIR}/../bin/linja" @ONLY)
+
 include_directories("${LEAN_BINARY_DIR}")
 add_subdirectory(util)
 set(LEAN_LIBS ${LEAN_LIBS} util)