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

feat(src/CMakeLists): build stdlib using leanc instead of nested CMake run

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-18 16:10:22 +01:00
parent f6d3062524
commit dec8b76c32
4 changed files with 18 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/leanc.in
View file

@ -16,4 +16,4 @@ for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
fi
done
[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "$@" "-L$bindir" -ldl -Wl,-Bstatic -lleanstatic -lgmp @LEANC_EXTRA_LIBS@ -static-libgcc -static-libstdc++ -Wl,-Bdynamic -Wno-unused-command-line-argument
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "$@" "-L$bindir" -ldl -Wl,-Bstatic -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_LIBS@ -static-libgcc -static-libstdc++ -Wl,-Bdynamic -Wno-unused-command-line-argument

9
library/Makefile.in
View file

@ -34,16 +34,17 @@ $(STAGE1_DIR)/%.cpp: %.lean %.olean
@mkdir -p $(@D)
$(LEAN) $(OPTS) --cpp=$@ $<
$(STAGE1_DIR)/CMakeLists.txt: $(CPPS)
echo "add_library (cpp_stage1 OBJECT $(CPPS_CORE))" > $(STAGE1_DIR)/CMakeLists.txt
$(STAGE1_DIR)/%.o: $(STAGE1_DIR)/%.cpp
../bin/leanc -c -o $@ $< -O3
export-stage1: $(STAGE1_DIR)/CMakeLists.txt
$(STAGE1_DIR)/libleanstdlib.a: $(patsubst %.cpp,%.o,$(CPPS))
@ar rcs $@ $^
update-stage0:
rm -r $(STAGE0_DIR)/init
cp -R $(STAGE1_DIR)/init $(STAGE0_DIR)/init
echo "add_library (boot OBJECT $(CPPS_CORE))" > $(STAGE0_DIR)/CMakeLists.txt
.PRECIOUS: %.depend
.PRECIOUS: %.depend $(STAGE1_DIR)/%.cpp
include $(DEPS)

33
src/CMakeLists.txt
View file

@ -457,31 +457,20 @@ endif()
add_library(leanstatic_stage0 ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $<TARGET_OBJECTS:boot>)
target_link_libraries(leanstatic_stage0 ${EXTRA_LIBS})
if(STAGE1)
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $<TARGET_OBJECTS:cpp_stage1>)
target_link_libraries(leanstatic ${EXTRA_LIBS})
else()
# Build `leanstatic` after `export-stage1`, triggering a CMake re-run after (potentially) updating
# `src/stage1/CMakeLists.txt`
add_custom_target(boot_leanstatic
# '-G Ninja' complains otherwise
BYPRODUCTS libleanstatic.a
WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
COMMAND "${CMAKE_COMMAND}" "${CMAKE_SOURCE_DIR}" -DSTAGE1=ON
COMMAND "${CMAKE_COMMAND}" --build . --target leanstatic
COMMAND "${CMAKE_COMMAND}" "${CMAKE_SOURCE_DIR}" -DSTAGE1=OFF
DEPENDS export-stage1)
# import the output from the nested CMake run
add_library(leanstatic ${LEAN_LIBRARY_TYPE} IMPORTED)
set_target_properties(leanstatic PROPERTIES
IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic.a"
INTERFACE_LINK_LIBRARIES "${EXTRA_LIBS}")
add_dependencies(leanstatic boot_leanstatic)
endif()
add_custom_target(build_leanstdlib
# '-G Ninja' complains otherwise
BYPRODUCTS "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
COMMAND make -j8 ../src/stage1/libleanstdlib.a "LEAN=$<TARGET_FILE:lean_stage0>"
DEPENDS lean_stage0)
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
target_link_libraries(leanstatic "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a" ${EXTRA_LIBS})
add_dependencies(leanstatic build_leanstdlib)
ADD_CUSTOM_TARGET(bin_lib ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${LEAN_SOURCE_DIR}/stage1/libleanstdlib*" "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
DEPENDS leanstatic
)
# Configure leanc

7
src/shell/CMakeLists.txt
View file

@ -6,14 +6,9 @@ else()
set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/lean_stage0")
endif()
add_custom_target(export-stage1
COMMAND make -j8 export-stage1 "LEAN=$<TARGET_FILE:lean_stage0>"
DEPENDS lean_stage0
WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library")
add_custom_target(update-stage0
COMMAND make update-stage0
DEPENDS export-stage1
DEPENDS lean
WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library")
add_executable(lean lean.cpp)