2021-01-15 13:21:58 +00:00
|
|
|
{ lib, stdenv, fetchpatch, fetchFromGitHub, cmake, zlib, gmp, jdk8,
|
2022-12-18 00:39:44 +00:00
|
|
|
# The JDK we use on Darwin currently makes extensive use of rpaths which are
|
2018-07-08 16:42:56 +00:00
|
|
|
# annoying and break the python library, so let's not bother for now
|
|
|
|
includeJava ? !stdenv.hostPlatform.isDarwin, includeGplCode ? true }:
|
|
|
|
|
|
|
|
let
|
|
|
|
boolToCmake = x: if x then "ON" else "OFF";
|
|
|
|
|
2019-06-26 19:44:22 +00:00
|
|
|
rev = "1.8.0";
|
|
|
|
sha256 = "0q3a8x3iih25xkp2bm842sm2hxlb8hxlls4qmvj7vzwrh4lvsl7b";
|
2018-07-08 16:42:56 +00:00
|
|
|
|
|
|
|
pname = "monosat";
|
2019-06-26 19:44:22 +00:00
|
|
|
version = rev;
|
2018-07-08 16:42:56 +00:00
|
|
|
|
|
|
|
src = fetchFromGitHub {
|
|
|
|
owner = "sambayless";
|
|
|
|
repo = pname;
|
|
|
|
inherit rev sha256;
|
|
|
|
};
|
|
|
|
|
2020-03-02 22:18:08 +00:00
|
|
|
patches = [
|
|
|
|
# Python 3.8 compatibility
|
|
|
|
(fetchpatch {
|
2020-04-01 01:11:51 +00:00
|
|
|
url = "https://github.com/sambayless/monosat/commit/a5079711d0df0451f9840f3a41248e56dbb03967.patch";
|
2020-03-03 17:44:33 +00:00
|
|
|
sha256 = "1p2y0jw8hb9c90nbffhn86k1dxd6f6hk5v70dfmpzka3y6g1ksal";
|
2020-03-02 22:18:08 +00:00
|
|
|
})
|
|
|
|
];
|
|
|
|
|
2021-11-14 14:31:09 +00:00
|
|
|
# source behind __linux__ check assumes system is also x86 and
|
|
|
|
# tries to disable x86/x87-specific extended precision mode
|
|
|
|
# https://github.com/sambayless/monosat/issues/33
|
2021-11-21 01:50:41 +00:00
|
|
|
commonPostPatch = lib.optionalString (!stdenv.hostPlatform.isx86) ''
|
2021-11-14 14:31:09 +00:00
|
|
|
substituteInPlace src/monosat/Main.cc \
|
|
|
|
--replace 'defined(__linux__)' '0'
|
|
|
|
'';
|
|
|
|
|
2019-08-13 21:52:01 +00:00
|
|
|
core = stdenv.mkDerivation {
|
2018-07-08 16:42:56 +00:00
|
|
|
name = "${pname}-${version}";
|
2020-03-02 22:18:08 +00:00
|
|
|
inherit src patches;
|
2021-11-14 14:31:09 +00:00
|
|
|
postPatch = commonPostPatch;
|
2020-12-31 07:48:55 +00:00
|
|
|
nativeBuildInputs = [ cmake ];
|
|
|
|
buildInputs = [ zlib gmp jdk8 ];
|
2018-07-08 16:42:56 +00:00
|
|
|
|
2019-06-26 19:44:22 +00:00
|
|
|
cmakeFlags = [
|
|
|
|
"-DBUILD_STATIC=OFF"
|
|
|
|
"-DJAVA=${boolToCmake includeJava}"
|
|
|
|
"-DGPL=${boolToCmake includeGplCode}"
|
2022-07-14 23:50:09 +00:00
|
|
|
|
|
|
|
# file RPATH_CHANGE could not write new RPATH
|
|
|
|
"-DCMAKE_SKIP_BUILD_RPATH=ON"
|
2019-06-26 19:44:22 +00:00
|
|
|
];
|
2018-07-08 16:42:56 +00:00
|
|
|
|
2024-08-13 20:04:30 +00:00
|
|
|
postInstall = lib.optionalString includeJava ''
|
2018-07-08 16:42:56 +00:00
|
|
|
mkdir -p $out/share/java
|
|
|
|
cp monosat.jar $out/share/java
|
|
|
|
'';
|
|
|
|
|
|
|
|
passthru = { inherit python; };
|
|
|
|
|
2024-08-13 20:04:30 +00:00
|
|
|
meta = with lib; {
|
2018-07-08 16:42:56 +00:00
|
|
|
description = "SMT solver for Monotonic Theories";
|
2024-03-19 02:14:51 +00:00
|
|
|
mainProgram = "monosat";
|
2018-07-08 16:42:56 +00:00
|
|
|
platforms = platforms.unix;
|
|
|
|
license = if includeGplCode then licenses.gpl2 else licenses.mit;
|
2020-04-01 01:11:51 +00:00
|
|
|
homepage = "https://github.com/sambayless/monosat";
|
2019-06-26 20:24:16 +00:00
|
|
|
maintainers = [ maintainers.acairncross ];
|
2018-07-08 16:42:56 +00:00
|
|
|
};
|
|
|
|
};
|
|
|
|
|
2022-05-12 00:29:58 +00:00
|
|
|
python = { buildPythonPackage, cython, pytestCheckHook }: buildPythonPackage {
|
2020-03-02 22:18:08 +00:00
|
|
|
inherit pname version src patches;
|
2018-07-08 16:42:56 +00:00
|
|
|
|
|
|
|
propagatedBuildInputs = [ core cython ];
|
|
|
|
|
2019-06-26 19:44:22 +00:00
|
|
|
# This tells setup.py to use cython, which should produce faster bindings
|
2018-07-09 02:04:05 +00:00
|
|
|
MONOSAT_CYTHON = true;
|
|
|
|
|
2020-03-02 22:18:08 +00:00
|
|
|
# After patching src, move to where the actually relevant source is. This could just be made
|
|
|
|
# the sourceRoot if it weren't for the patch.
|
2021-11-14 14:31:09 +00:00
|
|
|
postPatch = commonPostPatch + ''
|
2020-03-02 22:18:08 +00:00
|
|
|
cd src/monosat/api/python
|
|
|
|
'' +
|
2018-07-08 16:42:56 +00:00
|
|
|
# The relative paths here don't make sense for our Nix build
|
|
|
|
# TODO: do we want to just reference the core monosat library rather than copying the
|
|
|
|
# shared lib? The current setup.py copies the .dylib/.so...
|
2020-03-02 22:18:08 +00:00
|
|
|
''
|
2018-07-08 16:42:56 +00:00
|
|
|
substituteInPlace setup.py \
|
2019-06-26 19:44:22 +00:00
|
|
|
--replace 'library_dir = "../../../../"' 'library_dir = "${core}/lib/"'
|
2018-07-08 16:42:56 +00:00
|
|
|
'';
|
2022-05-12 00:29:58 +00:00
|
|
|
|
2023-01-21 12:00:00 +00:00
|
|
|
nativeCheckInputs = [ pytestCheckHook ];
|
2022-05-12 00:29:58 +00:00
|
|
|
|
|
|
|
disabledTests = [
|
|
|
|
"test_assertAtMostOne"
|
|
|
|
"test_assertEqual"
|
|
|
|
];
|
2018-07-08 16:42:56 +00:00
|
|
|
};
|
2019-10-07 15:20:23 +00:00
|
|
|
in core
|