From 6dcd6c8f08aeeada967470b3571934c85fac0bb3 Mon Sep 17 00:00:00 2001 From: Garmelon Date: Wed, 28 Jan 2026 19:23:08 +0100 Subject: [PATCH] chore: reformat all cmake files (#12218) The script to run for reformatting is `script/fmt`. --- CMakeLists.txt | 81 +- script/fmt | 13 + src/CMakeLists.txt | 488 ++++++---- src/cmake/Modules/FindGMP.cmake | 10 +- src/cmake/Modules/FindLibUV.cmake | 10 +- src/cmake/Modules/FindWindowsSDK.cmake | 859 +++++++++--------- .../Modules/GetGitRevisionDescription.cmake | 347 ++++--- .../GetGitRevisionDescription.cmake.in | 33 +- src/cmake/Modules/README.md | 7 + src/kernel/CMakeLists.txt | 27 +- src/library/CMakeLists.txt | 28 +- src/library/constructions/CMakeLists.txt | 4 +- src/runtime/CMakeLists.txt | 77 +- src/shell/CMakeLists.txt | 294 +++--- src/util/CMakeLists.txt | 28 +- 15 files changed, 1280 insertions(+), 1026 deletions(-) create mode 100755 script/fmt diff --git a/CMakeLists.txt b/CMakeLists.txt index 79b02efae3..ca09a5d4ac 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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) diff --git a/script/fmt b/script/fmt new file mode 100755 index 0000000000..ec255be9f2 --- /dev/null +++ b/script/fmt @@ -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 \ + -- {} + diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3d57848dd3..bf144551d7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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=' 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 $) -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} $) - 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() diff --git a/src/cmake/Modules/FindGMP.cmake b/src/cmake/Modules/FindGMP.cmake index 9300547eff..424e31a100 100644 --- a/src/cmake/Modules/FindGMP.cmake +++ b/src/cmake/Modules/FindGMP.cmake @@ -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) \ No newline at end of file +find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) +mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) diff --git a/src/cmake/Modules/FindLibUV.cmake b/src/cmake/Modules/FindLibUV.cmake index e20d1ef010..353fe769b0 100644 --- a/src/cmake/Modules/FindLibUV.cmake +++ b/src/cmake/Modules/FindLibUV.cmake @@ -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) diff --git a/src/cmake/Modules/FindWindowsSDK.cmake b/src/cmake/Modules/FindWindowsSDK.cmake index 782bab7a64..012be6c1a4 100644 --- a/src/cmake/Modules/FindWindowsSDK.cmake +++ b/src/cmake/Modules/FindWindowsSDK.cmake @@ -64,96 +64,90 @@ set(_win_sdk_buildsanddirs) # pre-output set(_winsdk_vistaonly) # search parameters set(_winsdk_kits) # search parameters - set(_WINDOWSSDK_ANNOUNCE OFF) if(NOT WINDOWSSDK_FOUND AND (NOT WindowsSDK_FIND_QUIETLY)) - set(_WINDOWSSDK_ANNOUNCE ON) + set(_WINDOWSSDK_ANNOUNCE ON) endif() macro(_winsdk_announce) - if(_WINSDK_ANNOUNCE) - message(STATUS ${ARGN}) - endif() + if(_WINSDK_ANNOUNCE) + message(STATUS ${ARGN}) + endif() endmacro() # See https://developer.microsoft.com/en-us/windows/downloads/sdk-archive - # although version numbers listed on that page don't necessarily match the directory # used by the installer. -set(_winsdk_win10vers - 10.0.26100.0 - 10.0.22621.0 - 10.0.22000.0 - 10.0.20348.0 - 10.0.19041.0 - 10.0.18362.0 # Win10 1903 "19H1" - 10.0.17763.0 # Win10 1809 "October 2018 Update" - 10.0.17134.0 # Redstone 4 aka Win10 1803 "April 2018 Update" - 10.0.17133.0 # Redstone 4 aka Win10 1803 "April 2018 Update" - 10.0.16299.0 # Redstone 3 aka Win10 1709 "Fall Creators Update" - 10.0.15063.0 # Redstone 2 aka Win10 1703 "Creators Update" - 10.0.14393.0 # Redstone aka Win10 1607 "Anniversary Update" - 10.0.10586.0 # TH2 aka Win10 1511 - 10.0.10240.0 # Win10 RTM - 10.0.10150.0 # just ucrt - 10.0.10056.0 +set( + _winsdk_win10vers + 10.0.26100.0 + 10.0.22621.0 + 10.0.22000.0 + 10.0.20348.0 + 10.0.19041.0 + 10.0.18362.0 # Win10 1903 "19H1" + 10.0.17763.0 # Win10 1809 "October 2018 Update" + 10.0.17134.0 # Redstone 4 aka Win10 1803 "April 2018 Update" + 10.0.17133.0 # Redstone 4 aka Win10 1803 "April 2018 Update" + 10.0.16299.0 # Redstone 3 aka Win10 1709 "Fall Creators Update" + 10.0.15063.0 # Redstone 2 aka Win10 1703 "Creators Update" + 10.0.14393.0 # Redstone aka Win10 1607 "Anniversary Update" + 10.0.10586.0 # TH2 aka Win10 1511 + 10.0.10240.0 # Win10 RTM + 10.0.10150.0 # just ucrt + 10.0.10056.0 ) if(WindowsSDK_FIND_COMPONENTS MATCHES "tools") - set(_WINDOWSSDK_IGNOREMSVC ON) - _winsdk_announce("Checking for tools from Windows/Platform SDKs...") + set(_WINDOWSSDK_IGNOREMSVC ON) + _winsdk_announce("Checking for tools from Windows/Platform SDKs...") else() - set(_WINDOWSSDK_IGNOREMSVC OFF) - _winsdk_announce("Checking for Windows/Platform SDKs...") + set(_WINDOWSSDK_IGNOREMSVC OFF) + _winsdk_announce("Checking for Windows/Platform SDKs...") endif() # Appends to the three main pre-output lists used only if the path exists # and is not already in the list. function(_winsdk_conditional_append _vername _build _path) - if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}")) - # Path invalid - do not add - return() - endif() - list(FIND _win_sdk_dirs "${_path}" _win_sdk_idx) - if(_win_sdk_idx GREATER -1) - # Path already in list - do not add - return() - endif() - _winsdk_announce( " - ${_vername}, Build ${_build} @ ${_path}") - # Not yet in the list, so we'll add it - list(APPEND _win_sdk_dirs "${_path}") - set(_win_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE) - list(APPEND - _win_sdk_versanddirs - "${_vername}" - "${_path}") - set(_win_sdk_versanddirs "${_win_sdk_versanddirs}" CACHE INTERNAL "" FORCE) - list(APPEND - _win_sdk_buildsanddirs - "${_build}" - "${_path}") - set(_win_sdk_buildsanddirs "${_win_sdk_buildsanddirs}" CACHE INTERNAL "" FORCE) + if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}")) + # Path invalid - do not add + return() + endif() + list(FIND _win_sdk_dirs "${_path}" _win_sdk_idx) + if(_win_sdk_idx GREATER -1) + # Path already in list - do not add + return() + endif() + _winsdk_announce(" - ${_vername}, Build ${_build} @ ${_path}") + # Not yet in the list, so we'll add it + list(APPEND _win_sdk_dirs "${_path}") + set(_win_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE) + list(APPEND _win_sdk_versanddirs "${_vername}" "${_path}") + set(_win_sdk_versanddirs "${_win_sdk_versanddirs}" CACHE INTERNAL "" FORCE) + list(APPEND _win_sdk_buildsanddirs "${_build}" "${_path}") + set(_win_sdk_buildsanddirs "${_win_sdk_buildsanddirs}" CACHE INTERNAL "" FORCE) endfunction() # Appends to the "preferred SDK" lists only if the path exists function(_winsdk_conditional_append_preferred _info _path) - if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}")) - # Path invalid - do not add - return() - endif() + if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}")) + # Path invalid - do not add + return() + endif() - get_filename_component(_path "${_path}" ABSOLUTE) + get_filename_component(_path "${_path}" ABSOLUTE) - list(FIND _win_sdk_preferred_sdk_dirs "${_path}" _win_sdk_idx) - if(_win_sdk_idx GREATER -1) - # Path already in list - do not add - return() - endif() - _winsdk_announce( " - Found \"preferred\" SDK ${_info} @ ${_path}") - # Not yet in the list, so we'll add it - list(APPEND _win_sdk_preferred_sdk_dirs "${_path}") - set(_win_sdk_preferred_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE) + list(FIND _win_sdk_preferred_sdk_dirs "${_path}" _win_sdk_idx) + if(_win_sdk_idx GREATER -1) + # Path already in list - do not add + return() + endif() + _winsdk_announce(" - Found \"preferred\" SDK ${_info} @ ${_path}") + # Not yet in the list, so we'll add it + list(APPEND _win_sdk_preferred_sdk_dirs "${_path}") + set(_win_sdk_preferred_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE) - # Just in case we somehow missed it: - _winsdk_conditional_append("${_info}" "" "${_path}") + # Just in case we somehow missed it: + _winsdk_conditional_append("${_info}" "" "${_path}") endfunction() # Given a version like v7.0A, looks for an SDK in the registry under "Microsoft SDKs". @@ -163,43 +157,37 @@ endfunction() # # Pass a "default" build number as an extra argument in case we can't find it. function(_winsdk_check_microsoft_sdks_registry _winsdkver) - set(SDKKEY "HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows\\${_winsdkver}") - get_filename_component(_sdkdir - "[${SDKKEY};InstallationFolder]" - ABSOLUTE) + set(SDKKEY "HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows\\${_winsdkver}") + get_filename_component(_sdkdir "[${SDKKEY};InstallationFolder]" ABSOLUTE) - set(_sdkname "Windows SDK ${_winsdkver}") + set(_sdkname "Windows SDK ${_winsdkver}") - # Default build number passed as extra argument - set(_build ${ARGN}) - # See if the registry holds a Microsoft-mutilated, err, designated, product name - # (just using get_filename_component to execute the registry lookup) - get_filename_component(_sdkproductname - "[${SDKKEY};ProductName]" - NAME) - if(NOT "${_sdkproductname}" MATCHES "registry") - # Got a product name - set(_sdkname "${_sdkname} (${_sdkproductname})") - endif() + # Default build number passed as extra argument + set(_build ${ARGN}) + # See if the registry holds a Microsoft-mutilated, err, designated, product name + # (just using get_filename_component to execute the registry lookup) + get_filename_component(_sdkproductname "[${SDKKEY};ProductName]" NAME) + if(NOT "${_sdkproductname}" MATCHES "registry") + # Got a product name + set(_sdkname "${_sdkname} (${_sdkproductname})") + endif() - # try for a version to augment our name - # (just using get_filename_component to execute the registry lookup) - get_filename_component(_sdkver - "[${SDKKEY};ProductVersion]" - NAME) - if(NOT "${_sdkver}" MATCHES "registry" AND NOT MATCHES) - # Got a version - if(NOT "${_sdkver}" MATCHES "\\.\\.") - # and it's not an invalid one with two dots in it: - # use to override the default build - set(_build ${_sdkver}) - if(NOT "${_sdkname}" MATCHES "${_sdkver}") - # Got a version that's not already in the name, let's use it to improve our name. - set(_sdkname "${_sdkname} (${_sdkver})") - endif() - endif() - endif() - _winsdk_conditional_append("${_sdkname}" "${_build}" "${_sdkdir}") + # try for a version to augment our name + # (just using get_filename_component to execute the registry lookup) + get_filename_component(_sdkver "[${SDKKEY};ProductVersion]" NAME) + if(NOT "${_sdkver}" MATCHES "registry" AND NOT MATCHES) + # Got a version + if(NOT "${_sdkver}" MATCHES "\\.\\.") + # and it's not an invalid one with two dots in it: + # use to override the default build + set(_build ${_sdkver}) + if(NOT "${_sdkname}" MATCHES "${_sdkver}") + # Got a version that's not already in the name, let's use it to improve our name. + set(_sdkname "${_sdkname} (${_sdkver})") + endif() + endif() + endif() + _winsdk_conditional_append("${_sdkname}" "${_build}" "${_sdkdir}") endfunction() # Given a name for identification purposes, the build number, and a key (technically a "value name") @@ -211,10 +199,12 @@ endfunction() # sometimes you get keys in both parts of the registry (in the wow64 portion especially), # and the non-"Windows Kits" location is often more descriptive. function(_winsdk_check_windows_kits_registry _winkit_name _winkit_build _winkit_key) - get_filename_component(_sdkdir - "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;${_winkit_key}]" - ABSOLUTE) - _winsdk_conditional_append("${_winkit_name}" "${_winkit_build}" "${_sdkdir}") + get_filename_component( + _sdkdir + "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;${_winkit_key}]" + ABSOLUTE + ) + _winsdk_conditional_append("${_winkit_name}" "${_winkit_build}" "${_sdkdir}") endfunction() # Given a name for identification purposes and the build number @@ -224,27 +214,31 @@ endfunction() # sometimes you get keys in both parts of the registry (in the wow64 portion especially), # and the non-"Windows Kits" location is often more descriptive. function(_winsdk_check_win10_kits _winkit_build) - get_filename_component(_sdkdir - "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;KitsRoot10]" - ABSOLUTE) - if(("${_sdkdir}" MATCHES "registry") OR (NOT EXISTS "${_sdkdir}")) - return() # not found - endif() - if(EXISTS "${_sdkdir}/Include/${_winkit_build}/um") - _winsdk_conditional_append("Windows Kits 10 (Build ${_winkit_build})" "${_winkit_build}" "${_sdkdir}") - endif() + get_filename_component( + _sdkdir + "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;KitsRoot10]" + ABSOLUTE + ) + if(("${_sdkdir}" MATCHES "registry") OR (NOT EXISTS "${_sdkdir}")) + return() # not found + endif() + if(EXISTS "${_sdkdir}/Include/${_winkit_build}/um") + _winsdk_conditional_append("Windows Kits 10 (Build ${_winkit_build})" "${_winkit_build}" "${_sdkdir}") + endif() endfunction() # Given a name for identification purposes, the build number, and the associated package GUID, # look in the registry under both HKLM and HKCU in \\SOFTWARE\\Microsoft\\MicrosoftSDK\\InstalledSDKs\\ # for that guid and the SDK it points to. function(_winsdk_check_platformsdk_registry _platformsdkname _build _platformsdkguid) - foreach(_winsdk_hive HKEY_LOCAL_MACHINE HKEY_CURRENT_USER) - get_filename_component(_sdkdir - "[${_winsdk_hive}\\SOFTWARE\\Microsoft\\MicrosoftSDK\\InstalledSDKs\\${_platformsdkguid};Install Dir]" - ABSOLUTE) - _winsdk_conditional_append("${_platformsdkname} (${_build})" "${_build}" "${_sdkdir}") - endforeach() + foreach(_winsdk_hive HKEY_LOCAL_MACHINE HKEY_CURRENT_USER) + get_filename_component( + _sdkdir + "[${_winsdk_hive}\\SOFTWARE\\Microsoft\\MicrosoftSDK\\InstalledSDKs\\${_platformsdkguid};Install Dir]" + ABSOLUTE + ) + _winsdk_conditional_append("${_platformsdkname} (${_build})" "${_build}" "${_sdkdir}") + endforeach() endfunction() ### @@ -252,25 +246,28 @@ endfunction() ### set(_winsdk_vistaonly_ok OFF) if(MSVC AND NOT _WINDOWSSDK_IGNOREMSVC) - # VC 10 and older has broad target support - if(MSVC_VERSION LESS 1700) - # VC 11 by default targets Vista and later only, so we can add a few more SDKs that (might?) only work on vista+ - elseif("${CMAKE_VS_PLATFORM_TOOLSET}" MATCHES "_xp") - # This is the XP-compatible v110+ toolset - elseif("${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v100" OR "${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v90") - # This is the VS2010/VS2008 toolset - else() - # OK, we're VC11 or newer and not using a backlevel or XP-compatible toolset. - # These versions have no XP (and possibly Vista pre-SP1) support - set(_winsdk_vistaonly_ok ON) - if(_WINDOWSSDK_ANNOUNCE AND NOT _WINDOWSSDK_VISTAONLY_PESTERED) - set(_WINDOWSSDK_VISTAONLY_PESTERED ON CACHE INTERNAL "" FORCE) - message(STATUS "FindWindowsSDK: Detected Visual Studio 2012 or newer, not using the _xp toolset variant: including SDK versions that drop XP support in search!") - endif() - endif() + # VC 10 and older has broad target support + if(MSVC_VERSION LESS 1700) + # VC 11 by default targets Vista and later only, so we can add a few more SDKs that (might?) only work on vista+ + elseif("${CMAKE_VS_PLATFORM_TOOLSET}" MATCHES "_xp") + # This is the XP-compatible v110+ toolset + elseif("${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v100" OR "${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v90") + # This is the VS2010/VS2008 toolset + else() + # OK, we're VC11 or newer and not using a backlevel or XP-compatible toolset. + # These versions have no XP (and possibly Vista pre-SP1) support + set(_winsdk_vistaonly_ok ON) + if(_WINDOWSSDK_ANNOUNCE AND NOT _WINDOWSSDK_VISTAONLY_PESTERED) + set(_WINDOWSSDK_VISTAONLY_PESTERED ON CACHE INTERNAL "" FORCE) + message( + STATUS + "FindWindowsSDK: Detected Visual Studio 2012 or newer, not using the _xp toolset variant: including SDK versions that drop XP support in search!" + ) + endif() + endif() endif() if(_WINDOWSSDK_IGNOREMSVC) - set(_winsdk_vistaonly_ok ON) + set(_winsdk_vistaonly_ok ON) endif() ### @@ -279,365 +276,387 @@ endif() ### set(_winsdk_msvc_greater_1200 OFF) if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION GREATER 1200))) - set(_winsdk_msvc_greater_1200 ON) + set(_winsdk_msvc_greater_1200 ON) endif() # Newer than VS .NET/VS Toolkit 2003 set(_winsdk_msvc_greater_1310 OFF) if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION GREATER 1310))) - set(_winsdk_msvc_greater_1310 ON) + set(_winsdk_msvc_greater_1310 ON) endif() # VS2005/2008 set(_winsdk_msvc_less_1600 OFF) if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION LESS 1600))) - set(_winsdk_msvc_less_1600 ON) + set(_winsdk_msvc_less_1600 ON) endif() # VS2013+ set(_winsdk_msvc_not_less_1800 OFF) if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (NOT MSVC_VERSION LESS 1800))) - set(_winsdk_msvc_not_less_1800 ON) + set(_winsdk_msvc_not_less_1800 ON) endif() ### # START body of find module ### if(_winsdk_msvc_greater_1310) # Newer than VS .NET/VS Toolkit 2003 - ### - # Look for "preferred" SDKs - ### + ### + # Look for "preferred" SDKs + ### - # Environment variable for SDK dir - if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL "")) - _winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}") - endif() + # Environment variable for SDK dir + if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL "")) + _winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}") + endif() - if(_winsdk_msvc_less_1600) - # Per-user current Windows SDK for VS2005/2008 - get_filename_component(_sdkdir - "[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" - ABSOLUTE) - _winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}") + if(_winsdk_msvc_less_1600) + # Per-user current Windows SDK for VS2005/2008 + get_filename_component( + _sdkdir + "[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" + ABSOLUTE + ) + _winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}") - # System-wide current Windows SDK for VS2005/2008 - get_filename_component(_sdkdir - "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" - ABSOLUTE) - _winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}") - endif() + # System-wide current Windows SDK for VS2005/2008 + get_filename_component( + _sdkdir + "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" + ABSOLUTE + ) + _winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}") + endif() - ### - # Begin the massive list of SDK searching! - ### - if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800) - # These require at least Visual Studio 2013 (VC12) + ### + # Begin the massive list of SDK searching! + ### + if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800) + # These require at least Visual Studio 2013 (VC12) - _winsdk_check_microsoft_sdks_registry(v10.0A) + _winsdk_check_microsoft_sdks_registry(v10.0A) - # Windows Software Development Kit (SDK) for Windows 10 - # Several different versions living in the same directory - if nothing else we can assume RTM (10240) - _winsdk_check_microsoft_sdks_registry(v10.0 10.0.10240.0) - foreach(_win10build ${_winsdk_win10vers}) - _winsdk_check_win10_kits(${_win10build}) - endforeach() - endif() # vista-only and 2013+ + # Windows Software Development Kit (SDK) for Windows 10 + # Several different versions living in the same directory - if nothing else we can assume RTM (10240) + _winsdk_check_microsoft_sdks_registry(v10.0 10.0.10240.0) + foreach(_win10build ${_winsdk_win10vers}) + _winsdk_check_win10_kits(${_win10build}) + endforeach() + endif() # vista-only and 2013+ - # Included in Visual Studio 2013 - # Includes the v120_xp toolset - _winsdk_check_microsoft_sdks_registry(v8.1A 8.1.51636) + # Included in Visual Studio 2013 + # Includes the v120_xp toolset + _winsdk_check_microsoft_sdks_registry(v8.1A 8.1.51636) - if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800) - # Windows Software Development Kit (SDK) for Windows 8.1 - # http://msdn.microsoft.com/en-gb/windows/desktop/bg162891 - _winsdk_check_microsoft_sdks_registry(v8.1 8.1.25984.0) - _winsdk_check_windows_kits_registry("Windows Kits 8.1" 8.1.25984.0 KitsRoot81) - endif() # vista-only and 2013+ + if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800) + # Windows Software Development Kit (SDK) for Windows 8.1 + # http://msdn.microsoft.com/en-gb/windows/desktop/bg162891 + _winsdk_check_microsoft_sdks_registry(v8.1 8.1.25984.0) + _winsdk_check_windows_kits_registry("Windows Kits 8.1" 8.1.25984.0 KitsRoot81) + endif() # vista-only and 2013+ - if(_winsdk_vistaonly_ok) - # Included in Visual Studio 2012 - _winsdk_check_microsoft_sdks_registry(v8.0A 8.0.50727) + if(_winsdk_vistaonly_ok) + # Included in Visual Studio 2012 + _winsdk_check_microsoft_sdks_registry(v8.0A 8.0.50727) - # Microsoft Windows SDK for Windows 8 and .NET Framework 4.5 - # This is the first version to also include the DirectX SDK - # http://msdn.microsoft.com/en-US/windows/desktop/hh852363.aspx - _winsdk_check_microsoft_sdks_registry(v8.0 6.2.9200.16384) - _winsdk_check_windows_kits_registry("Windows Kits 8.0" 6.2.9200.16384 KitsRoot) - endif() # vista-only + # Microsoft Windows SDK for Windows 8 and .NET Framework 4.5 + # This is the first version to also include the DirectX SDK + # http://msdn.microsoft.com/en-US/windows/desktop/hh852363.aspx + _winsdk_check_microsoft_sdks_registry(v8.0 6.2.9200.16384) + _winsdk_check_windows_kits_registry("Windows Kits 8.0" 6.2.9200.16384 KitsRoot) + endif() # vista-only - # Included with VS 2012 Update 1 or later - # Introduces v110_xp toolset - _winsdk_check_microsoft_sdks_registry(v7.1A 7.1.51106) - if(_winsdk_vistaonly_ok) - # Microsoft Windows SDK for Windows 7 and .NET Framework 4 - # http://www.microsoft.com/downloads/en/details.aspx?FamilyID=6b6c21d2-2006-4afa-9702-529fa782d63b - _winsdk_check_microsoft_sdks_registry(v7.1 7.1.7600.0.30514) - endif() # vista-only + # Included with VS 2012 Update 1 or later + # Introduces v110_xp toolset + _winsdk_check_microsoft_sdks_registry(v7.1A 7.1.51106) + if(_winsdk_vistaonly_ok) + # Microsoft Windows SDK for Windows 7 and .NET Framework 4 + # http://www.microsoft.com/downloads/en/details.aspx?FamilyID=6b6c21d2-2006-4afa-9702-529fa782d63b + _winsdk_check_microsoft_sdks_registry(v7.1 7.1.7600.0.30514) + endif() # vista-only - # Included with VS 2010 - _winsdk_check_microsoft_sdks_registry(v7.0A 6.1.7600.16385) + # Included with VS 2010 + _winsdk_check_microsoft_sdks_registry(v7.0A 6.1.7600.16385) - # Windows SDK for Windows 7 and .NET Framework 3.5 SP1 - # Works with VC9 - # http://www.microsoft.com/en-us/download/details.aspx?id=18950 - _winsdk_check_microsoft_sdks_registry(v7.0 6.1.7600.16385) + # Windows SDK for Windows 7 and .NET Framework 3.5 SP1 + # Works with VC9 + # http://www.microsoft.com/en-us/download/details.aspx?id=18950 + _winsdk_check_microsoft_sdks_registry(v7.0 6.1.7600.16385) - # Two versions call themselves "v6.1": - # Older: - # Windows Vista Update & .NET 3.0 SDK - # http://www.microsoft.com/en-us/download/details.aspx?id=14477 + # Two versions call themselves "v6.1": + # Older: + # Windows Vista Update & .NET 3.0 SDK + # http://www.microsoft.com/en-us/download/details.aspx?id=14477 - # Newer: - # Windows Server 2008 & .NET 3.5 SDK - # may have broken VS9SP1? they recommend v7.0 instead, or a KB... - # http://www.microsoft.com/en-us/download/details.aspx?id=24826 - _winsdk_check_microsoft_sdks_registry(v6.1 6.1.6000.16384.10) + # Newer: + # Windows Server 2008 & .NET 3.5 SDK + # may have broken VS9SP1? they recommend v7.0 instead, or a KB... + # http://www.microsoft.com/en-us/download/details.aspx?id=24826 + _winsdk_check_microsoft_sdks_registry(v6.1 6.1.6000.16384.10) - # Included in VS 2008 - _winsdk_check_microsoft_sdks_registry(v6.0A 6.1.6723.1) + # Included in VS 2008 + _winsdk_check_microsoft_sdks_registry(v6.0A 6.1.6723.1) - # Microsoft Windows Software Development Kit for Windows Vista and .NET Framework 3.0 Runtime Components - # http://blogs.msdn.com/b/stanley/archive/2006/11/08/microsoft-windows-software-development-kit-for-windows-vista-and-net-framework-3-0-runtime-components.aspx - _winsdk_check_microsoft_sdks_registry(v6.0 6.0.6000.16384) + # Microsoft Windows Software Development Kit for Windows Vista and .NET Framework 3.0 Runtime Components + # http://blogs.msdn.com/b/stanley/archive/2006/11/08/microsoft-windows-software-development-kit-for-windows-vista-and-net-framework-3-0-runtime-components.aspx + _winsdk_check_microsoft_sdks_registry(v6.0 6.0.6000.16384) endif() # Let's not forget the Platform SDKs, which sometimes are useful! if(_winsdk_msvc_greater_1200) - _winsdk_check_platformsdk_registry("Microsoft Platform SDK for Windows Server 2003 R2" "5.2.3790.2075.51" "D2FF9F89-8AA2-4373-8A31-C838BF4DBBE1") - _winsdk_check_platformsdk_registry("Microsoft Platform SDK for Windows Server 2003 SP1" "5.2.3790.1830.15" "8F9E5EF3-A9A5-491B-A889-C58EFFECE8B3") + _winsdk_check_platformsdk_registry( + "Microsoft Platform SDK for Windows Server 2003 R2" + "5.2.3790.2075.51" + "D2FF9F89-8AA2-4373-8A31-C838BF4DBBE1" + ) + _winsdk_check_platformsdk_registry( + "Microsoft Platform SDK for Windows Server 2003 SP1" + "5.2.3790.1830.15" + "8F9E5EF3-A9A5-491B-A889-C58EFFECE8B3" + ) endif() ### # Finally, look for "preferred" SDKs ### if(_winsdk_msvc_greater_1310) # Newer than VS .NET/VS Toolkit 2003 + # Environment variable for SDK dir + if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL "")) + _winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}") + endif() + if(_winsdk_msvc_less_1600) + # Per-user current Windows SDK for VS2005/2008 + get_filename_component( + _sdkdir + "[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" + ABSOLUTE + ) + _winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}") - # Environment variable for SDK dir - if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL "")) - _winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}") - endif() - - if(_winsdk_msvc_less_1600) - # Per-user current Windows SDK for VS2005/2008 - get_filename_component(_sdkdir - "[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" - ABSOLUTE) - _winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}") - - # System-wide current Windows SDK for VS2005/2008 - get_filename_component(_sdkdir - "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" - ABSOLUTE) - _winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}") - endif() + # System-wide current Windows SDK for VS2005/2008 + get_filename_component( + _sdkdir + "[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]" + ABSOLUTE + ) + _winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}") + endif() endif() - function(windowssdk_name_lookup _dir _outvar) - list(FIND _win_sdk_versanddirs "${_dir}" _diridx) - math(EXPR _idx "${_diridx} - 1") - if(${_idx} GREATER -1) - list(GET _win_sdk_versanddirs ${_idx} _ret) - else() - set(_ret "NOTFOUND") - endif() - set(${_outvar} "${_ret}" PARENT_SCOPE) + list(FIND _win_sdk_versanddirs "${_dir}" _diridx) + math(EXPR _idx "${_diridx} - 1") + if(${_idx} GREATER -1) + list(GET _win_sdk_versanddirs ${_idx} _ret) + else() + set(_ret "NOTFOUND") + endif() + set(${_outvar} "${_ret}" PARENT_SCOPE) endfunction() function(windowssdk_build_lookup _dir _outvar) - list(FIND _win_sdk_buildsanddirs "${_dir}" _diridx) - math(EXPR _idx "${_diridx} - 1") - if(${_idx} GREATER -1) - list(GET _win_sdk_buildsanddirs ${_idx} _ret) - else() - set(_ret "NOTFOUND") - endif() - set(${_outvar} "${_ret}" PARENT_SCOPE) + list(FIND _win_sdk_buildsanddirs "${_dir}" _diridx) + math(EXPR _idx "${_diridx} - 1") + if(${_idx} GREATER -1) + list(GET _win_sdk_buildsanddirs ${_idx} _ret) + else() + set(_ret "NOTFOUND") + endif() + set(${_outvar} "${_ret}" PARENT_SCOPE) endfunction() # If we found something... if(_win_sdk_dirs) - list(GET _win_sdk_dirs 0 WINDOWSSDK_LATEST_DIR) - windowssdk_name_lookup("${WINDOWSSDK_LATEST_DIR}" - WINDOWSSDK_LATEST_NAME) - set(WINDOWSSDK_DIRS ${_win_sdk_dirs}) + list(GET _win_sdk_dirs 0 WINDOWSSDK_LATEST_DIR) + windowssdk_name_lookup("${WINDOWSSDK_LATEST_DIR}" WINDOWSSDK_LATEST_NAME) + set(WINDOWSSDK_DIRS ${_win_sdk_dirs}) - # Fallback, in case no preference found. - set(WINDOWSSDK_PREFERRED_DIR "${WINDOWSSDK_LATEST_DIR}") - set(WINDOWSSDK_PREFERRED_NAME "${WINDOWSSDK_LATEST_NAME}") - set(WINDOWSSDK_PREFERRED_FIRST_DIRS ${WINDOWSSDK_DIRS}) - set(WINDOWSSDK_FOUND_PREFERENCE OFF) + # Fallback, in case no preference found. + set(WINDOWSSDK_PREFERRED_DIR "${WINDOWSSDK_LATEST_DIR}") + set(WINDOWSSDK_PREFERRED_NAME "${WINDOWSSDK_LATEST_NAME}") + set(WINDOWSSDK_PREFERRED_FIRST_DIRS ${WINDOWSSDK_DIRS}) + set(WINDOWSSDK_FOUND_PREFERENCE OFF) endif() # If we found indications of a user preference... if(_win_sdk_preferred_sdk_dirs) - list(GET _win_sdk_preferred_sdk_dirs 0 WINDOWSSDK_PREFERRED_DIR) - windowssdk_name_lookup("${WINDOWSSDK_PREFERRED_DIR}" - WINDOWSSDK_PREFERRED_NAME) - set(WINDOWSSDK_PREFERRED_FIRST_DIRS - ${_win_sdk_preferred_sdk_dirs} - ${_win_sdk_dirs}) - list(REMOVE_DUPLICATES WINDOWSSDK_PREFERRED_FIRST_DIRS) - set(WINDOWSSDK_FOUND_PREFERENCE ON) + list(GET _win_sdk_preferred_sdk_dirs 0 WINDOWSSDK_PREFERRED_DIR) + windowssdk_name_lookup("${WINDOWSSDK_PREFERRED_DIR}" WINDOWSSDK_PREFERRED_NAME) + set(WINDOWSSDK_PREFERRED_FIRST_DIRS ${_win_sdk_preferred_sdk_dirs} ${_win_sdk_dirs}) + list(REMOVE_DUPLICATES WINDOWSSDK_PREFERRED_FIRST_DIRS) + set(WINDOWSSDK_FOUND_PREFERENCE ON) endif() include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(WindowsSDK - "No compatible version of the Windows SDK or Platform SDK found." - WINDOWSSDK_DIRS) +find_package_handle_standard_args( + WindowsSDK + "No compatible version of the Windows SDK or Platform SDK found." + WINDOWSSDK_DIRS +) if(WINDOWSSDK_FOUND) - # Internal: Architecture-appropriate library directory names. - if("${CMAKE_VS_PLATFORM_NAME}" STREQUAL "ARM") - if(CMAKE_SIZEOF_VOID_P MATCHES "8") - # Only supported in Win10 SDK and up. - set(_winsdk_arch8 arm64) # what the WDK for Win8+ calls this architecture - else() - set(_winsdk_archbare /arm) # what the architecture used to be called in oldest SDKs - set(_winsdk_arch arm) # what the architecture used to be called - set(_winsdk_arch8 arm) # what the WDK for Win8+ calls this architecture - endif() - else() - if(CMAKE_SIZEOF_VOID_P MATCHES "8") - set(_winsdk_archbare /x64) # what the architecture used to be called in oldest SDKs - set(_winsdk_arch amd64) # what the architecture used to be called - set(_winsdk_arch8 x64) # what the WDK for Win8+ calls this architecture - else() - set(_winsdk_archbare ) # what the architecture used to be called in oldest SDKs - set(_winsdk_arch i386) # what the architecture used to be called - set(_winsdk_arch8 x86) # what the WDK for Win8+ calls this architecture - endif() - endif() + # Internal: Architecture-appropriate library directory names. + if("${CMAKE_VS_PLATFORM_NAME}" STREQUAL "ARM") + if(CMAKE_SIZEOF_VOID_P MATCHES "8") + # Only supported in Win10 SDK and up. + set(_winsdk_arch8 arm64) # what the WDK for Win8+ calls this architecture + else() + set(_winsdk_archbare /arm) # what the architecture used to be called in oldest SDKs + set(_winsdk_arch arm) # what the architecture used to be called + set(_winsdk_arch8 arm) # what the WDK for Win8+ calls this architecture + endif() + else() + if(CMAKE_SIZEOF_VOID_P MATCHES "8") + set(_winsdk_archbare /x64) # what the architecture used to be called in oldest SDKs + set(_winsdk_arch amd64) # what the architecture used to be called + set(_winsdk_arch8 x64) # what the WDK for Win8+ calls this architecture + else() + set(_winsdk_archbare) # what the architecture used to be called in oldest SDKs + set(_winsdk_arch i386) # what the architecture used to be called + set(_winsdk_arch8 x86) # what the WDK for Win8+ calls this architecture + endif() + endif() - function(get_windowssdk_from_component _component _var) - get_filename_component(_component "${_component}" ABSOLUTE) - file(TO_CMAKE_PATH "${_component}" _component) - foreach(_sdkdir ${WINDOWSSDK_DIRS}) - get_filename_component(_sdkdir "${_sdkdir}" ABSOLUTE) - string(LENGTH "${_sdkdir}" _sdklen) - file(RELATIVE_PATH _rel "${_sdkdir}" "${_component}") - # If we don't have any "parent directory" items... - if(NOT "${_rel}" MATCHES "[.][.]") - set(${_var} "${_sdkdir}" PARENT_SCOPE) - return() - endif() - endforeach() - # Fail. - set(${_var} "NOTFOUND" PARENT_SCOPE) - endfunction() - function(get_windowssdk_library_dirs _winsdk_dir _var) - set(_dirs) - set(_suffixes - "lib${_winsdk_archbare}" # SDKs like 7.1A - "lib/${_winsdk_arch}" # just because some SDKs have x86 dir and root dir - "lib/w2k/${_winsdk_arch}" # Win2k min requirement - "lib/wxp/${_winsdk_arch}" # WinXP min requirement - "lib/wnet/${_winsdk_arch}" # Win Server 2003 min requirement - "lib/wlh/${_winsdk_arch}" - "lib/wlh/um/${_winsdk_arch8}" # Win Vista ("Long Horn") min requirement - "lib/win7/${_winsdk_arch}" - "lib/win7/um/${_winsdk_arch8}" # Win 7 min requirement - ) - foreach(_ver - wlh # Win Vista ("Long Horn") min requirement - win7 # Win 7 min requirement - win8 # Win 8 min requirement - winv6.3 # Win 8.1 min requirement - ) + function(get_windowssdk_from_component _component _var) + get_filename_component(_component "${_component}" ABSOLUTE) + file(TO_CMAKE_PATH "${_component}" _component) + foreach(_sdkdir ${WINDOWSSDK_DIRS}) + get_filename_component(_sdkdir "${_sdkdir}" ABSOLUTE) + string(LENGTH "${_sdkdir}" _sdklen) + file(RELATIVE_PATH _rel "${_sdkdir}" "${_component}") + # If we don't have any "parent directory" items... + if(NOT "${_rel}" MATCHES "[.][.]") + set(${_var} "${_sdkdir}" PARENT_SCOPE) + return() + endif() + endforeach() + # Fail. + set(${_var} "NOTFOUND" PARENT_SCOPE) + endfunction() + function(get_windowssdk_library_dirs _winsdk_dir _var) + set(_dirs) + set( + _suffixes + "lib${_winsdk_archbare}" # SDKs like 7.1A + "lib/${_winsdk_arch}" # just because some SDKs have x86 dir and root dir + "lib/w2k/${_winsdk_arch}" # Win2k min requirement + "lib/wxp/${_winsdk_arch}" # WinXP min requirement + "lib/wnet/${_winsdk_arch}" # Win Server 2003 min requirement + "lib/wlh/${_winsdk_arch}" + "lib/wlh/um/${_winsdk_arch8}" # Win Vista ("Long Horn") min requirement + "lib/win7/${_winsdk_arch}" + "lib/win7/um/${_winsdk_arch8}" # Win 7 min requirement + ) + foreach( + _ver + wlh # Win Vista ("Long Horn") min requirement + win7 # Win 7 min requirement + win8 # Win 8 min requirement + winv6.3 # Win 8.1 min requirement + ) + list( + APPEND _suffixes + "lib/${_ver}/${_winsdk_arch}" + "lib/${_ver}/um/${_winsdk_arch8}" + "lib/${_ver}/km/${_winsdk_arch8}" + ) + endforeach() - list(APPEND _suffixes - "lib/${_ver}/${_winsdk_arch}" - "lib/${_ver}/um/${_winsdk_arch8}" - "lib/${_ver}/km/${_winsdk_arch8}" - ) - endforeach() + # Look for WDF libraries in Win10+ SDK + foreach(_mode umdf kmdf) + file(GLOB _wdfdirs RELATIVE "${_winsdk_dir}" "${_winsdk_dir}/lib/wdf/${_mode}/${_winsdk_arch8}/*") + if(_wdfdirs) + list(APPEND _suffixes ${_wdfdirs}) + endif() + endforeach() - # Look for WDF libraries in Win10+ SDK - foreach(_mode umdf kmdf) - file(GLOB _wdfdirs RELATIVE "${_winsdk_dir}" "${_winsdk_dir}/lib/wdf/${_mode}/${_winsdk_arch8}/*") - if(_wdfdirs) - list(APPEND _suffixes ${_wdfdirs}) - endif() - endforeach() + # Look in each Win10+ SDK version for the components + foreach(_win10ver ${_winsdk_win10vers}) + foreach(_component um km ucrt mmos) + list(APPEND _suffixes "lib/${_win10ver}/${_component}/${_winsdk_arch8}") + endforeach() + endforeach() - # Look in each Win10+ SDK version for the components - foreach(_win10ver ${_winsdk_win10vers}) - foreach(_component um km ucrt mmos) - list(APPEND _suffixes "lib/${_win10ver}/${_component}/${_winsdk_arch8}") - endforeach() - endforeach() + foreach(_suffix ${_suffixes}) + # Check to see if a library actually exists here. + file(GLOB _libs "${_winsdk_dir}/${_suffix}/*.lib") + if(_libs) + list(APPEND _dirs "${_winsdk_dir}/${_suffix}") + endif() + endforeach() + if("${_dirs}" STREQUAL "") + set(_dirs NOTFOUND) + else() + list(REMOVE_DUPLICATES _dirs) + endif() + set(${_var} ${_dirs} PARENT_SCOPE) + endfunction() + function(get_windowssdk_include_dirs _winsdk_dir _var) + set(_dirs) - foreach(_suffix ${_suffixes}) - # Check to see if a library actually exists here. - file(GLOB _libs "${_winsdk_dir}/${_suffix}/*.lib") - if(_libs) - list(APPEND _dirs "${_winsdk_dir}/${_suffix}") - endif() - endforeach() - if("${_dirs}" STREQUAL "") - set(_dirs NOTFOUND) - else() - list(REMOVE_DUPLICATES _dirs) - endif() - set(${_var} ${_dirs} PARENT_SCOPE) - endfunction() - function(get_windowssdk_include_dirs _winsdk_dir _var) - set(_dirs) + set( + _subdirs + shared + um + winrt + km + wdf + mmos + ucrt + ) + set(_suffixes Include) - set(_subdirs shared um winrt km wdf mmos ucrt) - set(_suffixes Include) + foreach(_dir ${_subdirs}) + list(APPEND _suffixes "Include/${_dir}") + endforeach() - foreach(_dir ${_subdirs}) - list(APPEND _suffixes "Include/${_dir}") - endforeach() + foreach(_ver ${_winsdk_win10vers}) + foreach(_dir ${_subdirs}) + list(APPEND _suffixes "Include/${_ver}/${_dir}") + endforeach() + endforeach() - foreach(_ver ${_winsdk_win10vers}) - foreach(_dir ${_subdirs}) - list(APPEND _suffixes "Include/${_ver}/${_dir}") - endforeach() - endforeach() - - foreach(_suffix ${_suffixes}) - # Check to see if a header file actually exists here. - file(GLOB _headers "${_winsdk_dir}/${_suffix}/*.h") - if(_headers) - list(APPEND _dirs "${_winsdk_dir}/${_suffix}") - endif() - endforeach() - if("${_dirs}" STREQUAL "") - set(_dirs NOTFOUND) - else() - list(REMOVE_DUPLICATES _dirs) - endif() - set(${_var} ${_dirs} PARENT_SCOPE) - endfunction() - function(get_windowssdk_library_dirs_multiple _var) - set(_dirs) - foreach(_sdkdir ${ARGN}) - get_windowssdk_library_dirs("${_sdkdir}" _current_sdk_libdirs) - if(_current_sdk_libdirs) - list(APPEND _dirs ${_current_sdk_libdirs}) - endif() - endforeach() - if("${_dirs}" STREQUAL "") - set(_dirs NOTFOUND) - else() - list(REMOVE_DUPLICATES _dirs) - endif() - set(${_var} ${_dirs} PARENT_SCOPE) - endfunction() - function(get_windowssdk_include_dirs_multiple _var) - set(_dirs) - foreach(_sdkdir ${ARGN}) - get_windowssdk_include_dirs("${_sdkdir}" _current_sdk_incdirs) - if(_current_sdk_libdirs) - list(APPEND _dirs ${_current_sdk_incdirs}) - endif() - endforeach() - if("${_dirs}" STREQUAL "") - set(_dirs NOTFOUND) - else() - list(REMOVE_DUPLICATES _dirs) - endif() - set(${_var} ${_dirs} PARENT_SCOPE) - endfunction() + foreach(_suffix ${_suffixes}) + # Check to see if a header file actually exists here. + file(GLOB _headers "${_winsdk_dir}/${_suffix}/*.h") + if(_headers) + list(APPEND _dirs "${_winsdk_dir}/${_suffix}") + endif() + endforeach() + if("${_dirs}" STREQUAL "") + set(_dirs NOTFOUND) + else() + list(REMOVE_DUPLICATES _dirs) + endif() + set(${_var} ${_dirs} PARENT_SCOPE) + endfunction() + function(get_windowssdk_library_dirs_multiple _var) + set(_dirs) + foreach(_sdkdir ${ARGN}) + get_windowssdk_library_dirs("${_sdkdir}" _current_sdk_libdirs) + if(_current_sdk_libdirs) + list(APPEND _dirs ${_current_sdk_libdirs}) + endif() + endforeach() + if("${_dirs}" STREQUAL "") + set(_dirs NOTFOUND) + else() + list(REMOVE_DUPLICATES _dirs) + endif() + set(${_var} ${_dirs} PARENT_SCOPE) + endfunction() + function(get_windowssdk_include_dirs_multiple _var) + set(_dirs) + foreach(_sdkdir ${ARGN}) + get_windowssdk_include_dirs("${_sdkdir}" _current_sdk_incdirs) + if(_current_sdk_libdirs) + list(APPEND _dirs ${_current_sdk_incdirs}) + endif() + endforeach() + if("${_dirs}" STREQUAL "") + set(_dirs NOTFOUND) + else() + list(REMOVE_DUPLICATES _dirs) + endif() + set(${_var} ${_dirs} PARENT_SCOPE) + endfunction() endif() diff --git a/src/cmake/Modules/GetGitRevisionDescription.cmake b/src/cmake/Modules/GetGitRevisionDescription.cmake index 0b1ed5c570..f6fcaf8a94 100644 --- a/src/cmake/Modules/GetGitRevisionDescription.cmake +++ b/src/cmake/Modules/GetGitRevisionDescription.cmake @@ -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() diff --git a/src/cmake/Modules/GetGitRevisionDescription.cmake.in b/src/cmake/Modules/GetGitRevisionDescription.cmake.in index 9b8d207637..b2e52bddc2 100644 --- a/src/cmake/Modules/GetGitRevisionDescription.cmake.in +++ b/src/cmake/Modules/GetGitRevisionDescription.cmake.in @@ -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() diff --git a/src/cmake/Modules/README.md b/src/cmake/Modules/README.md index 4d50b70d46..3564f75aa6 100644 --- a/src/cmake/Modules/README.md +++ b/src/cmake/Modules/README.md @@ -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 +``` diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 2d21c3af49..913f167235 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -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 +) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 97c4edff84..0095beb6c8 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -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 +) diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index ced912152c..4d11e309fe 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -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) diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 6f55ee242a..b49ca7c0e4 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -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$, -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$, -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() diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index e6ea40b70c..1139337c87 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -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) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 1868773874..45e7f0cda8 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -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" +)