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

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