2
2
lib ,
3
3
stdenv ,
4
4
fetchurl ,
5
+ versionCheckHook ,
5
6
} :
6
7
7
8
stdenv . mkDerivation {
8
9
pname = "prover9" ;
9
- version = "2009-11a " ;
10
+ version = "2009-11A " ;
10
11
11
12
src = fetchurl {
12
13
url = "https://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz" ;
13
- sha256 = "1l2i3d3h5z7nnbzilb6z92r0rbx0kh6yaxn2c5qhn3000xcfsay3 " ;
14
+ hash = "sha256-wyvtWAcADAtxYcJ25Q2coK8MskjfLBr/svb8AkcbUdA= " ;
14
15
} ;
15
16
16
17
hardeningDisable = [ "format" ] ;
@@ -20,31 +21,54 @@ stdenv.mkDerivation {
20
21
MV=$(type -tp mv)
21
22
CP=$(type -tp cp)
22
23
for f in Makefile */Makefile; do
23
- substituteInPlace $f --replace "/bin/rm" "$RM" \
24
- --replace "/bin/mv" "$MV" \
25
- --replace "/bin/cp" "$CP";
24
+ substituteInPlace $f --replace-quiet "/bin/rm" "$RM" \
25
+ --replace-quiet "/bin/mv" "$MV" \
26
+ --replace-quiet "/bin/cp" "$CP";
26
27
done
27
28
'' ;
28
29
29
30
buildFlags = [ "all" ] ;
30
31
31
- checkPhase = "make test1" ;
32
+ # Fails the build on clang-16 and gcc-14.
33
+ env . NIX_CFLAGS_COMPILE = "-Wno-error=implicit-int" ;
34
+
35
+ doCheck = true ;
36
+ checkPhase = ''
37
+ runHook preCheck
38
+
39
+ make test1
40
+ make test2
41
+ make test3
42
+
43
+ runHook postCheck
44
+ '' ;
32
45
33
46
installPhase = ''
47
+ runHook preInstall
34
48
mkdir -p $out/bin
35
- cp bin/* $out/bin
49
+ for f in mace4 prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr; do
50
+ install -Dm555 bin/$f $out/bin/$f;
51
+ done
52
+ install -Dm644 -t $out/share/man/man1 manpages/*.1
53
+ runHook postInstall
36
54
'' ;
37
55
38
- meta = with lib ; {
56
+ nativeInstallCheckInputs = [
57
+ versionCheckHook
58
+ ] ;
59
+ doInstallCheck = true ;
60
+
61
+ meta = {
39
62
homepage = "https://www.cs.unm.edu/~mccune/mace4/" ;
40
- license = licenses . gpl2Only ;
63
+ license = lib . licenses . gpl2Only ;
41
64
description = "Automated theorem prover for first-order and equational logic" ;
42
65
longDescription = ''
43
66
Prover9 is a resolution/paramodulation automated theorem prover
44
67
for first-order and equational logic. Prover9 is a successor of
45
68
the Otter Prover. This is the LADR command-line version.
46
69
'' ;
47
- platforms = platforms . linux ;
70
+ mainProgram = "prover9" ;
71
+ platforms = lib . platforms . linux ;
48
72
maintainers = [ ] ;
49
73
} ;
50
74
}
0 commit comments