pkgs/applications/science/logic/satallax/default.nix

   1 { lib, stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq }:
   2 stdenv.mkDerivation rec {
   3   pname = "satallax";
   4   version = "2.7";
   5
   6   strictDeps = true;
   7
   8   nativeBuildInputs = [ makeWrapper ocaml which eprover coq ];
   9   buildInputs = [ zlib ];
  10
  11   src = fetchurl {
  12     url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${pname}-${version}.tar.gz";
  13     sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib";
  14   };
  15
  16   patches = [
  17     # GCC9 doesn't allow default value in friend declaration.
  18     ./fix-declaration-gcc9.patch
  19   ];
  20
  21   prePatch = ''
  22     patch -p1 -i ${../avy/minisat-fenv.patch} -d minisat
  23   '';
  24
  25   preConfigure = ''
  26     mkdir fake-tools
  27     echo "echo 'Nix-build-host.localdomain'" > fake-tools/hostname
  28     chmod a+x fake-tools/hostname
  29     export PATH="$PATH:$PWD/fake-tools"
  30
  31     (
  32       cd picosat-*
  33       ./configure
  34       make
  35     )
  36     export PATH="$PATH:$PWD/libexec/satallax"
  37
  38     mkdir -p "$out/libexec/satallax"
  39     cp picosat-*/picosat picosat-*/picomus "$out/libexec/satallax"
  40
  41     (
  42       cd minisat
  43       export MROOT=$PWD
  44       cd core
  45       make
  46       cd ../simp
  47       make
  48     )
  49   '';
  50
  51   # error: invalid suffix on literal; C++11 requires a space between literal and identifier
  52   env.NIX_CFLAGS_COMPILE = lib.optionalString stdenv.hostPlatform.isDarwin "-Wno-reserved-user-defined-literal";
  53
  54   installPhase = ''
  55     mkdir -p "$out/share/doc/satallax" "$out/bin" "$out/lib" "$out/lib/satallax"
  56     cp bin/satallax.opt "$out/bin/satallax"
  57     wrapProgram "$out/bin/satallax" \
  58       --suffix PATH : "${lib.makeBinPath [ coq eprover ]}:$out/libexec/satallax" \
  59       --add-flags "-M" --add-flags "$out/lib/satallax/modes"
  60
  61     cp LICENSE README "$out/share/doc/satallax"
  62
  63     cp bin/*.so "$out/lib"
  64
  65     cp -r modes "$out/lib/satallax/"
  66     cp -r problems "$out/lib/satallax/"
  67     cp -r coq* "$out/lib/satallax/"
  68   '';
  69
  70   doCheck = stdenv.hostPlatform.isLinux;
  71
  72   checkPhase = ''
  73     runHook preCheck
  74     if bash ./test | grep ERROR; then
  75       echo "Tests failed"
  76       exit 1
  77     fi
  78     runHook postCheck
  79   '';
  80
  81   meta = {
  82     description = "Automated theorem prover for higher-order logic";
  83     mainProgram = "satallax";
  84     license = lib.licenses.mit;
  85     maintainers = [ lib.maintainers.raskin ];
  86     platforms = lib.platforms.unix;
  87     downloadPage = "http://www.ps.uni-saarland.de/~cebrown/satallax/downloads.php";
  88     homepage = "http://www.ps.uni-saarland.de/~cebrown/satallax/index.php";
  89   };
  90 }