max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(CMakeLists): trying again to fix new build system

Browse source 
Trying to find a solution that works in all platforms.
This commit is contained in:
Leonardo de Moura 2018-10-19 10:25:28 -07:00
parent 45b505e808
commit 8ce945bc24
3 changed files with 39 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/Makefile
View file

@ -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

28
library/Makefile.in Normal file
View file

@ -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)

15
src/CMakeLists.txt
View file

@ -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"
)