diff --git a/.gitpod.yml b/.gitpod.yml index 600c1a8c8a..1b0aec7735 100644 --- a/.gitpod.yml +++ b/.gitpod.yml @@ -6,6 +6,6 @@ vscode: - leanprover.lean4 tasks: - - name: Release build - init: cmake --preset release + - name: Build + init: cmake --preset dev command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu) diff --git a/CMakePresets.json b/CMakePresets.json index f354144c15..9b140c9e1f 100644 --- a/CMakePresets.json +++ b/CMakePresets.json @@ -8,16 +8,26 @@ "configurePresets": [ { "name": "release", - "displayName": "Default development optimized build config", + "displayName": "Release build config", "generator": "Unix Makefiles", "binaryDir": "${sourceDir}/build/release" }, + { + "name": "dev", + "displayName": "Default development optimized build config", + "cacheVariables": { + "STRIP_BINARIES": "OFF" + }, + "generator": "Unix Makefiles", + "binaryDir": "${sourceDir}/build/dev" + }, { "name": "debug", "displayName": "Debug build config", "cacheVariables": { + "CMAKE_BUILD_TYPE": "Debug", "LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024", - "CMAKE_BUILD_TYPE": "Debug" + "STRIP_BINARIES": "OFF" }, "generator": "Unix Makefiles", "binaryDir": "${sourceDir}/build/debug" @@ -26,7 +36,8 @@ "name": "reldebug", "displayName": "Release with assertions enabled", "cacheVariables": { - "CMAKE_BUILD_TYPE": "RelWithAssert" + "CMAKE_BUILD_TYPE": "RelWithAssert", + "STRIP_BINARIES": "OFF" }, "generator": "Unix Makefiles", "binaryDir": "${sourceDir}/build/reldebug" @@ -38,6 +49,7 @@ "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024", "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined", "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime", + "STRIP_BINARIES": "OFF", "SMALL_ALLOCATOR": "OFF", "USE_MIMALLOC": "OFF", "BSYMBOLIC": "OFF", @@ -58,6 +70,10 @@ "name": "release", "configurePreset": "release" }, + { + "name": "dev", + "configurePreset": "dev" + }, { "name": "debug", "configurePreset": "debug" @@ -81,6 +97,11 @@ "configurePreset": "release", "output": {"outputOnFailure": true, "shortProgress": true} }, + { + "name": "dev", + "configurePreset": "dev", + "output": {"outputOnFailure": true, "shortProgress": true} + }, { "name": "debug", "configurePreset": "debug", diff --git a/doc/make/index.md b/doc/make/index.md index 7dd4f5dbd1..14e05e35f3 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -30,6 +30,9 @@ cd lean4 cmake --preset release make -C build/release -j$(nproc || sysctl -n hw.logicalcpu) ``` + +For development, `cmake --preset dev` is recommended instead. + You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount. The above commands will compile the Lean library and binaries into the diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dd9824bae7..c481e004fb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -80,6 +80,7 @@ option(CCACHE "use ccache" ON) option(SPLIT_STACK "SPLIT_STACK" OFF) # When OFF we disable LLVM support option(LLVM "LLVM" OFF) +option(STRIP_BINARIES "Strip produced binaries" ON) # When ON we include githash in the version string option(USE_GITHASH "GIT_HASH" ON) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index b399c745cf..40904462ad 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -162,7 +162,7 @@ else -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group -lInit -lStd -lLean -lleancpp -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} endif endif -ifeq "${CMAKE_BUILD_TYPE}" "Release" +ifeq "${STRIP_BINARIES}" "ON" ifeq "${CMAKE_SYSTEM_NAME}" "Linux" # We only strip like this on Linux for now as our other platforms already seem to exclude the # unexported symbols by default