tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 ocaml,
6 zlib,
7 which,
8 eprover,
9 makeWrapper,
10 coq,
11}:
12stdenv.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}