From 8ce945bc249682b247a497d8f2ca513c2f2befef Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Oct 2018 10:25:28 -0700
Subject: [PATCH] fix(CMakeLists): trying again to fix new build system

Trying to find a solution that works in all platforms.
---
 library/Makefile    |  5 +++--
 library/Makefile.in | 28 ++++++++++++++++++++++++++++
 src/CMakeLists.txt  | 15 ++++++++-------
 3 files changed, 39 insertions(+), 9 deletions(-)
 create mode 100644 library/Makefile.in

diff --git a/library/Makefile b/library/Makefile
index af3990ec1d..1fb7851c35 100644
--- a/library/Makefile
+++ b/library/Makefile
@@ -1,10 +1,11 @@
 # Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 # Released under Apache 2.0 license as described in the file LICENSE.
 # Authors: Simon Hudon, Sebastian Ullrich
-LEAN ?= lean
+LEAN = ../bin/lean
 SRCS = $(shell find . -name '*.lean')
 OBJS = $(SRCS:.lean=.olean)
 DEPS = $(SRCS:.lean=.depend)
+OPTS = -s40000
 
 .PHONY: all clean
 
@@ -16,7 +17,7 @@ depends: $(DEPS)
 	@echo $(<:.lean=.olean): `$(LEAN) --deps $< | python relative.py` > $@
 
 %.olean: %.lean %.depend
-	$(LEAN) --make $<
+	$(LEAN) $(OPTS) --make $<
 
 clean:
 	find . -name *.olean -delete
diff --git a/library/Makefile.in b/library/Makefile.in
new file mode 100644
index 0000000000..c4c54fe13b
--- /dev/null
+++ b/library/Makefile.in
@@ -0,0 +1,28 @@
+# Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+# Authors: Simon Hudon, Sebastian Ullrich
+LEAN = ../bin/lean
+SRCS = $(shell find . -name '*.lean')
+OBJS = $(SRCS:.lean=.olean)
+DEPS = $(SRCS:.lean=.depend)
+OPTS = @LEAN_EXTRA_MAKE_OPTS@
+
+.PHONY: all clean
+
+all: $(OBJS)
+
+depends: $(DEPS)
+
+%.depend: %.lean
+	@echo $(<:.lean=.olean): `$(LEAN) --deps $< | python relative.py` > $@
+
+%.olean: %.lean %.depend
+	$(LEAN) $(OPTS) --make $<
+
+clean:
+	find . -name *.olean -delete
+	find . -name *.depend -delete
+
+.PRECIOUS: %.depend
+
+include $(DEPS)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8e7ffd8342..2e7e109592 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -385,9 +385,16 @@ else()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
+# OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
+# See issue #1721
+if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
+  set(LEAN_EXTRA_MAKE_OPTS -s40000 ${LEAN_EXTRA_MAKE_OPTS})
+endif ()
+
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
 configure_file("${LEAN_SOURCE_DIR}/../library/init/version.lean.in" "${LEAN_SOURCE_DIR}/../library/init/version.lean")
+configure_file("${LEAN_SOURCE_DIR}/../library/Makefile.in" "${LEAN_SOURCE_DIR}/../library/Makefile")
 
 include_directories("${LEAN_BINARY_DIR}")
 add_subdirectory(runtime)
@@ -459,15 +466,9 @@ add_style_check_target(style "${LEAN_SOURCES}")
 add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py" ${LEAN_SOURCES})
 endif()
 
-# OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
-# See issue #1721
-if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
-  set(LEAN_EXTRA_MAKE_OPTS -s40000 ${LEAN_EXTRA_MAKE_OPTS})
-endif ()
-
 add_custom_target(
     standard_lib ALL
-    COMMAND make -j4 -e "LEAN=${LEAN_SOURCE_DIR}/../bin/lean ${LEAN_EXTRA_MAKE_OPTS}"
+    COMMAND make -j4
     DEPENDS bin_lean
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
     )