diff options
Diffstat (limited to 'pkgs/applications/science/logic')
8 files changed, 15 insertions, 116 deletions
diff --git a/pkgs/applications/science/logic/avy/default.nix b/pkgs/applications/science/logic/avy/default.nix index 9b59828ddab..b43e0c6fbf1 100644 --- a/pkgs/applications/science/logic/avy/default.nix +++ b/pkgs/applications/science/logic/avy/default.nix @@ -12,14 +12,14 @@ stdenv.mkDerivation { }; buildInputs = [ cmake zlib boost.out boost.dev ]; - NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ] + NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ] # Squelch endless stream of warnings on same few things ++ stdenv.lib.optionals stdenv.cc.isClang [ "-Wno-empty-body" "-Wno-tautological-compare" "-Wc++11-compat-deprecated-writable-strings" "-Wno-deprecated" - ]; + ]); prePatch = '' sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 2378cb9408e..ac001540e09 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -143,7 +143,7 @@ self = stdenv.mkDerivation { prefixKey = "-prefix "; - buildFlags = "revision coq coqide bin/votour"; + buildFlags = [ "revision" "coq" "coqide" "bin/votour" ]; createFindlibDestdir = true; diff --git a/pkgs/applications/science/logic/minisat/clang.diff b/pkgs/applications/science/logic/minisat/clang.diff deleted file mode 100644 index 5b5072c71f3..00000000000 --- a/pkgs/applications/science/logic/minisat/clang.diff +++ /dev/null @@ -1,45 +0,0 @@ -diff -aur minisat/core/SolverTypes.h minisat.clang/core/SolverTypes.h ---- minisat/core/SolverTypes.h 2010-07-10 18:07:36.000000000 +0200 -+++ minisat.clang/core/SolverTypes.h 2016-05-13 12:14:50.759671959 +0200 -@@ -47,7 +47,7 @@ - int x; - - // Use this as a constructor: -- friend Lit mkLit(Var var, bool sign = false); -+ //friend Lit mkLit(Var var, bool sign = false); - - bool operator == (Lit p) const { return x == p.x; } - bool operator != (Lit p) const { return x != p.x; } -@@ -55,7 +55,7 @@ - }; - - --inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } -+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } - inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } - inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } - inline bool sign (Lit p) { return p.x & 1; } -diff -aur minisat/utils/Options.h minisat.clang/utils/Options.h ---- minisat/utils/Options.h 2010-07-10 18:07:36.000000000 +0200 -+++ minisat.clang/utils/Options.h 2016-05-13 12:14:50.759671959 +0200 -@@ -282,15 +282,15 @@ - if (range.begin == INT64_MIN) - fprintf(stderr, "imin"); - else -- fprintf(stderr, "%4"PRIi64, range.begin); -+ fprintf(stderr, "%4" PRIi64, range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT64_MAX) - fprintf(stderr, "imax"); - else -- fprintf(stderr, "%4"PRIi64, range.end); -+ fprintf(stderr, "%4" PRIi64, range.end); - -- fprintf(stderr, "] (default: %"PRIi64")\n", value); -+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); -Only in minisat.clang/utils: Options.o -Only in minisat.clang/utils: System.o diff --git a/pkgs/applications/science/logic/minisat/darwin.patch b/pkgs/applications/science/logic/minisat/darwin.patch deleted file mode 100644 index f2b618d6bb3..00000000000 --- a/pkgs/applications/science/logic/minisat/darwin.patch +++ /dev/null @@ -1,26 +0,0 @@ -https://github.com/fasterthanlime/homebrew-mingw/blob/master/Library/Formula/minisat.rb - -diff --git a/utils/System.cc b/utils/System.cc -index a7cf53f..feeaf3c 100644 ---- a/utils/System.cc -+++ b/utils/System.cc -@@ -78,16 +78,17 @@ double Minisat::memUsed(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_maxrss / 1024; } --double MiniSat::memUsedPeak(void) { return memUsed(); } -+double Minisat::memUsedPeak(void) { return memUsed(); } - - - #elif defined(__APPLE__) - #include <malloc/malloc.h> - --double Minisat::memUsed(void) { -+double Minisat::memUsed() { - malloc_statistics_t t; - malloc_zone_statistics(NULL, &t); - return (double)t.max_size_in_use / (1024*1024); } -+double Minisat::memUsedPeak() { return memUsed(); } - - #else - double Minisat::memUsed() { diff --git a/pkgs/applications/science/logic/minisat/default.nix b/pkgs/applications/science/logic/minisat/default.nix index 34051a1da40..6b642832b83 100644 --- a/pkgs/applications/science/logic/minisat/default.nix +++ b/pkgs/applications/science/logic/minisat/default.nix @@ -1,27 +1,19 @@ -{ stdenv, fetchurl, zlib }: +{ stdenv, fetchFromGitHub, cmake, zlib }: stdenv.mkDerivation rec { pname = "minisat"; - version = "2.2.0"; + version = "2.2.1"; - src = fetchurl { - url = "http://minisat.se/downloads/${pname}-${version}.tar.gz"; - sha256 = "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj"; + src = fetchFromGitHub { + owner = "stp"; + repo = pname; + rev = "releases/${version}"; + sha256 = "14vcbjnlia00lpyv2fhbmw3wbc9bk9h7bln9zpyc3nwiz5cbjz4a"; }; - patches = - [ ./darwin.patch ] - ++ stdenv.lib.optionals stdenv.cc.isClang [ ./clang.diff ]; - + nativeBuildInputs = [ cmake ]; buildInputs = [ zlib ]; - preBuild = "cd simp"; - makeFlags = [ "r" "MROOT=.." ]; - installPhase = '' - mkdir -p $out/bin - cp minisat_release $out/bin/minisat - ''; - meta = with stdenv.lib; { description = "Compact and readable SAT solver"; maintainers = with maintainers; [ gebner raskin ]; diff --git a/pkgs/applications/science/logic/minisat/unstable.nix b/pkgs/applications/science/logic/minisat/unstable.nix deleted file mode 100644 index ef46c694acb..00000000000 --- a/pkgs/applications/science/logic/minisat/unstable.nix +++ /dev/null @@ -1,23 +0,0 @@ -{ stdenv, fetchFromGitHub, zlib, cmake }: - -stdenv.mkDerivation { - name = "minisat-unstable-2013-09-25"; - - src = fetchFromGitHub { - owner = "niklasso"; - repo = "minisat"; - rev = "37dc6c67e2af26379d88ce349eb9c4c6160e8543"; - sha256 = "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq"; - }; - - buildInputs = [ zlib ]; - nativeBuildInputs = [ cmake ]; - - meta = with stdenv.lib; { - description = "Compact and readable SAT solver"; - maintainers = with maintainers; [ mic92 ]; - platforms = platforms.unix; - license = licenses.mit; - homepage = http://minisat.se/; - }; -} diff --git a/pkgs/applications/science/logic/prover9/default.nix b/pkgs/applications/science/logic/prover9/default.nix index a4538e1070a..9528a5942a4 100644 --- a/pkgs/applications/science/logic/prover9/default.nix +++ b/pkgs/applications/science/logic/prover9/default.nix @@ -21,7 +21,7 @@ stdenv.mkDerivation { done ''; - buildFlags = "all"; + buildFlags = [ "all" ]; checkPhase = "make test1"; diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix index 0ea659d1927..dd00eda1b57 100644 --- a/pkgs/applications/science/logic/stp/default.nix +++ b/pkgs/applications/science/logic/stp/default.nix @@ -1,4 +1,5 @@ -{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }: +{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl +, python3, python3Packages, zlib, minisat, cryptominisat }: stdenv.mkDerivation rec { pname = "stp"; @@ -11,7 +12,7 @@ stdenv.mkDerivation rec { sha256 = "1yg2v4wmswh1sigk47drwsxyayr472mf4i47lqmlcgn9hhbx1q87"; }; - buildInputs = [ boost zlib minisatUnstable cryptominisat python3 ]; + buildInputs = [ boost zlib minisat cryptominisat python3 ]; nativeBuildInputs = [ cmake bison flex perl ]; preConfigure = '' python_install_dir=$out/${python3Packages.python.sitePackages} |