diff --git a/bin/leanc.in b/bin/leanc.in index 788b205b11..8d18b74cd4 100644 --- a/bin/leanc.in +++ b/bin/leanc.in @@ -34,7 +34,7 @@ if [[ $use_c == yes ]]; then done [ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!" - $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument + @CMAKE_C_COMPILER_LAUNCHER@ $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument else # Check C++ compiler for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do @@ -44,5 +44,5 @@ else done [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!" - $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument + @CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument fi diff --git a/default.nix b/default.nix index f6c8930356..849cac081e 100644 --- a/default.nix +++ b/default.nix @@ -1,5 +1,3 @@ { pkgs ? import ./nix/nixpkgs.nix, llvmPackages ? pkgs.llvmPackages_9 }: -# always use clang inside ccache -let stdenv = pkgs.overrideCC pkgs.stdenv (pkgs.ccacheWrapper.override { cc = llvmPackages.clang; }); -in pkgs.callPackage ./nix/derivation.nix { inherit llvmPackages stdenv; } +pkgs.callPackage ./nix/derivation.nix { inherit llvmPackages; } diff --git a/nix/derivation.nix b/nix/derivation.nix index 73333bb179..0bbb6e18a6 100644 --- a/nix/derivation.nix +++ b/nix/derivation.nix @@ -1,13 +1,13 @@ -{ stdenv, llvmPackages, bash, cmake, python, gmp }: +{ llvmPackages, bash, cmake, ccache, python, gmp }: -stdenv.mkDerivation rec { +llvmPackages.stdenv.mkDerivation rec { name = "lean-${version}"; version = "local"; # I have way too many untracked files in my checkout src = if builtins.pathExists ../.git then builtins.fetchGit { url = ../.; } else ../.; - nativeBuildInputs = [ bash cmake python ]; + nativeBuildInputs = [ bash cmake ccache python ]; buildInputs = [ gmp llvmPackages.llvm ]; enableParallelBuilding = true; @@ -18,7 +18,7 @@ stdenv.mkDerivation rec { patchShebangs ../../bin ''; - meta = with stdenv.lib; { + meta = with llvmPackages.stdenv.lib; { description = "Automatic and interactive theorem prover"; homepage = https://leanprover.github.io/; license = licenses.asl20; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 40a1d42240..8a84c40006 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -29,6 +29,7 @@ set(CMAKE_COLOR_MAKEFILE ON) enable_testing() option(MULTI_THREAD "MULTI_THREAD" ON) +option(CCACHE "use ccache" ON) option(STATIC "STATIC" OFF) option(SPLIT_STACK "SPLIT_STACK" OFF) option(VM_UNCHECKED "VM_UNCHECKED" OFF) @@ -378,6 +379,17 @@ if(TRACK_MEMORY_USAGE) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_TRACK_MEMORY") endif() +# ccache +if(CCACHE) + find_program(CCACHE_PATH ccache) + if(CCACHE_PATH) + set(CMAKE_CXX_COMPILER_LAUNCHER "${CCACHE_PATH}") + set(CMAKE_C_COMPILER_LAUNCHER "${CCACHE_PATH}") + else() + message(WARNING "Failed to find ccache, prepare for longer and redundant builds...") + endif() +endif() + # jemalloc if(JEMALLOC) find_package(Jemalloc) @@ -519,6 +531,7 @@ if(NOT STAGE0) BINARY_DIR stage0 CMAKE_ARGS -DSTAGE0=ON + -DCCACHE=${CCACHE} -DCHECK_OLEAN_VERSION=${CHECK_OLEAN_VERSION} "-DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}" "-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}" diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index 40a1d42240..1045d969e6 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -29,6 +29,7 @@ set(CMAKE_COLOR_MAKEFILE ON) enable_testing() option(MULTI_THREAD "MULTI_THREAD" ON) +option(CCACHE "use ccache" ON) option(STATIC "STATIC" OFF) option(SPLIT_STACK "SPLIT_STACK" OFF) option(VM_UNCHECKED "VM_UNCHECKED" OFF) @@ -378,6 +379,17 @@ if(TRACK_MEMORY_USAGE) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_TRACK_MEMORY") endif() +# ccache +if(CCACHE) + find_program(CCACHE_PATH ccache) + if(CCACHE_PATH) + set(CMAKE_CXX_COMPILER_LAUNCHER "${CCACHE_PATH}") + set(CMAKE_C_COMPILER_LAUNCHER "${CCACHE_PATH}") + else() + message(WARNING "Failed to find ccache, prepare for longer and redundant builds...") + endif() +endif() + # jemalloc if(JEMALLOC) find_package(Jemalloc)