From 2a17a11f0e066d63158563ea9c5935c6ae335120 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 10 Dec 2020 00:50:35 +0000 Subject: [PATCH] CMake builds: set a default build type (Release) and document this In absence of a default build type, CMake would not use any pre-defined build configuration. As a consequence, any user running CMake without setting -DCMAKE_BUILD_TYPE would end up with builds without optimisation, and thus (surprisingly!) poor performance. The fix is copied from https://stackoverflow.com/questions/48832233/have-a-cmake-project-default-to-the-release-build-type. --- CMakeLists.txt | 7 +++++++ COMPILING.md | 3 ++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 21fb43623f0..38ad7ab671e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,12 @@ cmake_minimum_required(VERSION 3.2) +# Build a Release version by default (default build flags for each build type +# are configured below). +if (NOT EXISTS ${CMAKE_BINARY_DIR}/CMakeCache.txt) + if (NOT CMAKE_BUILD_TYPE) + set(CMAKE_BUILD_TYPE "Release" CACHE STRING "" FORCE) + endif() +endif() # Grab the current CBMC version from config.inc # We do this so we have a matching cbmc version between the Makefile build and diff --git a/COMPILING.md b/COMPILING.md index e4e5dece720..57a3b78eda5 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -266,7 +266,8 @@ require manual modification of build files. Generally it is not necessary to manually specify individual compiler or linker flags, as CMake defines a number of "build modes" including Debug and Release modes. To build in a particular mode, add the flag - `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation. + `-DCMAKE_BUILD_TYPE=Debug` (or `RelWithDebInfo`) to the initial invocation. + The default is to perform an optimized build via the `Release` configuration. If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and `-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's