tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 bison,
6 flex,
7}:
8
9let
10 baseVersion = "3";
11 minorVersion = "9";
12
13 extraTools =
14 "FLOTTER prolog2dfg dfg2otter dfg2dimacs dfg2tptp"
15 + " dfg2ascii dfg2dfg tptp2dfg dimacs2dfg pgen rescmp";
16in
17
18stdenv.mkDerivation {
19 pname = "spass";
20 version = "${baseVersion}.${minorVersion}";
21
22 src = fetchurl {
23 url = "http://www.spass-prover.org/download/sources/spass${baseVersion}${minorVersion}.tgz";
24 sha256 = "11cyn3kcff4r79rsw2s0xm6rdb8bi0kpkazv2b48jhcms7xw75qp";
25 };
26
27 sourceRoot = ".";
28
29 nativeBuildInputs = [
30 bison
31 flex
32 ];
33
34 buildPhase = ''
35 make RM="rm -f" proparser.c ${extraTools} opt
36 '';
37 installPhase = ''
38 mkdir -p $out/bin
39 install -m0755 SPASS ${extraTools} $out/bin/
40 '';
41
42 meta = with lib; {
43 description = "Automated theorem prover for first-order logic";
44 maintainers = with maintainers; [
45 raskin
46 ];
47 platforms = platforms.unix;
48 license = licenses.bsd2;
49 downloadPage = "http://www.spass-prover.org/download/index.html";
50 };
51}