blob: 77613a135710b91e5b3b622d2913149fc52e554b (
plain)
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
|
{ stdenv, fetchurl, haskell, spass }:
stdenv.mkDerivation {
name = "system-for-automated-deduction-2.3.25";
src = fetchurl {
url = "http://nevidal.org/download/sad-2.3-25.tar.gz";
sha256 = "10jd93xgarik7xwys5lq7fx4vqp7c0yg1gfin9cqfch1k1v8ap4b";
};
buildInputs = [ haskell.compiler.ghc844 spass ];
patches = [
./patch.patch
# Since the LTS 12.0 update, <> is an operator in Prelude, colliding with
# the <> operator with a different meaning defined by this package
./monoid.patch
];
postPatch = ''
substituteInPlace Alice/Main.hs --replace init.opt $out/init.opt
'';
installPhase = ''
mkdir -p $out/{bin,provers}
install alice $out/bin
install provers/moses $out/provers
substituteAll provers/provers.dat $out/provers/provers.dat
substituteAll init.opt $out/init.opt
cp -r examples $out
'';
inherit spass;
meta = {
description = "A program for automated proving of mathematical texts";
longDescription = ''
The system for automated deduction is intended for automated processing of formal mathematical texts
written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language
'';
license = stdenv.lib.licenses.gpl3Plus;
maintainers = [ stdenv.lib.maintainers.schmitthenner ];
homepage = "http://nevidal.org/sad.en.html";
platforms = stdenv.lib.platforms.linux;
broken = true; # ghc-8.4.4 is gone from Nixpkgs
};
}
|
