bitwuzla: fix kissat not compiled in error (#400299)

This commit is contained in:
Guillaume Girol 2025-05-06 21:36:15 +02:00 committed by GitHub
commit 0f88b38c1e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 50 additions and 13 deletions

View File

@ -12,6 +12,7 @@
gmp, gmp,
cadical, cadical,
cryptominisat, cryptominisat,
kissat,
zlib, zlib,
pkg-config, pkg-config,
cmake, cmake,
@ -37,6 +38,7 @@ stdenv.mkDerivation (finalAttrs: {
ninja ninja
cmake cmake
]; ];
buildInputs = [ buildInputs = [
cadical cadical
cryptominisat cryptominisat
@ -44,6 +46,7 @@ stdenv.mkDerivation (finalAttrs: {
symfpu symfpu
gmp gmp
zlib zlib
kissat
]; ];
mesonFlags = [ mesonFlags = [
@ -51,6 +54,7 @@ stdenv.mkDerivation (finalAttrs: {
# but setting it to shared works even in pkgsStatic # but setting it to shared works even in pkgsStatic
"-Ddefault_library=shared" "-Ddefault_library=shared"
"-Dcryptominisat=true" "-Dcryptominisat=true"
"-Dkissat=true"
(lib.strings.mesonEnable "testing" finalAttrs.finalPackage.doCheck) (lib.strings.mesonEnable "testing" finalAttrs.finalPackage.doCheck)
]; ];
@ -77,6 +81,7 @@ stdenv.mkDerivation (finalAttrs: {
set -euxo pipefail; set -euxo pipefail;
$out/bin/bitwuzla -S cms -j 3 -m file.smt2 | tee /dev/stderr | grep $needle; $out/bin/bitwuzla -S cms -j 3 -m file.smt2 | tee /dev/stderr | grep $needle;
$out/bin/bitwuzla -S cadical -m file.smt2 | tee /dev/stderr | grep $needle; $out/bin/bitwuzla -S cadical -m file.smt2 | tee /dev/stderr | grep $needle;
$out/bin/bitwuzla -S kissat -m file.smt2 | tee /dev/stderr | grep $needle;
) )
runHook postInstallCheck runHook postInstallCheck

View File

@ -4,8 +4,25 @@
fetchFromGitHub, fetchFromGitHub,
drat-trim, drat-trim,
p7zip, p7zip,
pkg-config,
}: }:
let
# Early meta to reference in pkgconfig generation
meta = with lib; {
description = "'keep it simple and clean bare metal SAT solver' written in C";
mainProgram = "kissat";
longDescription = ''
Kissat is a "keep it simple and clean bare metal SAT solver" written in C.
It is a port of CaDiCaL back to C with improved data structures,
better scheduling of inprocessing and optimized algorithms and implementation.
'';
maintainers = with maintainers; [ shnarazk ];
platforms = platforms.unix;
license = licenses.mit;
homepage = "https://fmv.jku.at/kissat";
};
in
stdenv.mkDerivation rec { stdenv.mkDerivation rec {
pname = "kissat"; pname = "kissat";
version = "4.0.2"; version = "4.0.2";
@ -23,6 +40,10 @@ stdenv.mkDerivation rec {
"lib" "lib"
]; ];
nativeBuildInputs = [
pkg-config
];
nativeCheckInputs = [ nativeCheckInputs = [
drat-trim drat-trim
p7zip p7zip
@ -37,6 +58,14 @@ stdenv.mkDerivation rec {
dontAddPrefix = true; dontAddPrefix = true;
setOutputFlags = false; setOutputFlags = false;
configurePhase = ''
./configure
'';
buildPhase = ''
make -j$NIX_BUILD_CORES
'';
installPhase = '' installPhase = ''
runHook preInstall runHook preInstall
@ -46,20 +75,23 @@ stdenv.mkDerivation rec {
mkdir -p "$out/share/doc/kissat/" mkdir -p "$out/share/doc/kissat/"
install -Dm0644 {LICEN?E,README*,VERSION} "$out/share/doc/kissat/" install -Dm0644 {LICEN?E,README*,VERSION} "$out/share/doc/kissat/"
# Create pkgconfig
mkdir -p $dev/lib/pkgconfig
cat > $dev/lib/pkgconfig/kissat.pc <<EOF
prefix=${placeholder "dev"}
exec_prefix=\''${prefix}
libdir=${placeholder "lib"}/lib
includedir=\''${prefix}/include
Name: ${pname}
Description: ${meta.description}
Version: ${version}
Libs: -L\''${libdir} -lkissat
Cflags: -I\''${includedir}
EOF
runHook postInstall runHook postInstall
''; '';
meta = with lib; { inherit meta;
description = "'keep it simple and clean bare metal SAT solver' written in C";
mainProgram = "kissat";
longDescription = ''
Kissat is a "keep it simple and clean bare metal SAT solver" written in C.
It is a port of CaDiCaL back to C with improved data structures,
better scheduling of inprocessing and optimized algorithms and implementation.
'';
maintainers = with maintainers; [ shnarazk ];
platforms = platforms.unix;
license = licenses.mit;
homepage = "https://fmv.jku.at/kissat";
};
} }