blob: f3c4f22eae3694438ab2ffce8f5c36bd1dba63c7 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
{ stdenv, fetchurl, yap, tcsh, perl, patchelf }:
stdenv.mkDerivation rec {
name = "TPTP-${version}";
version = "7.1.0";
src = fetchurl {
url = [
"http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz"
"http://www.cs.miami.edu/~tptp/TPTP/Archive/TPTP-v${version}.tgz"
];
sha256 = "0slqbqv4y43wz6wnh72s4n540ssapah0d12mndi0c7xr04kf2v2d";
};
nativeBuildInputs = [ patchelf ];
buildInputs = [ tcsh yap perl ];
installPhase = ''
sharedir=$out/share/tptp
mkdir -p $sharedir
cp -r ./ $sharedir
export TPTP=$sharedir
tcsh $sharedir/Scripts/tptp2T_install -default
substituteInPlace $sharedir/TPTP2X/tptp2X_install --replace /bin/mv mv
tcsh $sharedir/TPTP2X/tptp2X_install -default
patchelf --interpreter $(cat $NIX_CC/nix-support/dynamic-linker) $sharedir/Scripts/tptp4X
mkdir -p $out/bin
ln -s $sharedir/TPTP2X/tptp2X $out/bin
ln -s $sharedir/Scripts/tptp2T $out/bin
ln -s $sharedir/Scripts/tptp4X $out/bin
'';
meta = with stdenv.lib; {
description = "Thousands of problems for theorem provers and tools";
maintainers = with maintainers; [ raskin gebner ];
# 6.3 GiB of data. Installation is unpacking and editing a few files.
# No sense in letting Hydra build it.
# Also, it is unclear what is covered by "verbatim" - we will edit configs
hydraPlatforms = [];
platforms = platforms.all;
license = licenses.unfreeRedistributable;
};
}
|