sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: reformat all cmake files (#12218)

Browse Source 
The script to run for reformatting is `script/fmt`.
This commit is contained in:
Garmelon
2026-01-28 19:23:08 +01:00
committed by GitHub
parent 71be4901c3
commit 6dcd6c8f08
15 changed files with 1280 additions and 1026 deletions
Download Patch File Download Diff File Expand all files Collapse all files

81
CMakeLists.txt
View File

@@ -2,7 +2,6 @@ cmake_minimum_required(VERSION 3.11)
option(USE_MIMALLOC "use mimalloc" ON)
# store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
# https://stackoverflow.com/a/48555098/161659
# MUST be done before call to 'project'
@@ -35,7 +34,7 @@ include(ExternalProject)
project(LEAN CXX C)
if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
endif()
# Don't do anything with cadical on wasm
@@ -59,38 +58,47 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
endif()
string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
ExternalProject_add(cadical
ExternalProject_Add(
cadical
PREFIX cadical
GIT_REPOSITORY https://github.com/arminbiere/cadical
GIT_TAG rel-2.1.2
CONFIGURE_COMMAND ""
BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
CXX=${CADICAL_CXX}
CXXFLAGS=${CADICAL_CXXFLAGS}
LDFLAGS=${CADICAL_LDFLAGS}
BUILD_COMMAND
$(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS} LDFLAGS=${CADICAL_LDFLAGS}
BUILD_IN_SOURCE ON
INSTALL_COMMAND "")
set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
INSTALL_COMMAND ""
)
set(
CADICAL
${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX}
CACHE FILEPATH
"path to cadical binary"
FORCE
)
list(APPEND EXTRA_DEPENDS cadical)
endif()
list(APPEND CL_ARGS -DCADICAL=${CADICAL})
endif()
if(USE_MIMALLOC)
ExternalProject_add(mimalloc
ExternalProject_Add(
mimalloc
PREFIX mimalloc
GIT_REPOSITORY https://github.com/microsoft/mimalloc
GIT_TAG v2.2.3
# just download, we compile it as part of each stage as it is small
CONFIGURE_COMMAND ""
BUILD_COMMAND ""
INSTALL_COMMAND "")
INSTALL_COMMAND ""
)
list(APPEND EXTRA_DEPENDS mimalloc)
endif()
if(NOT STAGE1_PREV_STAGE)
ExternalProject_add(stage0
ExternalProject_Add(
stage0
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
SOURCE_SUBDIR src
BINARY_DIR stage0
@@ -98,38 +106,49 @@ if(NOT STAGE1_PREV_STAGE)
# (however, CI will override this as we need to embed the githash into the stage 1 library built
# by stage 0)
CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND "" # skip install
BUILD_ALWAYS
ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND
"" # skip install
DEPENDS ${EXTRA_DEPENDS}
)
list(APPEND EXTRA_DEPENDS stage0)
endif()
ExternalProject_add(stage1
ExternalProject_Add(
stage1
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage1
CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
CMAKE_ARGS
-DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0
-DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS ${EXTRA_DEPENDS}
STEP_TARGETS configure
)
ExternalProject_add(stage2
ExternalProject_Add(
stage2
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage2
CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
CMAKE_ARGS
-DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage1
EXCLUDE_FROM_ALL ON
STEP_TARGETS configure
)
ExternalProject_add(stage3
ExternalProject_Add(
stage3
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage3
CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
CMAKE_ARGS
-DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage2
@@ -138,24 +157,14 @@ ExternalProject_add(stage3
# targets forwarded to appropriate stages
add_custom_target(update-stage0
COMMAND $(MAKE) -C stage1 update-stage0
DEPENDS stage1)
add_custom_target(update-stage0 COMMAND $(MAKE) -C stage1 update-stage0 DEPENDS stage1)
add_custom_target(update-stage0-commit
COMMAND $(MAKE) -C stage1 update-stage0-commit
DEPENDS stage1)
add_custom_target(update-stage0-commit COMMAND $(MAKE) -C stage1 update-stage0-commit DEPENDS stage1)
add_custom_target(test
COMMAND $(MAKE) -C stage1 test
DEPENDS stage1)
add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1)
add_custom_target(clean-stdlib
COMMAND $(MAKE) -C stage1 clean-stdlib
DEPENDS stage1)
add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
install(CODE "execute_process(COMMAND make -C stage1 install)")
add_custom_target(check-stage3
COMMAND diff "stage2/bin/lean" "stage3/bin/lean"
DEPENDS stage3)
add_custom_target(check-stage3 COMMAND diff "stage2/bin/lean" "stage3/bin/lean" DEPENDS stage3)

13
script/fmt Executable file
View File

@@ -0,0 +1,13 @@
#!/usr/bin/env bash
set -euo pipefail
# This script expects to be run from the repo root.
# Format cmake files
find -regex '.*/CMakeLists\.txt\(\.in\)?\|.*\.cmake\(\.in\)?' \
! -path './build/*' \
! -path "./stage0/*" \
-exec \
uvx gersemi --in-place --line-length 120 --indent 2 \
--definitions src/cmake/Modules/ src/CMakeLists.txt \
-- {} +

488
src/CMakeLists.txt
View File

@@ -12,7 +12,7 @@ project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 29)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
if(LEAN_SPECIAL_VERSION_DESC)
@@ -30,8 +30,11 @@ set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform")
if(NOT LEAN_PLATFORM_TARGET)
# this may fail when the compiler is not clang, but this should only happen in local builds where
# the value of the variable is not of immediate relevance
execute_process(COMMAND ${CMAKE_C_COMPILER} --print-target-triple
OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(
COMMAND ${CMAKE_C_COMPILER} --print-target-triple
OUTPUT_VARIABLE LEAN_PLATFORM_TARGET
OUTPUT_STRIP_TRAILING_WHITESPACE
)
endif()
set(LEAN_EXTRA_LINKER_FLAGS_DEFAULT "")
@@ -46,8 +49,18 @@ if(CMAKE_SYSTEM_NAME MATCHES "Darwin")
endif()
set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
set(
LEAN_EXTRA_CXX_FLAGS
""
CACHE STRING
"Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical."
)
set(
LEAN_TEST_VARS
"LEAN_CC=${CMAKE_C_COMPILER}"
CACHE STRING
"Additional environment variables used when running tests"
)
if(NOT CMAKE_BUILD_TYPE)
message(STATUS "No build type selected, default to Release")
@@ -57,35 +70,35 @@ endif()
set(CMAKE_COLOR_MAKEFILE ON)
enable_testing()
option(MULTI_THREAD "MULTI_THREAD" ON)
option(CCACHE "use ccache" ON)
option(SPLIT_STACK "SPLIT_STACK" OFF)
option(MULTI_THREAD "MULTI_THREAD" ON)
option(CCACHE "use ccache" ON)
option(SPLIT_STACK "SPLIT_STACK" OFF)
# When OFF we disable LLVM support
option(LLVM "LLVM" OFF)
option(LLVM "LLVM" OFF)
# When ON we include githash in the version string
option(USE_GITHASH "GIT_HASH" ON)
option(USE_GITHASH "GIT_HASH" ON)
# When ON we install LICENSE files to CMAKE_INSTALL_PREFIX
option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
# When ON we install a copy of cadical
option(INSTALL_CADICAL "Install a copy of cadical" ON)
# FLAGS for disabling optimizations and debugging
option(FREE_VAR_RANGE_OPT "FREE_VAR_RANGE_OPT" ON)
option(HAS_LOCAL_OPT "HAS_LOCAL_OPT" ON)
option(ABSTRACTION_CACHE "ABSTRACTION_CACHE" ON)
option(TYPE_CLASS_CACHE "TYPE_CLASS_CACHE" ON)
option(TYPE_INFER_CACHE "TYPE_INFER_CACHE" ON)
option(ALPHA "ALPHA FEATURES" OFF)
option(FREE_VAR_RANGE_OPT "FREE_VAR_RANGE_OPT" ON)
option(HAS_LOCAL_OPT "HAS_LOCAL_OPT" ON)
option(ABSTRACTION_CACHE "ABSTRACTION_CACHE" ON)
option(TYPE_CLASS_CACHE "TYPE_CLASS_CACHE" ON)
option(TYPE_INFER_CACHE "TYPE_INFER_CACHE" ON)
option(ALPHA "ALPHA FEATURES" OFF)
option(TRACK_CUSTOM_ALLOCATORS "TRACK_CUSTOM_ALLOCATORS" OFF)
option(TRACK_LIVE_EXPRS "TRACK_LIVE_EXPRS" OFF)
option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON)
option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON)
option(SAVE_INFO "SAVE_INFO" ON)
option(SMALL_ALLOCATOR "SMALL_ALLOCATOR" OFF)
option(MMAP "MMAP" ON)
option(LAZY_RC "LAZY_RC" OFF)
option(RUNTIME_STATS "RUNTIME_STATS" OFF)
option(TRACK_LIVE_EXPRS "TRACK_LIVE_EXPRS" OFF)
option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON)
option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON)
option(SAVE_INFO "SAVE_INFO" ON)
option(SMALL_ALLOCATOR "SMALL_ALLOCATOR" OFF)
option(MMAP "MMAP" ON)
option(LAZY_RC "LAZY_RC" OFF)
option(RUNTIME_STATS "RUNTIME_STATS" OFF)
option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
option(USE_GMP "USE_GMP" ON)
option(USE_MIMALLOC "use mimalloc" ON)
@@ -95,8 +108,8 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
if(LAZY_RC MATCHES "ON")
set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -133,18 +146,18 @@ if(CHECK_OLEAN_VERSION MATCHES "ON")
endif()
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# TODO(WN): code size/performance tradeoffs
# - we're using -O3; it's /okay/
# - -Oz produces quite slow code
# - system libraries such as OpenGL are included in the JS but shouldn't be
# - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2)
# TODO(WN): code size/performance tradeoffs
# - we're using -O3; it's /okay/
# - -Oz produces quite slow code
# - system libraries such as OpenGL are included in the JS but shouldn't be
# - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2)
# From https://emscripten.org/docs/compiling/WebAssembly.html#backends:
# > The simple and safe thing is to pass all -s flags at both compile and link time.
set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto")
string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread")
string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}")
# From https://emscripten.org/docs/compiling/WebAssembly.html#backends:
# > The simple and safe thing is to pass all -s flags at both compile and link time.
set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto")
string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread")
string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}")
endif()
# Added for CTest
@@ -191,70 +204,72 @@ endif()
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
# Initialize CXXFLAGS.
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG")
set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG")
set(
CMAKE_CXX_FLAGS
"${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING"
)
set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG")
set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "-DLEAN_DEBUG")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "-DLEAN_DEBUG")
# SPLIT_STACK
if(SPLIT_STACK)
if((CMAKE_SYSTEM_NAME MATCHES "Linux") AND (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
string(APPEND CMAKE_CXX_FLAGS " -fsplit-stack -D LEAN_USE_SPLIT_STACK")
message(STATUS "Using split-stacks")
string(APPEND CMAKE_CXX_FLAGS " -fsplit-stack -D LEAN_USE_SPLIT_STACK")
message(STATUS "Using split-stacks")
else()
message(FATAL_ERROR "Split-stacks are only supported on Linux with g++")
message(FATAL_ERROR "Split-stacks are only supported on Linux with g++")
endif()
endif()
# Compiler-specific C++14 activation.
if(CMAKE_CXX_COMPILER_ID MATCHES "GNU")
execute_process(
COMMAND "${CMAKE_CXX_COMPILER}" -dumpversion OUTPUT_VARIABLE GCC_VERSION)
if(NOT (GCC_VERSION VERSION_GREATER 4.9 OR GCC_VERSION VERSION_EQUAL 4.9))
message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.9 or greater.")
endif()
execute_process(COMMAND "${CMAKE_CXX_COMPILER}" -dumpversion OUTPUT_VARIABLE GCC_VERSION)
if(NOT (GCC_VERSION VERSION_GREATER 4.9 OR GCC_VERSION VERSION_EQUAL 4.9))
message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.9 or greater.")
endif()
elseif(CMAKE_CXX_COMPILER_ID MATCHES "Clang")
string(APPEND CMAKE_CXX_FLAGS " -D__CLANG__")
elseif(MSVC)
# All good. Maybe enforce a recent version?
set(CMAKE_CXX_FLAGS "/GL /EHsc /W2 /Zc:implicitNoexcept- -D_SCL_SECURE_NO_WARNINGS ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
set(CMAKE_CXX_FLAGS_MINSIZEREL "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
set(CMAKE_CXX_FLAGS_RELEASE "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
set(LEAN_EXTRA_LINKER_FLAGS "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
set(CMAKE_STATIC_LINKER_FLAGS "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
# All good. Maybe enforce a recent version?
set(CMAKE_CXX_FLAGS "/GL /EHsc /W2 /Zc:implicitNoexcept- -D_SCL_SECURE_NO_WARNINGS ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
set(CMAKE_CXX_FLAGS_MINSIZEREL "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
set(CMAKE_CXX_FLAGS_RELEASE "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
set(LEAN_EXTRA_LINKER_FLAGS "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
set(CMAKE_STATIC_LINKER_FLAGS "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
elseif(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
message(STATUS "Emscripten is detected: Make sure the wrapped compiler supports C++14")
message(STATUS "Emscripten is detected: Make sure the wrapped compiler supports C++14")
else()
message(FATAL_ERROR "Unsupported compiler: ${CMAKE_CXX_COMPILER_ID}")
message(FATAL_ERROR "Unsupported compiler: ${CMAKE_CXX_COMPILER_ID}")
endif()
if(NOT MSVC)
set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++14 ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# smallest+slower | -Oz .. -Os .. -O3 | largest+faster
set(CMAKE_CXX_FLAGS_MINSIZEREL "-Oz ${CMAKE_CXX_FLAGS_MINSIZEREL}")
else ()
set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
endif()
set(CMAKE_CXX_FLAGS_RELEASE "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++14 ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# smallest+slower | -Oz .. -Os .. -O3 | largest+faster
set(CMAKE_CXX_FLAGS_MINSIZEREL "-Oz ${CMAKE_CXX_FLAGS_MINSIZEREL}")
else()
set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
endif()
set(CMAKE_CXX_FLAGS_RELEASE "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
elseif(MULTI_THREAD)
set(CMAKE_CXX_FLAGS_DEBUG "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
set(CMAKE_CXX_FLAGS_MINSIZEREL "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
set(CMAKE_CXX_FLAGS_RELEASE "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
set(CMAKE_CXX_FLAGS_DEBUG "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
set(CMAKE_CXX_FLAGS_MINSIZEREL "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
set(CMAKE_CXX_FLAGS_RELEASE "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
set(CMAKE_CXX_FLAGS_RELWITHASSERT "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
endif()
if(USE_GMP MATCHES "ON")
set(CMAKE_CXX_FLAGS "-D LEAN_USE_GMP ${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS "-D LEAN_USE_GMP ${CMAKE_CXX_FLAGS}")
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
include_directories(${GMP_INSTALL_PREFIX}/include)
set(GMP_LIBRARIES "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
@@ -283,7 +298,9 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# uv__platform_loop_delete, uv__platform_loop_init. Making additional
# LibUV features available on WebAssembly might require adapting the
# patch to include additional LibUV source files.
set(LIBUV_PATCH_IN "
set(
LIBUV_PATCH_IN
"
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5e8e0166..f3b29134 100644
--- a/CMakeLists.txt
@@ -300,18 +317,24 @@ index 5e8e0166..f3b29134 100644
if(CMAKE_SYSTEM_NAME STREQUAL \"Linux\")
list(APPEND uv_defines _GNU_SOURCE _POSIX_C_SOURCE=200112)
list(APPEND uv_libraries dl rt)
")
"
)
string(REPLACE "\n" "\\n" LIBUV_PATCH ${LIBUV_PATCH_IN})
ExternalProject_add(libuv
ExternalProject_Add(
libuv
PREFIX libuv
GIT_REPOSITORY https://github.com/libuv/libuv
# Sync version with flake.nix
GIT_TAG v1.48.0
CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DLIBUV_BUILD_TESTS=OFF -DLIBUV_BUILD_SHARED=OFF -DCMAKE_AR=${CMAKE_AR} -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_FLAGS=${LIBUV_EMSCRIPTEN_FLAGS}
PATCH_COMMAND git reset --hard HEAD && printf "${LIBUV_PATCH}" > patch.diff && git apply patch.diff
CMAKE_ARGS
-DCMAKE_BUILD_TYPE=Release -DLIBUV_BUILD_TESTS=OFF -DLIBUV_BUILD_SHARED=OFF -DCMAKE_AR=${CMAKE_AR}
-DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON
-DCMAKE_C_FLAGS=${LIBUV_EMSCRIPTEN_FLAGS}
PATCH_COMMAND git reset --hard HEAD && printf "${LIBUV_PATCH}" > patch.diff && git apply patch.diff
BUILD_IN_SOURCE ON
INSTALL_COMMAND "")
INSTALL_COMMAND ""
)
set(LIBUV_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/libuv/src/libuv/include")
set(LIBUV_LDFLAGS "${CMAKE_BINARY_DIR}/libuv/src/libuv/libuv.a")
else()
@@ -362,27 +385,51 @@ if(LLVM)
message(STATUS "'-DLLVM_CONFIG=<path/to/llvm-config>' not passed as CMake flag, finding `llvm-config` via CMake...")
find_program(LLVM_CONFIG "llvm-config")
if(NOT LLVM_CONFIG) # check that it was found
message(FATAL_ERROR "Unable to find 'llvm-config'")
message(FATAL_ERROR "Unable to find 'llvm-config'")
endif()
endif()
# check that we have 'llvm-config' version.
message(STATUS "Executing 'llvm-config --version' at '${LLVM_CONFIG}' to check configuration.")
execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(
COMMAND ${LLVM_CONFIG} --version
COMMAND_ERROR_IS_FATAL ANY
OUTPUT_VARIABLE LLVM_CONFIG_VERSION
ECHO_OUTPUT_VARIABLE
OUTPUT_STRIP_TRAILING_WHITESPACE
)
string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
message(
STATUS
"Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'"
)
if(NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
endif()
# -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
execute_process(COMMAND ${LLVM_CONFIG} --ldflags OUTPUT_VARIABLE LLVM_CONFIG_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --libs OUTPUT_VARIABLE LLVM_CONFIG_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --libdir OUTPUT_VARIABLE LLVM_CONFIG_LIBDIR OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --includedir OUTPUT_VARIABLE LLVM_CONFIG_INCLUDEDIR OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --cxxflags OUTPUT_VARIABLE LLVM_CONFIG_CXXFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --system-libs OUTPUT_VARIABLE LLVM_CONFIG_SYSTEM_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE)
message(STATUS "llvm-config: libdir '${LLVM_CONFIG_LIBDIR}' | ldflags '${LLVM_CONFIG_LDFLAGS}' | libs '${LLVM_CONFIG_LIBS}' | system libs '${LLVM_CONFIG_SYSTEM_LIBS}' | cxxflags: ${LLVM_CONFIG_CXXFLAGS} | includedir: ${LLVM_CONFIG_INCLUDEDIR}")
execute_process(COMMAND ${LLVM_CONFIG} --ldflags OUTPUT_VARIABLE LLVM_CONFIG_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --libs OUTPUT_VARIABLE LLVM_CONFIG_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --libdir OUTPUT_VARIABLE LLVM_CONFIG_LIBDIR OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(
COMMAND ${LLVM_CONFIG} --includedir
OUTPUT_VARIABLE LLVM_CONFIG_INCLUDEDIR
OUTPUT_STRIP_TRAILING_WHITESPACE
)
execute_process(
COMMAND ${LLVM_CONFIG} --cxxflags
OUTPUT_VARIABLE LLVM_CONFIG_CXXFLAGS
OUTPUT_STRIP_TRAILING_WHITESPACE
)
execute_process(
COMMAND ${LLVM_CONFIG} --system-libs
OUTPUT_VARIABLE LLVM_CONFIG_SYSTEM_LIBS
OUTPUT_STRIP_TRAILING_WHITESPACE
)
message(
STATUS
"llvm-config: libdir '${LLVM_CONFIG_LIBDIR}' | ldflags '${LLVM_CONFIG_LDFLAGS}' | libs '${LLVM_CONFIG_LIBS}' | system libs '${LLVM_CONFIG_SYSTEM_LIBS}' | cxxflags: ${LLVM_CONFIG_CXXFLAGS} | includedir: ${LLVM_CONFIG_INCLUDEDIR}"
)
else()
message(WARNING "Disabling LLVM support")
endif()
@@ -402,7 +449,10 @@ if(CMAKE_SYSTEM_NAME MATCHES "Darwin")
elseif(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
else()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
string(
APPEND TOOLCHAIN_STATIC_LINKER_FLAGS
" -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group"
)
endif()
set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -429,27 +479,30 @@ else()
endif()
if(LLVM)
string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
string(
APPEND LEANSHARED_LINKER_FLAGS
" -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}"
)
string(APPEND CMAKE_CXX_FLAGS " -I${LLVM_CONFIG_INCLUDEDIR}")
endif()
if(LLVM AND STAGE GREATER 0)
# Here, we perform a replacement of `llvm-host` with `llvm`. This is necessary for our cross-compile
# builds in `script/prepare-llvm-*.sh`.
# - Recall that the host's copy of LLVM binaries and libraries is at
# `llvm-host`, and the target's copy of LLVM binaries and libraries is at
# `llvm`.
# - In an ideal world, we would run the target's `llvm/bin/llvm-config` and get the correct link options for the target
# (e.g. `-Lllvm/lib/libLLVM`.)
# - However, the target's `llvm/bin/llvm-config` has a different target
# triple from the host, and thus cannot be run on the host.
# - So, we run the host `llvm-host/bin/llvm-config` from which we pick up
# compiler options, and change the output of the host to point to the target.
# - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while
# we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
string(REPLACE "llvm-host" "llvm" CMAKE_CXX_FLAGS ${CMAKE_CXX_FLAGS})
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
# Here, we perform a replacement of `llvm-host` with `llvm`. This is necessary for our cross-compile
# builds in `script/prepare-llvm-*.sh`.
# - Recall that the host's copy of LLVM binaries and libraries is at
# `llvm-host`, and the target's copy of LLVM binaries and libraries is at
# `llvm`.
# - In an ideal world, we would run the target's `llvm/bin/llvm-config` and get the correct link options for the target
# (e.g. `-Lllvm/lib/libLLVM`.)
# - However, the target's `llvm/bin/llvm-config` has a different target
# triple from the host, and thus cannot be run on the host.
# - So, we run the host `llvm-host/bin/llvm-config` from which we pick up
# compiler options, and change the output of the host to point to the target.
# - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while
# we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
string(REPLACE "llvm-host" "llvm" CMAKE_CXX_FLAGS ${CMAKE_CXX_FLAGS})
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
endif()
# We always strip away unused declarations to reduce binary sizes as the time cost is small and the
@@ -474,7 +527,10 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive")
string(
APPEND LAKESHARED_LINKER_FLAGS
" -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
)
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean")
elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
@@ -482,13 +538,19 @@ elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin")
string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib")
string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib")
string(
APPEND LAKESHARED_LINKER_FLAGS
" -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib"
)
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
elseif(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
string(APPEND CMAKE_CXX_FLAGS " -fPIC")
string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
elseif(CMAKE_SYSTEM_NAME MATCHES "Windows")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive")
string(
APPEND LAKESHARED_LINKER_FLAGS
" -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive"
)
endif()
if(CMAKE_SYSTEM_NAME MATCHES "Linux")
@@ -524,7 +586,7 @@ endif()
# Linux ignores undefined symbols in shared libraries by default
if(MULTI_THREAD AND NOT MSVC AND NOT CMAKE_SYSTEM_NAME MATCHES "Darwin")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -pthread")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -pthread")
endif()
# Git HASH
@@ -541,9 +603,10 @@ else()
if(USE_LAKE AND STAGE EQUAL 0)
# we need to embed *some* hash for Lake to invalidate stage 1 on stage 0 changes
execute_process(
COMMAND git ls-tree HEAD "${CMAKE_CURRENT_SOURCE_DIR}/../../stage0" --object-only
OUTPUT_VARIABLE GIT_SHA1
OUTPUT_STRIP_TRAILING_WHITESPACE)
COMMAND git ls-tree HEAD "${CMAKE_CURRENT_SOURCE_DIR}/../../stage0" --object-only
OUTPUT_VARIABLE GIT_SHA1
OUTPUT_STRIP_TRAILING_WHITESPACE
)
message(STATUS "stage0 sha1: ${GIT_SHA1}")
# Now that we've prepared the information for the next stage, we can forget that we will use
# Lake in the future as we won't use it in this stage
@@ -576,15 +639,18 @@ else()
endif()
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
if(USE_MIMALLOC)
file(COPY "${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include/mimalloc.h" DESTINATION "${LEAN_BINARY_DIR}/include/lean")
file(
COPY "${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include/mimalloc.h"
DESTINATION "${LEAN_BINARY_DIR}/include/lean"
)
endif()
install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
include_directories(${LEAN_SOURCE_DIR})
include_directories(${CMAKE_BINARY_DIR}) # version.h etc., "private" headers
include_directories(${CMAKE_BINARY_DIR}/include) # config.h etc., "public" headers
include_directories(${CMAKE_BINARY_DIR}) # version.h etc., "private" headers
include_directories(${CMAKE_BINARY_DIR}/include) # config.h etc., "public" headers
# Lean code only needs this one include
string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include")
@@ -604,13 +670,12 @@ add_subdirectory(shell)
# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
# in the world)
add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
set_target_properties(leaninitialize PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leaninitialize)
set_target_properties(
leaninitialize
PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leaninitialize
)
add_library(leanshell STATIC util/shell.cpp)
set_target_properties(leanshell PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leanshell)
set_target_properties(leanshell PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leanshell)
if(CMAKE_SYSTEM_NAME MATCHES "Windows")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lleanmanifest -Wl,--no-whole-archive")
endif()
@@ -618,30 +683,36 @@ endif()
if(STAGE GREATER 1)
# reuse C++ parts, which don't change
add_library(leanrt_initial-exec STATIC IMPORTED)
set_target_properties(leanrt_initial-exec PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
set_target_properties(
leanrt_initial-exec
PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
)
add_library(leanrt STATIC IMPORTED)
set_target_properties(leanrt PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a")
set_target_properties(leanrt PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a")
add_library(leancpp_1 STATIC IMPORTED)
set_target_properties(leancpp_1 PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
set_target_properties(leancpp_1 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
add_library(leancpp STATIC IMPORTED)
set_target_properties(leancpp PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_custom_target(copy-leancpp
COMMAND cmake -E copy_if_different "${PREV_STAGE}/runtime/libleanrt_initial-exec.a" "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
set_target_properties(leancpp PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_custom_target(
copy-leancpp
COMMAND
cmake -E copy_if_different "${PREV_STAGE}/runtime/libleanrt_initial-exec.a"
"${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
COMMAND
cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a"
)
add_dependencies(leanrt_initial-exec copy-leancpp)
add_dependencies(leanrt copy-leancpp)
add_dependencies(leancpp_1 copy-leancpp)
add_dependencies(leancpp copy-leancpp)
if(LLVM)
add_custom_target(copy-lean-h-bc
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/lean.h.bc" "${CMAKE_BINARY_DIR}/lib/lean/lean.h.bc")
add_dependencies(leancpp copy-lean-h-bc)
add_custom_target(
copy-lean-h-bc
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/lean.h.bc" "${CMAKE_BINARY_DIR}/lib/lean/lean.h.bc"
)
add_dependencies(leancpp copy-lean-h-bc)
endif()
else()
add_subdirectory(runtime)
@@ -661,17 +732,19 @@ else()
# leancpp without `initialize` (see `leaninitialize` above)
add_library(leancpp_1 STATIC ${LEAN_OBJS})
set_target_properties(leancpp_1 PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leancpp_1)
set_target_properties(
leancpp_1
PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leancpp_1
)
add_library(leancpp STATIC ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
set_target_properties(leancpp PROPERTIES
OUTPUT_NAME leancpp)
set_target_properties(leancpp PROPERTIES OUTPUT_NAME leancpp)
endif()
if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
add_custom_target(copy-cadical
COMMAND cmake -E copy_if_different "${CADICAL}" "${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX}")
add_custom_target(
copy-cadical
COMMAND cmake -E copy_if_different "${CADICAL}" "${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX}"
)
add_dependencies(leancpp copy-cadical)
endif()
@@ -690,7 +763,10 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# We set `ERROR_ON_UNDEFINED_SYMBOLS=0` because our build of LibUV does not
# define all symbols, see the comment about LibUV on WebAssembly further up
# in this file.
string(APPEND LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0")
string(
APPEND LEAN_EXE_LINKER_FLAGS
" ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0"
)
endif()
# Build the compiler using the bootstrapped C sources for stage0, and use
@@ -704,18 +780,21 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
list(APPEND STDLIBS Lake LeanChecker)
endif()
add_custom_target(make_stdlib ALL
add_custom_target(
make_stdlib
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
# We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make ${STDLIBS}
VERBATIM)
VERBATIM
)
# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
# of Lean runtime to be built.
if(LLVM AND STAGE EQUAL 1)
add_dependencies(make_stdlib runtime_bc)
add_dependencies(make_stdlib runtime_bc)
endif()
# We declare these as separate custom targets so they use separate `make` invocations, which makes `make` recompute which dependencies
@@ -723,75 +802,98 @@ endif()
if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
# dummy targets, see `MAIN_MODULE` discussion above
add_custom_target(Init_shared ALL
add_custom_target(
Init_shared
ALL
DEPENDS make_stdlib leanrt_initial-exec
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
add_custom_target(leanshared ALL
add_custom_target(
leanshared
ALL
DEPENDS Init_shared leancpp
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX}
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
add_custom_target(lake_shared ALL
add_custom_target(
lake_shared
ALL
DEPENDS leanshared
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
else()
add_custom_target(Init_shared ALL
add_custom_target(
Init_shared
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS make_stdlib leanrt_initial-exec
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init_shared
VERBATIM)
VERBATIM
)
add_custom_target(leanshared ALL
add_custom_target(
leanshared
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS Init_shared leancpp_1 leancpp leanshell leaninitialize
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
VERBATIM)
VERBATIM
)
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
endif()
if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
add_custom_target(lake_shared
add_custom_target(
lake_shared
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
VERBATIM)
add_custom_target(lake ALL
VERBATIM
)
add_custom_target(
lake
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_shared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
VERBATIM)
VERBATIM
)
add_custom_target(leanchecker ALL
add_custom_target(
leanchecker
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_shared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanchecker
VERBATIM)
VERBATIM
)
endif()
if(PREV_STAGE)
add_custom_target(update-stage0
add_custom_target(
update-stage0
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/.."
)
add_custom_target(update-stage0-commit
COMMAND git commit -m "chore: update stage0"
DEPENDS update-stage0)
add_custom_target(update-stage0-commit COMMAND git commit -m "chore: update stage0" DEPENDS update-stage0)
endif()
# use Bash version for building, use Lean version in bin/ for tests & distribution
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
if(STAGE GREATER 0 AND EXISTS "${LEAN_SOURCE_DIR}/Leanc.lean" AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
add_custom_target(leanc ALL
add_custom_target(
leanc
ALL
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
VERBATIM)
VERBATIM
)
endif()
file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
@@ -802,18 +904,22 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
install(PROGRAMS "${CADICAL}" DESTINATION bin)
endif()
add_custom_target(clean-stdlib
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true)
add_custom_target(
clean-stdlib
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true
)
add_custom_target(clean-olean
DEPENDS clean-stdlib)
add_custom_target(clean-olean DEPENDS clean-stdlib)
install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
install(
DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
DESTINATION lib
PATTERN temp EXCLUDE
PATTERN "*.export" EXCLUDE
PATTERN "*.hash" EXCLUDE
PATTERN "*.trace" EXCLUDE
PATTERN "*.rsp" EXCLUDE)
PATTERN "*.rsp" EXCLUDE
)
# symlink source into expected installation location for go-to-definition, if file system allows it
file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
@@ -826,27 +932,33 @@ else()
file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
endif()
install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.md"
PATTERN examples EXCLUDE)
install(
DIRECTORY "${CMAKE_SOURCE_DIR}/"
DESTINATION src/lean
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.md"
PATTERN examples EXCLUDE
)
if(STAGE GREATER 0 AND INSTALL_LICENSE)
install(FILES "${CMAKE_SOURCE_DIR}/../LICENSE" "${CMAKE_SOURCE_DIR}/../LICENSES" DESTINATION ".")
endif()
file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include
FILES_MATCHING PATTERN "*.h")
file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include FILES_MATCHING PATTERN "*.h")
set(LEAN_INSTALL_PREFIX "" CACHE STRING "If set, set CMAKE_INSTALL_PREFIX to this value + version name")
if(LEAN_INSTALL_PREFIX)
string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME)
set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX")
set(
LEAN_INSTALL_SUFFIX
"-${LOWER_SYSTEM_NAME}"
CACHE STRING
"If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX"
)
set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
endif()
if(USE_LAKE_CACHE AND STAGE EQUAL 1)
set(LAKE_ARTIFACT_CACHE_TOML "true")
else()

10
src/cmake/Modules/FindGMP.cmake
View File

@@ -1,13 +1,13 @@
if (GMP_INCLUDE_DIR AND GMP_LIBRARIES)
if(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
# Already in cache, be silent
set(GMP_FIND_QUIETLY TRUE)
endif (GMP_INCLUDE_DIR AND GMP_LIBRARIES)
endif(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
find_path(GMP_INCLUDE_DIR NAMES gmp.h )
find_path(GMP_INCLUDE_DIR NAMES gmp.h)
find_library(GMP_LIBRARIES NAMES gmp libgmp mpir REQUIRED)
#find_library(GMPXX_LIBRARIES NAMES gmpxx libgmpxx )
#MESSAGE(STATUS "GMP: " ${GMP_LIBRARIES}) # " " ${GMPXX_LIBRARIES} )
include(FindPackageHandleStandardArgs)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)

10
src/cmake/Modules/FindLibUV.cmake
View File

@@ -1,13 +1,13 @@
if (LIBUV_FOUND)
if(LIBUV_FOUND)
# Already in cache, be silent
set(LIBUV_FIND_QUIETLY TRUE)
endif (LIBUV_FOUND)
endif(LIBUV_FOUND)
find_package(PkgConfig REQUIRED)
pkg_search_module(LIBUV REQUIRED libuv)
MESSAGE(STATUS "LIBUV_LDFLAGS: " ${LIBUV_LDFLAGS})
MESSAGE(STATUS "LIBUV_INCLUDE_DIRS: " ${LIBUV_INCLUDE_DIRS})
message(STATUS "LIBUV_LDFLAGS: " ${LIBUV_LDFLAGS})
message(STATUS "LIBUV_INCLUDE_DIRS: " ${LIBUV_INCLUDE_DIRS})
include(FindPackageHandleStandardArgs)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(LibUV DEFAULT_MSG LIBUV_FOUND)
find_package_handle_standard_args(LibUV DEFAULT_MSG LIBUV_FOUND)
mark_as_advanced(LIBUV_INCLUDE_DIRS LIBUV_LDFLAGS)

859
src/cmake/Modules/FindWindowsSDK.cmake
View File

File diff suppressed because it is too large Load Diff

347
src/cmake/Modules/GetGitRevisionDescription.cmake
View File

@@ -46,7 +46,7 @@
# http://www.boost.org/LICENSE_1_0.txt)
if(__get_git_revision_description)
return()
return()
endif()
set(__get_git_revision_description YES)
@@ -65,223 +65,192 @@ get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH)
# C:/bla/.git
#
function(_git_find_closest_git_dir _start_dir _git_dir_var)
set(cur_dir "${_start_dir}")
set(git_dir "${_start_dir}/.git")
while(NOT EXISTS "${git_dir}")
# .git dir not found, search parent directories
set(git_previous_parent "${cur_dir}")
get_filename_component(cur_dir "${cur_dir}" DIRECTORY)
if(cur_dir STREQUAL git_previous_parent)
# We have reached the root directory, we are not in git
set(${_git_dir_var}
""
PARENT_SCOPE)
return()
endif()
set(git_dir "${cur_dir}/.git")
endwhile()
set(${_git_dir_var}
"${git_dir}"
PARENT_SCOPE)
set(cur_dir "${_start_dir}")
set(git_dir "${_start_dir}/.git")
while(NOT EXISTS "${git_dir}")
# .git dir not found, search parent directories
set(git_previous_parent "${cur_dir}")
get_filename_component(cur_dir "${cur_dir}" DIRECTORY)
if(cur_dir STREQUAL git_previous_parent)
# We have reached the root directory, we are not in git
set(${_git_dir_var} "" PARENT_SCOPE)
return()
endif()
set(git_dir "${cur_dir}/.git")
endwhile()
set(${_git_dir_var} "${git_dir}" PARENT_SCOPE)
endfunction()
function(get_git_head_revision _refspecvar _hashvar)
_git_find_closest_git_dir("${CMAKE_CURRENT_SOURCE_DIR}" GIT_DIR)
_git_find_closest_git_dir("${CMAKE_CURRENT_SOURCE_DIR}" GIT_DIR)
if("${ARGN}" STREQUAL "ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR")
set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR TRUE)
else()
set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR FALSE)
endif()
if(NOT "${GIT_DIR}" STREQUAL "")
file(RELATIVE_PATH _relative_to_source_dir "${CMAKE_SOURCE_DIR}"
"${GIT_DIR}")
if("${_relative_to_source_dir}" MATCHES "[.][.]"
AND NOT ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
# We've gone above the CMake root dir.
set(GIT_DIR "")
endif()
endif()
if("${GIT_DIR}" STREQUAL "")
set(${_refspecvar}
"GITDIR-NOTFOUND"
PARENT_SCOPE)
set(${_hashvar}
"GITDIR-NOTFOUND"
PARENT_SCOPE)
return()
if("${ARGN}" STREQUAL "ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR")
set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR TRUE)
else()
set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR FALSE)
endif()
if(NOT "${GIT_DIR}" STREQUAL "")
file(RELATIVE_PATH _relative_to_source_dir "${CMAKE_SOURCE_DIR}" "${GIT_DIR}")
if("${_relative_to_source_dir}" MATCHES "[.][.]" AND NOT ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
# We've gone above the CMake root dir.
set(GIT_DIR "")
endif()
endif()
if("${GIT_DIR}" STREQUAL "")
set(${_refspecvar} "GITDIR-NOTFOUND" PARENT_SCOPE)
set(${_hashvar} "GITDIR-NOTFOUND" PARENT_SCOPE)
return()
endif()
# Check if the current source dir is a git submodule or a worktree.
# In both cases .git is a file instead of a directory.
# Check if the current source dir is a git submodule or a worktree.
# In both cases .git is a file instead of a directory.
#
if(NOT IS_DIRECTORY ${GIT_DIR})
# The following git command will return a non empty string that
# points to the super project working tree if the current
# source dir is inside a git submodule.
# Otherwise the command will return an empty string.
#
if(NOT IS_DIRECTORY ${GIT_DIR})
# The following git command will return a non empty string that
# points to the super project working tree if the current
# source dir is inside a git submodule.
# Otherwise the command will return an empty string.
#
execute_process(
COMMAND "${GIT_EXECUTABLE}" rev-parse
--show-superproject-working-tree
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
OUTPUT_VARIABLE out
ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
if(NOT "${out}" STREQUAL "")
# If out is empty, GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a submodule
file(READ ${GIT_DIR} submodule)
string(REGEX REPLACE "gitdir: (.*)$" "\\1" GIT_DIR_RELATIVE
${submodule})
string(STRIP ${GIT_DIR_RELATIVE} GIT_DIR_RELATIVE)
get_filename_component(SUBMODULE_DIR ${GIT_DIR} PATH)
get_filename_component(GIT_DIR ${SUBMODULE_DIR}/${GIT_DIR_RELATIVE}
ABSOLUTE)
set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
else()
# GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a worktree
file(READ ${GIT_DIR} worktree_ref)
# The .git directory contains a path to the worktree information directory
# inside the parent git repo of the worktree.
#
string(REGEX REPLACE "gitdir: (.*)$" "\\1" git_worktree_dir
${worktree_ref})
string(STRIP ${git_worktree_dir} git_worktree_dir)
_git_find_closest_git_dir("${git_worktree_dir}" GIT_DIR)
set(HEAD_SOURCE_FILE "${git_worktree_dir}/HEAD")
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" rev-parse --show-superproject-working-tree
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
OUTPUT_VARIABLE out
ERROR_QUIET
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if(NOT "${out}" STREQUAL "")
# If out is empty, GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a submodule
file(READ ${GIT_DIR} submodule)
string(REGEX REPLACE "gitdir: (.*)$" "\\1" GIT_DIR_RELATIVE ${submodule})
string(STRIP ${GIT_DIR_RELATIVE} GIT_DIR_RELATIVE)
get_filename_component(SUBMODULE_DIR ${GIT_DIR} PATH)
get_filename_component(GIT_DIR ${SUBMODULE_DIR}/${GIT_DIR_RELATIVE} ABSOLUTE)
set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
else()
set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
endif()
set(GIT_DATA "${CMAKE_CURRENT_BINARY_DIR}/CMakeFiles/git-data")
if(NOT EXISTS "${GIT_DATA}")
file(MAKE_DIRECTORY "${GIT_DATA}")
# GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a worktree
file(READ ${GIT_DIR} worktree_ref)
# The .git directory contains a path to the worktree information directory
# inside the parent git repo of the worktree.
#
string(REGEX REPLACE "gitdir: (.*)$" "\\1" git_worktree_dir ${worktree_ref})
string(STRIP ${git_worktree_dir} git_worktree_dir)
_git_find_closest_git_dir("${git_worktree_dir}" GIT_DIR)
set(HEAD_SOURCE_FILE "${git_worktree_dir}/HEAD")
endif()
else()
set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
endif()
set(GIT_DATA "${CMAKE_CURRENT_BINARY_DIR}/CMakeFiles/git-data")
if(NOT EXISTS "${GIT_DATA}")
file(MAKE_DIRECTORY "${GIT_DATA}")
endif()
if(NOT EXISTS "${HEAD_SOURCE_FILE}")
return()
endif()
set(HEAD_FILE "${GIT_DATA}/HEAD")
configure_file("${HEAD_SOURCE_FILE}" "${HEAD_FILE}" COPYONLY)
if(NOT EXISTS "${HEAD_SOURCE_FILE}")
return()
endif()
set(HEAD_FILE "${GIT_DATA}/HEAD")
configure_file("${HEAD_SOURCE_FILE}" "${HEAD_FILE}" COPYONLY)
configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in"
"${GIT_DATA}/grabRef.cmake" @ONLY)
include("${GIT_DATA}/grabRef.cmake")
configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in" "${GIT_DATA}/grabRef.cmake" @ONLY)
include("${GIT_DATA}/grabRef.cmake")
set(${_refspecvar}
"${HEAD_REF}"
PARENT_SCOPE)
set(${_hashvar}
"${HEAD_HASH}"
PARENT_SCOPE)
set(${_refspecvar} "${HEAD_REF}" PARENT_SCOPE)
set(${_hashvar} "${HEAD_HASH}" PARENT_SCOPE)
endfunction()
function(git_describe _var)
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
get_git_head_revision(refspec hash)
if(NOT GIT_FOUND)
set(${_var}
"GIT-NOTFOUND"
PARENT_SCOPE)
return()
endif()
if(NOT hash)
set(${_var}
"HEAD-HASH-NOTFOUND"
PARENT_SCOPE)
return()
endif()
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
get_git_head_revision(refspec hash)
if(NOT GIT_FOUND)
set(${_var} "GIT-NOTFOUND" PARENT_SCOPE)
return()
endif()
if(NOT hash)
set(${_var} "HEAD-HASH-NOTFOUND" PARENT_SCOPE)
return()
endif()
# TODO sanitize
#if((${ARGN}" MATCHES "&&") OR
# (ARGN MATCHES "||") OR
# (ARGN MATCHES "\\;"))
# message("Please report the following error to the project!")
# message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}")
#endif()
# TODO sanitize
#if((${ARGN}" MATCHES "&&") OR
# (ARGN MATCHES "||") OR
# (ARGN MATCHES "\\;"))
# message("Please report the following error to the project!")
# message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}")
#endif()
#message(STATUS "Arguments to execute_process: ${ARGN}")
#message(STATUS "Arguments to execute_process: ${ARGN}")
execute_process(
COMMAND "${GIT_EXECUTABLE}" describe --tags --always ${hash} ${ARGN}
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
if(NOT res EQUAL 0)
set(out "${out}-${res}-NOTFOUND")
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" describe --tags --always ${hash} ${ARGN}
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if(NOT res EQUAL 0)
set(out "${out}-${res}-NOTFOUND")
endif()
set(${_var}
"${out}"
PARENT_SCOPE)
set(${_var} "${out}" PARENT_SCOPE)
endfunction()
function(git_describe_working_tree _var)
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
if(NOT GIT_FOUND)
set(${_var}
"GIT-NOTFOUND"
PARENT_SCOPE)
return()
endif()
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
if(NOT GIT_FOUND)
set(${_var} "GIT-NOTFOUND" PARENT_SCOPE)
return()
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" describe --dirty ${ARGN}
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
if(NOT res EQUAL 0)
set(out "${out}-${res}-NOTFOUND")
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" describe --dirty ${ARGN}
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if(NOT res EQUAL 0)
set(out "${out}-${res}-NOTFOUND")
endif()
set(${_var}
"${out}"
PARENT_SCOPE)
set(${_var} "${out}" PARENT_SCOPE)
endfunction()
function(git_get_exact_tag _var)
git_describe(out --exact-match ${ARGN})
set(${_var}
"${out}"
PARENT_SCOPE)
git_describe(out --exact-match ${ARGN})
set(${_var} "${out}" PARENT_SCOPE)
endfunction()
function(git_local_changes _var)
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
get_git_head_revision(refspec hash)
if(NOT GIT_FOUND)
set(${_var}
"GIT-NOTFOUND"
PARENT_SCOPE)
return()
endif()
if(NOT hash)
set(${_var}
"HEAD-HASH-NOTFOUND"
PARENT_SCOPE)
return()
endif()
if(NOT GIT_FOUND)
find_package(Git QUIET)
endif()
get_git_head_revision(refspec hash)
if(NOT GIT_FOUND)
set(${_var} "GIT-NOTFOUND" PARENT_SCOPE)
return()
endif()
if(NOT hash)
set(${_var} "HEAD-HASH-NOTFOUND" PARENT_SCOPE)
return()
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" diff-index --quiet HEAD --
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
if(res EQUAL 0)
set(${_var}
"CLEAN"
PARENT_SCOPE)
else()
set(${_var}
"DIRTY"
PARENT_SCOPE)
endif()
execute_process(
COMMAND "${GIT_EXECUTABLE}" diff-index --quiet HEAD --
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
RESULT_VARIABLE res
OUTPUT_VARIABLE out
ERROR_QUIET
OUTPUT_STRIP_TRAILING_WHITESPACE
)
if(res EQUAL 0)
set(${_var} "CLEAN" PARENT_SCOPE)
else()
set(${_var} "DIRTY" PARENT_SCOPE)
endif()
endfunction()

33
src/cmake/Modules/GetGitRevisionDescription.cmake.in
View File

@@ -23,26 +23,25 @@ file(READ "@HEAD_FILE@" HEAD_CONTENTS LIMIT 1024)
string(STRIP "${HEAD_CONTENTS}" HEAD_CONTENTS)
if(HEAD_CONTENTS MATCHES "ref")
# named branch
string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}")
if(EXISTS "@GIT_DIR@/${HEAD_REF}")
configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
else()
if(EXISTS "@GIT_DIR@/packed-refs")
configure_file("@GIT_DIR@/packed-refs" "@GIT_DATA@/packed-refs"
COPYONLY)
file(READ "@GIT_DATA@/packed-refs" PACKED_REFS)
if(${PACKED_REFS} MATCHES "([0-9a-z]*) ${HEAD_REF}")
set(HEAD_HASH "${CMAKE_MATCH_1}")
endif()
endif()
# named branch
string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}")
if(EXISTS "@GIT_DIR@/${HEAD_REF}")
configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
else()
if(EXISTS "@GIT_DIR@/packed-refs")
configure_file("@GIT_DIR@/packed-refs" "@GIT_DATA@/packed-refs" COPYONLY)
file(READ "@GIT_DATA@/packed-refs" PACKED_REFS)
if(${PACKED_REFS} MATCHES "([0-9a-z]*) ${HEAD_REF}")
set(HEAD_HASH "${CMAKE_MATCH_1}")
endif()
endif()
endif()
else()
# detached HEAD
configure_file("@GIT_DIR@/HEAD" "@GIT_DATA@/head-ref" COPYONLY)
# detached HEAD
configure_file("@GIT_DIR@/HEAD" "@GIT_DATA@/head-ref" COPYONLY)
endif()
if(NOT HEAD_HASH)
file(READ "@GIT_DATA@/head-ref" HEAD_HASH LIMIT 1024)
string(STRIP "${HEAD_HASH}" HEAD_HASH)
file(READ "@GIT_DATA@/head-ref" HEAD_HASH LIMIT 1024)
string(STRIP "${HEAD_HASH}" HEAD_HASH)
endif()

7
src/cmake/Modules/README.md
View File

@@ -12,3 +12,10 @@ of the `cmake-modules` repository:
```bash
./update-modules.sh /path-to-lean4-repo/src/cmake/Modules
```
Afterwards, reformat them by running the following command from the root of this
repository:
```bash
scripts/fmt
```

27
src/kernel/CMakeLists.txt
View File

@@ -1,5 +1,22 @@
add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
inductive.cpp trace.cpp instantiate_mvars.cpp)
add_library(
kernel
OBJECT
level.cpp
expr.cpp
expr_eq_fn.cpp
for_each_fn.cpp
replace_fn.cpp
abstract.cpp
instantiate.cpp
local_ctx.cpp
declaration.cpp
environment.cpp
type_checker.cpp
init_module.cpp
expr_cache.cpp
equiv_manager.cpp
quot.cpp
inductive.cpp
trace.cpp
instantiate_mvars.cpp
)

28
src/library/CMakeLists.txt
View File

@@ -1,11 +1,25 @@
add_library(library OBJECT expr_lt.cpp
bin_app.cpp constants.cpp max_sharing.cpp
module.cpp dynlib.cpp replace_visitor.cpp num.cpp
class.cpp util.cpp print.cpp annotation.cpp
reducible.cpp init_module.cpp
profiling.cpp time_task.cpp
add_library(
library
OBJECT
expr_lt.cpp
bin_app.cpp
constants.cpp
max_sharing.cpp
module.cpp
dynlib.cpp
replace_visitor.cpp
num.cpp
class.cpp
util.cpp
print.cpp
annotation.cpp
reducible.cpp
init_module.cpp
profiling.cpp
time_task.cpp
formatter.cpp
elab_environment.cpp
init_attribute.cpp
llvm.cpp
ir_interpreter.cpp)
ir_interpreter.cpp
)

4
src/library/constructions/CMakeLists.txt
View File

@@ -1,3 +1 @@
add_library(constructions OBJECT cases_on.cpp
init_module.cpp
util.cpp)
add_library(constructions OBJECT cases_on.cpp init_module.cpp util.cpp)

77
src/runtime/CMakeLists.txt
View File

@@ -1,9 +1,39 @@
set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp byteslice.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp uv/signal.cpp)
set(
RUNTIME_OBJS
debug.cpp
thread.cpp
mpz.cpp
utf8.cpp
object.cpp
apply.cpp
exception.cpp
interrupt.cpp
memory.cpp
stackinfo.cpp
compact.cpp
init_module.cpp
io.cpp
hash.cpp
byteslice.cpp
platform.cpp
alloc.cpp
allocprof.cpp
sharecommon.cpp
stack_overflow.cpp
process.cpp
object_ref.cpp
mpn.cpp
mutex.cpp
libuv.cpp
uv/net_addr.cpp
uv/event_loop.cpp
uv/timer.cpp
uv/tcp.cpp
uv/udp.cpp
uv/dns.cpp
uv/system.cpp
uv/signal.cpp
)
if(USE_MIMALLOC)
list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c)
# Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir
@@ -13,35 +43,39 @@ if(USE_MIMALLOC)
if(CMAKE_CXX_COMPILER_ID MATCHES "AppleClang|Clang")
string(APPEND MIMALLOC_FLAGS " -Wno-deprecated")
endif()
set_source_files_properties(${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c PROPERTIES
# (C flags are incomplete, compile as C++ instead like everything else)
LANGUAGE CXX
COMPILE_FLAGS ${MIMALLOC_FLAGS})
set_source_files_properties(
${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c
PROPERTIES
# (C flags are incomplete, compile as C++ instead like everything else)
LANGUAGE CXX
COMPILE_FLAGS ${MIMALLOC_FLAGS}
)
endif()
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
set_target_properties(leanrt_initial-exec PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
# The above library, like all other C++ code, is built using `-ftls-model=initial-exec`, which is necessary for linking it into `leanshared`,
# but introduces a measurable overhead while accessing the thread-local variable `g_heap` when allocating and deallocating. Therefore we compile
# the runtime again with the more restrictive `local-exec` and use it when linking Lean code statically, i.e. not against `leanshared`.
add_library(leanrt STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY})
set_target_properties(leanrt PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY})
if(NOT MSVC)
target_compile_options(leanrt PRIVATE -ftls-model=local-exec)
target_compile_options(leanrt PRIVATE -ftls-model=local-exec)
endif()
# We do not export Lean symbols when statically linking on Windows.
if(CMAKE_SYSTEM_NAME MATCHES "Windows")
target_compile_options(leanrt PRIVATE -ULEAN_EXPORTING)
target_compile_options(leanrt PRIVATE -ULEAN_EXPORTING)
endif()
if(LLVM)
if(NOT CMAKE_CXX_COMPILER_ID MATCHES "Clang")
message(FATAL_ERROR "building 'lean.h.bc', need CMAKE_CXX_COMPILER_ID to match Clang to build LLVM bitcode file of Lean runtime.")
message(
FATAL_ERROR
"building 'lean.h.bc', need CMAKE_CXX_COMPILER_ID to match Clang to build LLVM bitcode file of Lean runtime."
)
endif()
FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
file(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
# generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
# drop '#pragma once' in .c file to avoid warning
@@ -51,7 +85,10 @@ if(LLVM)
add_custom_command(
OUTPUT ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc
DEPENDS ${RUNTIME_OBJS} ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c
COMMAND bash -ec "${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc"
VERBATIM)
COMMAND
bash -ec
"${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc"
VERBATIM
)
add_custom_target(runtime_bc DEPENDS ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc)
endif()

294
src/shell/CMakeLists.txt
View File

@@ -1,15 +1,14 @@
add_library(leanmain STATIC lean.cpp)
set_target_properties(leanmain PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leanmain)
set_target_properties(leanmain PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp OUTPUT_NAME leanmain)
# library must contain at least one non-manifest file
# We use `CONFIGURE` instead of `WRITE` so as to avoid touching the file on each run
file(CONFIGURE OUTPUT ${CMAKE_BINARY_DIR}/temp/empty.c CONTENT "")
add_library(leanmanifest STATIC ${CMAKE_BINARY_DIR}/temp/empty.c manifest.rc)
set_target_properties(leanmanifest PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/lean
OUTPUT_NAME leanmanifest)
set_target_properties(
leanmanifest
PROPERTIES ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/lean OUTPUT_NAME leanmanifest
)
if(LLVM)
if(CMAKE_SYSTEM_NAME MATCHES "Linux")
@@ -23,7 +22,10 @@ if(LLVM)
set(LLVM_SYSTEM_LIBS "-lz")
endif()
if(NOT CMAKE_SYSTEM_NAME MATCHES "Darwin")
string(APPEND LEAN_EXE_LINKER_FLAGS " `llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic")
string(
APPEND LEAN_EXE_LINKER_FLAGS
" `llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic"
)
else()
string(APPEND LEAN_EXE_LINKER_FLAGS " `llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}")
endif()
@@ -32,207 +34,251 @@ if(LLVM)
endif()
endif()
add_custom_target(lean ALL
add_custom_target(
lean
ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared leanmain
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean
COMMAND_EXPAND_LISTS)
COMMAND_EXPAND_LISTS
)
# use executable of current stage for tests
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
add_test(lean_help1 "${CMAKE_BINARY_DIR}/bin/lean" --help)
add_test(lean_help2 "${CMAKE_BINARY_DIR}/bin/lean" -h)
add_test(lean_help1 "${CMAKE_BINARY_DIR}/bin/lean" --help)
add_test(lean_help2 "${CMAKE_BINARY_DIR}/bin/lean" -h)
add_test(lean_version1 "${CMAKE_BINARY_DIR}/bin/lean" --version)
if(NOT EMSCRIPTEN)
add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
endif()
add_test(lean_ghash1 "${CMAKE_BINARY_DIR}/bin/lean" -g)
add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash)
add_test(lean_ghash1 "${CMAKE_BINARY_DIR}/bin/lean" -g)
add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash)
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
add_test(
lean_unknown_file1
bash
"${LEAN_SOURCE_DIR}/cmake/check_failure.sh"
"${CMAKE_BINARY_DIR}/bin/lean"
"boofoo.lean"
)
if(EMSCRIPTEN)
configure_file("${LEAN_SOURCE_DIR}/bin/lean.in" "${CMAKE_BINARY_DIR}/bin/lean")
endif()
# LEANC_OPTS in CXX is necessary for macOS c++ to find its headers
set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'")
set(
TEST_VARS
"PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'"
)
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
FOREACH(T ${LEANTESTS})
foreach(T ${LEANTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN RUN TESTS
file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
FOREACH(T ${LEANRUNTESTS})
foreach(T ${LEANRUNTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN RUN doc/examples
file(GLOB LEANDOCEXS "${LEAN_SOURCE_DIR}/../doc/examples/*.lean")
FOREACH(T ${LEANDOCEXS})
foreach(T ${LEANDOCEXS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN COMPILER TESTS
file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
FOREACH(T ${LEANCOMPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T)
foreach(T ${LEANCOMPTESTS})
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endforeach(T)
add_test(NAME leancomptest_foreign
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign"
COMMAND bash -c "${LEAN_BIN}/leanmake --always-make")
add_test(NAME leancomptest_doc_example
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world")
add_test(
NAME leancomptest_foreign
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign"
COMMAND bash -c "${LEAN_BIN}/leanmake --always-make"
)
add_test(
NAME leancomptest_doc_example
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world"
)
# LEAN INTERPRETER TESTS
file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
FOREACH(T ${LEANINTERPTESTS})
foreach(T ${LEANINTERPTESTS})
if(NOT EXISTS "${T}.no_interpreter")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH} (interpreted)"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH} (interpreted)"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN BENCHMARK TESTS
# do not test all .lean files in bench/
file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out")
FOREACH(T_OUT ${LEANBENCHTESTS})
foreach(T_OUT ${LEANBENCHTESTS})
string(REPLACE ".expected.out" "" T ${T_OUT})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T_OUT)
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endforeach(T_OUT)
file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
FOREACH(T ${LEANINTERPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T)
foreach(T ${LEANINTERPTESTS})
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endforeach(T)
# LEAN TESTS using --trust=0
file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean")
FOREACH(T ${LEANT0TESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
ENDFOREACH(T)
foreach(T ${LEANT0TESTS})
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endforeach(T)
# LEAN PACKAGE TESTS
file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
FOREACH(T ${LEANPKGTESTS})
foreach(T ${LEANPKGTESTS})
if(EXISTS "${T}/test.sh")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${T}"
COMMAND bash -c "${TEST_VARS} ./test.sh")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}" WORKING_DIRECTORY "${T}" COMMAND bash -c "${TEST_VARS} ./test.sh")
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN SERVER TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean")
FOREACH(T ${LEANTESTS})
foreach(T ${LEANTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN INTERACTIVE SERVER TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
FOREACH(T ${LEANTESTS})
foreach(T ${LEANTESTS})
if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN INTERACTIVE PROJECT SERVER TESTS
file(GLOB_RECURSE LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/projects/*Test.lean")
FOREACH(T ${LEANTESTS})
foreach(T ${LEANTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive/projects"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive/projects"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# LEAN DOCSTRING PARSER TESTS
file(GLOB_RECURSE LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/docparse/*_[0-9][0-9][0-9][0-9]")
FOREACH(T ${LEANTESTS})
foreach(T ${LEANTESTS})
if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/docparse"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
get_filename_component(T_NAME ${T} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/docparse"
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
)
endif()
ENDFOREACH(T)
endforeach(T)
# Create a lake test for each test and examples subdirectory of `lake`
# which contains a `test.sh` file, excluding the following test(s):
# bootstrap: too slow
# toolchain: requires elan to download toolchain
# online: downloads remote repositories
file(GLOB_RECURSE LEANLAKETESTS
file(
GLOB_RECURSE LEANLAKETESTS
#"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
"${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh")
FOREACH(T ${LEANLAKETESTS})
"${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
)
foreach(T ${LEANLAKETESTS})
if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(NAME "${T_PATH}"
WORKING_DIRECTORY "${T_DIR}"
COMMAND bash -c "
get_filename_component(T_DIR ${T} DIRECTORY)
get_filename_component(DIR_NAME ${T_DIR} NAME)
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
add_test(
NAME "${T_PATH}"
WORKING_DIRECTORY "${T_DIR}"
COMMAND
bash -c
"
set -eu
export ${TEST_VARS}
LAKE=lake ./test.sh")
LAKE=lake ./test.sh"
)
endif()
ENDFOREACH(T)
endforeach(T)

28
src/util/CMakeLists.txt
View File

@@ -1,9 +1,23 @@
configure_file(ffi.cpp "${CMAKE_BINARY_DIR}/util/ffi.cpp" @ONLY)
add_library(util OBJECT name.cpp name_set.cpp
escaped.cpp bit_tricks.cpp ascii.cpp
path.cpp lbool.cpp init_module.cpp list_fn.cpp
timeit.cpp timer.cpp
name_generator.cpp kvmap.cpp map_foreach.cpp
options.cpp option_declarations.cpp
"${CMAKE_BINARY_DIR}/util/ffi.cpp")
add_library(
util
OBJECT
name.cpp
name_set.cpp
escaped.cpp
bit_tricks.cpp
ascii.cpp
path.cpp
lbool.cpp
init_module.cpp
list_fn.cpp
timeit.cpp
timer.cpp
name_generator.cpp
kvmap.cpp
map_foreach.cpp
options.cpp
option_declarations.cpp
"${CMAKE_BINARY_DIR}/util/ffi.cpp"
)