From 5a610c5f8d00da3e05694ae5b5fa0b4abc81218f Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 1/8] cadical: add pkg-config file bitwuzla switched to meson, and I was not able to tell meson how to tell where cadical is located without a pkg-config file --- .../science/logic/cadical/default.nix | 26 ++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix index 873b3836b73e..a4d93fbd2631 100644 --- a/pkgs/applications/science/logic/cadical/default.nix +++ b/pkgs/applications/science/logic/cadical/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchFromGitHub }: +{ lib, stdenv, fetchFromGitHub, copyPkgconfigItems, makePkgconfigItem }: stdenv.mkDerivation rec { pname = "cadical"; @@ -14,6 +14,30 @@ stdenv.mkDerivation rec { outputs = [ "out" "dev" "lib" ]; doCheck = true; + nativeBuildInputs = [ copyPkgconfigItems ]; + + pkgconfigItems = [ + (makePkgconfigItem { + name = "cadical"; + inherit version; + cflags = [ "-I\${includedir}" ]; + libs = [ "-L\${libdir}" "-lcadical" ]; + variables = { + includedir = "@includedir@"; + libdir = "@libdir@"; + }; + inherit (meta) description; + }) + ]; + + env = { + # copyPkgconfigItems will substitute these in the pkg-config file + includedir = "${placeholder "dev"}/include"; + libdir = "${placeholder "lib"}/lib"; + }; + + enableParallelBuilding = true; + # the configure script is not generated by autotools and does not accept the # arguments that the default configurePhase passes like --prefix and --libdir configurePhase = '' From 5ff10ee902e80132c5e92321a03452cd7b0d403b Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 2/8] symfpu: install headers in $out/include, add a pkg-config file bitwuzla switched to meson, and I found no other way to have meson find symfpu --- .../science/logic/symfpu/default.nix | 29 +++++++++++++++++-- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/pkgs/applications/science/logic/symfpu/default.nix b/pkgs/applications/science/logic/symfpu/default.nix index af61b7c617c7..2c83793114a1 100644 --- a/pkgs/applications/science/logic/symfpu/default.nix +++ b/pkgs/applications/science/logic/symfpu/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, fetchFromGitHub }: +{ lib, stdenv, fetchFromGitHub, copyPkgconfigItems, makePkgconfigItem }: stdenv.mkDerivation rec { pname = "symfpu"; @@ -11,9 +11,32 @@ stdenv.mkDerivation rec { sha256 = "1jf5lkn67q136ppfacw3lsry369v7mdr1rhidzjpbz18jfy9zl9q"; }; + nativeBuildInputs = [ copyPkgconfigItems ]; + + pkgconfigItems = [ + (makePkgconfigItem { + name = "symfpu"; + inherit version; + cflags = [ "-I\${includedir}" ]; + variables = { + includedir = "@includedir@"; + }; + inherit (meta) description; + }) + ]; + + env = { + # copyPkgconfigItems will substitute this in the pkg-config file + includedir = "${placeholder "out"}/include"; + }; + installPhase = '' - mkdir -p $out/symfpu - cp -r * $out/symfpu/ + runHook preInstall + + mkdir -p $out/include/symfpu + cp -r * $out/include/symfpu/ + + runHook postInstall ''; meta = with lib; { From 457090959e06536fa01a2b91f005eb61e40d83dc Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 3/8] bitwuzla: unstable-2022-10-03 -> 0.4.0 lingeling, picosat and minisat are no longer dependencies --- .../science/logic/bitwuzla/default.nix | 40 ++++++------------- 1 file changed, 13 insertions(+), 27 deletions(-) diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix index bacf8620e5fd..0d85540c280b 100644 --- a/pkgs/applications/science/logic/bitwuzla/default.nix +++ b/pkgs/applications/science/logic/bitwuzla/default.nix @@ -2,62 +2,48 @@ , fetchFromGitHub , lib , python3 -, cmake -, lingeling +, meson +, ninja +, git , btor2tools , symfpu , gtest , gmp , cadical -, minisat -, picosat , cryptominisat , zlib , pkg-config - # "*** internal error in 'lglib.c': watcher stack overflow" on aarch64-linux -, withLingeling ? !stdenv.hostPlatform.isAarch64 }: stdenv.mkDerivation rec { pname = "bitwuzla"; - version = "unstable-2022-10-03"; + version = "0.4.0"; src = fetchFromGitHub { owner = "bitwuzla"; repo = "bitwuzla"; - rev = "3bc0f9f1aca04afabe1aff53dd0937924618b2ad"; - hash = "sha256-UXZERl7Nedwex/oUrcf6/GkDSgOQ537WDYm117RfvWo="; + rev = version; + hash = "sha256-ZEdV4ml1LwrYwscgOcL2gLx/ijPYqRktXMQH/Njh8OI="; }; - nativeBuildInputs = [ cmake pkg-config ]; + strictDeps = true; + + nativeBuildInputs = [ meson pkg-config git ninja ]; buildInputs = [ cadical cryptominisat - picosat - minisat btor2tools symfpu gmp zlib - ] ++ lib.optional withLingeling lingeling; + ]; - cmakeFlags = [ - "-DBUILD_SHARED_LIBS=ON" - "-DPicoSAT_INCLUDE_DIR=${lib.getDev picosat}/include/picosat" - "-DBtor2Tools_INCLUDE_DIR=${lib.getDev btor2tools}/include/btor2parser" - "-DBtor2Tools_LIBRARIES=${lib.getLib btor2tools}/lib/libbtor2parser${stdenv.hostPlatform.extensions.sharedLibrary}" - ] ++ lib.optional doCheck "-DTESTING=YES"; + mesonFlags = [ "-Ddefault_library=shared" ]; - nativeCheckInputs = [ python3 gtest ]; + nativeCheckInputs = [ python3 ]; + checkInputs = [ gtest ]; # two tests fail on darwin and 3 on aarch64-linux doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64); - preCheck = let - var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"; - in - '' - export ${var}=$(readlink -f lib) - patchShebangs .. - ''; meta = with lib; { description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions"; From 67dc7cc9931b2bdfb2d5bbd59e2be37703663983 Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 4/8] cadical: fix static build --- pkgs/applications/science/logic/cadical/default.nix | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix index a4d93fbd2631..12b01dea1a3d 100644 --- a/pkgs/applications/science/logic/cadical/default.nix +++ b/pkgs/applications/science/logic/cadical/default.nix @@ -38,6 +38,11 @@ stdenv.mkDerivation rec { enableParallelBuilding = true; + # fix static build + postPatch = '' + substituteInPlace makefile.in --replace-fail "ar rc" '$(AR) rc' + ''; + # the configure script is not generated by autotools and does not accept the # arguments that the default configurePhase passes like --prefix and --libdir configurePhase = '' From 75e6297d10c6baea15cb3e6896bb77219f6569b7 Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 5/8] cryptominisat: fix static build --- .../science/logic/cryptominisat/default.nix | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/pkgs/applications/science/logic/cryptominisat/default.nix b/pkgs/applications/science/logic/cryptominisat/default.nix index 4be57a194635..4040cdb79729 100644 --- a/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/pkgs/applications/science/logic/cryptominisat/default.nix @@ -17,8 +17,14 @@ stdenv.mkDerivation rec { hash = "sha256-8oH9moMjQEWnQXKmKcqmXuXcYkEyvr4hwC1bC4l26mo="; }; - buildInputs = [ python3 boost ]; - nativeBuildInputs = [ cmake ]; + strictDeps = true; + buildInputs = [ boost ]; + nativeBuildInputs = [ python3 cmake ]; + + # musl does not have sys/unistd.h + postPatch = '' + substituteInPlace src/picosat/picosat.c --replace-fail '' '' + ''; meta = with lib; { description = "An advanced SAT Solver"; From 4c932f96886bcf2d0a866af4d421339b01e8af42 Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 6/8] bitwuzla: fix build with doCheck = false --- .../science/logic/bitwuzla/default.nix | 22 ++++++++++++------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix index 0d85540c280b..3246e534d8c1 100644 --- a/pkgs/applications/science/logic/bitwuzla/default.nix +++ b/pkgs/applications/science/logic/bitwuzla/default.nix @@ -15,14 +15,14 @@ , pkg-config }: -stdenv.mkDerivation rec { +stdenv.mkDerivation (finalAttrs: { pname = "bitwuzla"; version = "0.4.0"; src = fetchFromGitHub { owner = "bitwuzla"; repo = "bitwuzla"; - rev = version; + rev = finalAttrs.version; hash = "sha256-ZEdV4ml1LwrYwscgOcL2gLx/ijPYqRktXMQH/Njh8OI="; }; @@ -38,19 +38,25 @@ stdenv.mkDerivation rec { zlib ]; - mesonFlags = [ "-Ddefault_library=shared" ]; + mesonFlags = [ + # note: the default value for default_library fails to link dynamic dependencies + # but setting it to shared works even in pkgsStatic + "-Ddefault_library=shared" + + (lib.strings.mesonEnable "testing" finalAttrs.doCheck) + ]; nativeCheckInputs = [ python3 ]; checkInputs = [ gtest ]; # two tests fail on darwin and 3 on aarch64-linux doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64); - meta = with lib; { + meta = { description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions"; mainProgram = "bitwuzla"; homepage = "https://bitwuzla.github.io"; - license = licenses.mit; - platforms = platforms.unix; - maintainers = with maintainers; [ symphorien ]; + license = lib.licenses.mit; + platforms = lib.platforms.unix; + maintainers = with lib.maintainers; [ symphorien ]; }; -} +}) From 71096455f0632ef6c6f60b3e1a51b77afe8b813c Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 7/8] bitwuzla: fix on aarch64-linux --- pkgs/applications/science/logic/bitwuzla/default.nix | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix index 3246e534d8c1..c46ecb290520 100644 --- a/pkgs/applications/science/logic/bitwuzla/default.nix +++ b/pkgs/applications/science/logic/bitwuzla/default.nix @@ -1,5 +1,6 @@ { stdenv , fetchFromGitHub +, fetchpatch , lib , python3 , meson @@ -26,6 +27,15 @@ stdenv.mkDerivation (finalAttrs: { hash = "sha256-ZEdV4ml1LwrYwscgOcL2gLx/ijPYqRktXMQH/Njh8OI="; }; + patches = [ + # fix parser on aarch64 + # remove on next release + (fetchpatch { + url = "https://github.com/bitwuzla/bitwuzla/commit/4d914aa5ec34076c37749f0cf6dce976ea510386.patch"; + hash = "sha256-gp+HEamOySjPXCC39tt5DIMdQqEew26a+M15sNdCmTM="; + }) + ]; + strictDeps = true; nativeBuildInputs = [ meson pkg-config git ninja ]; From 5847c4078d299b88d8e4c27843a6ec4ac9aad1c6 Mon Sep 17 00:00:00 2001 From: Guillaume Girol Date: Wed, 3 Apr 2024 12:00:00 +0000 Subject: [PATCH 8/8] bitwuzla: test on aarch64-linux --- pkgs/applications/science/logic/bitwuzla/default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix index c46ecb290520..1fa78849db6e 100644 --- a/pkgs/applications/science/logic/bitwuzla/default.nix +++ b/pkgs/applications/science/logic/bitwuzla/default.nix @@ -58,8 +58,8 @@ stdenv.mkDerivation (finalAttrs: { nativeCheckInputs = [ python3 ]; checkInputs = [ gtest ]; - # two tests fail on darwin and 3 on aarch64-linux - doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64); + # two tests fail on darwin + doCheck = stdenv.hostPlatform.isLinux; meta = { description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";