Loading pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch +19 −34 Original line number Diff line number Diff line From 714f5ebe9ade721abdccf58edfcddba52465cb8d Mon Sep 17 00:00:00 2001 From: Jiajie Chen <c@jia.je> Date: Sun, 2 Jul 2023 22:43:27 +0800 From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 11:07:37 +0800 Subject: [PATCH] Do not download sources in cmake --- src/solvers/CMakeLists.txt | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) CMakeLists.txt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index daa0853a57..4bcbbdaa47 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -123,16 +123,6 @@ foreach(SOLVER ${sat_impl}) elseif("${SOLVER}" STREQUAL "cadical") message(STATUS "Building solvers with cadical") - download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt - COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 - ) - - add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) - target_compile_definitions(solvers PUBLIC SATCHECK_CADICAL HAVE_CADICAL ) @@ -140,6 +130,7 @@ foreach(SOLVER ${sat_impl}) target_include_directories(solvers PUBLIC ${cadical_SOURCE_DIR}/src + ${cadical_INCLUDE_DIR} diff --git a/CMakeLists.txt b/CMakeLists.txt index 2c1289a..8128362 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD) include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake") message(STATUS "Downloading Cudd-3.0.0") download_project(PROJ cudd - URL https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download - URL_MD5 4fdafe4924b81648b908881c81fe6c30 + SOURCE_DIR @cudd.src@ ) target_link_libraries(solvers cadical) if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile) -- 2.42.0 2.47.0 pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch 0 → 100644 +53 −0 Original line number Diff line number Diff line From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 11:35:03 +0800 Subject: [PATCH] Do not download sources in cmake --- src/solvers/CMakeLists.txt | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index ab8d111..d7165e2 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with glucose") download_project(PROJ glucose - URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz + SOURCE_DIR @srcglucose@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt - URL_MD5 7c539c62c248b74210aef7414787323a ) add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR}) @@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with cadical") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + SOURCE_DIR @srccadical@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure - URL_MD5 9fc2a66196b86adceb822a583318cc35 ) add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) @@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building with IPASIR solver linking against: CaDiCaL") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + SOURCE_DIR @srccadical@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch COMMAND ./configure - URL_MD5 9fc2a66196b86adceb822a583318cc35 ) message(STATUS "Building CaDiCaL") -- 2.47.0 pkgs/by-name/cb/cbmc/package.nix +93 −45 Original line number Diff line number Diff line { lib , stdenv , fetchFromGitHub , testers , bison , cadical , cbmc , cmake , flex , makeWrapper , perl { lib, stdenv, fetchFromGitHub, testers, bison, cadical, cbmc, cmake, flex, makeWrapper, perl, substituteAll, substitute, cudd, fetchurl, nix-update-script, apple-sdk, apple-sdk_10_15, darwinMinVersionHook, }: stdenv.mkDerivation rec { stdenv.mkDerivation (finalAttrs: { pname = "cbmc"; version = "6.0.1"; version = "6.4.0"; src = fetchFromGitHub { owner = "diffblue"; repo = pname; rev = "${pname}-${version}"; sha256 = "sha256-7syRpCNL7TRZoJaNrmAdahNy7IyovyniYyOwD/lzhuw="; repo = "cbmc"; rev = "refs/tags/cbmc-${finalAttrs.version}"; hash = "sha256-PZZnseOE3nodE0zwyG+82gm55BO4rsCcP4T+fZq7L6I="; }; srcglucose = fetchFromGitHub { owner = "brunodutertre"; repo = "glucose-syrup"; rev = "0bb2afd3b9baace6981cbb8b4a1c7683c44968b7"; hash = "sha256-+KrnXEJe7ApSuj936T615DaXOV+C2LlRxc213fQI+Q4="; }; srccadical = (cadical.override { version = "2.0.0"; }).src; nativeBuildInputs = [ bison cmake Loading @@ -30,25 +51,45 @@ stdenv.mkDerivation rec { makeWrapper ]; buildInputs = [ cadical ]; buildInputs = [ cadical ] ++ lib.optionals stdenv.hostPlatform.isDarwin [ (darwinMinVersionHook "10.15") ] ++ lib.optionals (stdenv.hostPlatform.isDarwin && lib.versionOlder apple-sdk.version "10.15") [ apple-sdk_10_15 ]; # do not download sources # link existing cadical instead patches = [ ./0001-Do-not-download-sources-in-cmake.patch (substituteAll { src = ./0001-Do-not-download-sources-in-cmake.patch; inherit cudd; }) ./0002-Do-not-download-sources-in-cmake.patch ]; postPatch = '' # do not hardcode gcc substituteInPlace "scripts/bash-autocomplete/extract_switches.sh" \ --replace "gcc" "$CC" \ --replace "g++" "$CXX" postPatch = '' # fix library_check.sh interpreter error patchShebangs . '' + lib.optionalString (!stdenv.cc.isGNU) '' mkdir -p srccadical cp -r ${finalAttrs.srccadical}/* srccadical mkdir -p srcglucose cp -r ${finalAttrs.srcglucose}/* srcglucose find -exec chmod +w {} \; substituteInPlace src/solvers/CMakeLists.txt \ --replace-fail "@srccadical@" "$PWD/srccadical" \ --replace-fail "@srcglucose@" "$PWD/srcglucose" '' + lib.optionalString (!stdenv.cc.isGNU) '' # goto-gcc rely on gcc substituteInPlace "regression/CMakeLists.txt" \ --replace "add_subdirectory(goto-gcc)" "" --replace-fail "add_subdirectory(goto-gcc)" "" ''; postInstall = '' Loading @@ -60,29 +101,36 @@ stdenv.mkDerivation rec { --prefix PATH : "$out/share/cbmc" \ ''; env.NIX_CFLAGS_COMPILE = toString (lib.optionals stdenv.cc.isGNU [ env.NIX_CFLAGS_COMPILE = toString ( lib.optionals stdenv.cc.isGNU [ # Needed with GCC 12 but breaks on darwin (with clang) "-Wno-error=maybe-uninitialized" ] ++ lib.optionals stdenv.cc.isClang [ ] ++ lib.optionals stdenv.cc.isClang [ # fix "argument unused during compilation" "-Wno-unused-command-line-argument" ]); ] ); # TODO: add jbmc support cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; passthru.tests.version = testers.testVersion { package = cbmc; command = "cbmc --version"; }; meta = with lib; { passthru.updateScript = nix-update-script { }; meta = { description = "CBMC is a Bounded Model Checker for C and C++ programs"; homepage = "http://www.cprover.org/cbmc/"; license = licenses.bsdOriginal; maintainers = with maintainers; [ jiegec ]; platforms = platforms.unix; # error: no member named 'aligned_alloc' in the global namespace broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isx86_64; license = lib.licenses.bsdOriginal; maintainers = with lib.maintainers; [ jiegec ]; platforms = lib.platforms.unix; }; } }) Loading
pkgs/by-name/cb/cbmc/0001-Do-not-download-sources-in-cmake.patch +19 −34 Original line number Diff line number Diff line From 714f5ebe9ade721abdccf58edfcddba52465cb8d Mon Sep 17 00:00:00 2001 From: Jiajie Chen <c@jia.je> Date: Sun, 2 Jul 2023 22:43:27 +0800 From 7b49a436bd5cc903b86b01f1a0f046ab8ec99fdb Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 11:07:37 +0800 Subject: [PATCH] Do not download sources in cmake --- src/solvers/CMakeLists.txt | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) CMakeLists.txt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index daa0853a57..4bcbbdaa47 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -123,16 +123,6 @@ foreach(SOLVER ${sat_impl}) elseif("${SOLVER}" STREQUAL "cadical") message(STATUS "Building solvers with cadical") - download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch - COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt - COMMAND ./configure - URL_MD5 be646831a017f81b300664e58deba1b5 - ) - - add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) - target_compile_definitions(solvers PUBLIC SATCHECK_CADICAL HAVE_CADICAL ) @@ -140,6 +130,7 @@ foreach(SOLVER ${sat_impl}) target_include_directories(solvers PUBLIC ${cadical_SOURCE_DIR}/src + ${cadical_INCLUDE_DIR} diff --git a/CMakeLists.txt b/CMakeLists.txt index 2c1289a..8128362 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -116,8 +116,7 @@ if(DEFINED CMAKE_USE_CUDD) include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake") message(STATUS "Downloading Cudd-3.0.0") download_project(PROJ cudd - URL https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download - URL_MD5 4fdafe4924b81648b908881c81fe6c30 + SOURCE_DIR @cudd.src@ ) target_link_libraries(solvers cadical) if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile) -- 2.42.0 2.47.0
pkgs/by-name/cb/cbmc/0002-Do-not-download-sources-in-cmake.patch 0 → 100644 +53 −0 Original line number Diff line number Diff line From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001 From: wxt <3264117476@qq.com> Date: Mon, 11 Nov 2024 11:35:03 +0800 Subject: [PATCH] Do not download sources in cmake --- src/solvers/CMakeLists.txt | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index ab8d111..d7165e2 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with glucose") download_project(PROJ glucose - URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz + SOURCE_DIR @srcglucose@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt - URL_MD5 7c539c62c248b74210aef7414787323a ) add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR}) @@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with cadical") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + SOURCE_DIR @srccadical@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure - URL_MD5 9fc2a66196b86adceb822a583318cc35 ) add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) @@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building with IPASIR solver linking against: CaDiCaL") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz + SOURCE_DIR @srccadical@ PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch COMMAND ./configure - URL_MD5 9fc2a66196b86adceb822a583318cc35 ) message(STATUS "Building CaDiCaL") -- 2.47.0
pkgs/by-name/cb/cbmc/package.nix +93 −45 Original line number Diff line number Diff line { lib , stdenv , fetchFromGitHub , testers , bison , cadical , cbmc , cmake , flex , makeWrapper , perl { lib, stdenv, fetchFromGitHub, testers, bison, cadical, cbmc, cmake, flex, makeWrapper, perl, substituteAll, substitute, cudd, fetchurl, nix-update-script, apple-sdk, apple-sdk_10_15, darwinMinVersionHook, }: stdenv.mkDerivation rec { stdenv.mkDerivation (finalAttrs: { pname = "cbmc"; version = "6.0.1"; version = "6.4.0"; src = fetchFromGitHub { owner = "diffblue"; repo = pname; rev = "${pname}-${version}"; sha256 = "sha256-7syRpCNL7TRZoJaNrmAdahNy7IyovyniYyOwD/lzhuw="; repo = "cbmc"; rev = "refs/tags/cbmc-${finalAttrs.version}"; hash = "sha256-PZZnseOE3nodE0zwyG+82gm55BO4rsCcP4T+fZq7L6I="; }; srcglucose = fetchFromGitHub { owner = "brunodutertre"; repo = "glucose-syrup"; rev = "0bb2afd3b9baace6981cbb8b4a1c7683c44968b7"; hash = "sha256-+KrnXEJe7ApSuj936T615DaXOV+C2LlRxc213fQI+Q4="; }; srccadical = (cadical.override { version = "2.0.0"; }).src; nativeBuildInputs = [ bison cmake Loading @@ -30,25 +51,45 @@ stdenv.mkDerivation rec { makeWrapper ]; buildInputs = [ cadical ]; buildInputs = [ cadical ] ++ lib.optionals stdenv.hostPlatform.isDarwin [ (darwinMinVersionHook "10.15") ] ++ lib.optionals (stdenv.hostPlatform.isDarwin && lib.versionOlder apple-sdk.version "10.15") [ apple-sdk_10_15 ]; # do not download sources # link existing cadical instead patches = [ ./0001-Do-not-download-sources-in-cmake.patch (substituteAll { src = ./0001-Do-not-download-sources-in-cmake.patch; inherit cudd; }) ./0002-Do-not-download-sources-in-cmake.patch ]; postPatch = '' # do not hardcode gcc substituteInPlace "scripts/bash-autocomplete/extract_switches.sh" \ --replace "gcc" "$CC" \ --replace "g++" "$CXX" postPatch = '' # fix library_check.sh interpreter error patchShebangs . '' + lib.optionalString (!stdenv.cc.isGNU) '' mkdir -p srccadical cp -r ${finalAttrs.srccadical}/* srccadical mkdir -p srcglucose cp -r ${finalAttrs.srcglucose}/* srcglucose find -exec chmod +w {} \; substituteInPlace src/solvers/CMakeLists.txt \ --replace-fail "@srccadical@" "$PWD/srccadical" \ --replace-fail "@srcglucose@" "$PWD/srcglucose" '' + lib.optionalString (!stdenv.cc.isGNU) '' # goto-gcc rely on gcc substituteInPlace "regression/CMakeLists.txt" \ --replace "add_subdirectory(goto-gcc)" "" --replace-fail "add_subdirectory(goto-gcc)" "" ''; postInstall = '' Loading @@ -60,29 +101,36 @@ stdenv.mkDerivation rec { --prefix PATH : "$out/share/cbmc" \ ''; env.NIX_CFLAGS_COMPILE = toString (lib.optionals stdenv.cc.isGNU [ env.NIX_CFLAGS_COMPILE = toString ( lib.optionals stdenv.cc.isGNU [ # Needed with GCC 12 but breaks on darwin (with clang) "-Wno-error=maybe-uninitialized" ] ++ lib.optionals stdenv.cc.isClang [ ] ++ lib.optionals stdenv.cc.isClang [ # fix "argument unused during compilation" "-Wno-unused-command-line-argument" ]); ] ); # TODO: add jbmc support cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; passthru.tests.version = testers.testVersion { package = cbmc; command = "cbmc --version"; }; meta = with lib; { passthru.updateScript = nix-update-script { }; meta = { description = "CBMC is a Bounded Model Checker for C and C++ programs"; homepage = "http://www.cprover.org/cbmc/"; license = licenses.bsdOriginal; maintainers = with maintainers; [ jiegec ]; platforms = platforms.unix; # error: no member named 'aligned_alloc' in the global namespace broken = stdenv.hostPlatform.isDarwin && stdenv.hostPlatform.isx86_64; license = lib.licenses.bsdOriginal; maintainers = with lib.maintainers; [ jiegec ]; platforms = lib.platforms.unix; }; } })
