tjh.dev
1{
2 lib,
3 stdenv,
4 fetchurl,
5 versionCheckHook,
6}:
7
8stdenv.mkDerivation {
9 pname = "prover9";
10 version = "2009-11A";
11
12 src = fetchurl {
13 url = "https://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz";
14 hash = "sha256-wyvtWAcADAtxYcJ25Q2coK8MskjfLBr/svb8AkcbUdA=";
15 };
16
17 hardeningDisable = [ "format" ];
18
19 postPatch = ''
20 RM=$(type -tp rm)
21 MV=$(type -tp mv)
22 CP=$(type -tp cp)
23 for f in Makefile */Makefile; do
24 substituteInPlace $f --replace-quiet "/bin/rm" "$RM" \
25 --replace-quiet "/bin/mv" "$MV" \
26 --replace-quiet "/bin/cp" "$CP";
27 done
28 '';
29
30 buildFlags = [ "all" ];
31
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 '';
45
46 installPhase = ''
47 runHook preInstall
48 mkdir -p $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
54 '';
55
56 nativeInstallCheckInputs = [
57 versionCheckHook
58 ];
59 doInstallCheck = true;
60
61 meta = {
62 homepage = "https://www.cs.unm.edu/~mccune/mace4/";
63 license = lib.licenses.gpl2Only;
64 description = "Automated theorem prover for first-order and equational logic";
65 longDescription = ''
66 Prover9 is a resolution/paramodulation automated theorem prover
67 for first-order and equational logic. Prover9 is a successor of
68 the Otter Prover. This is the LADR command-line version.
69 '';
70 mainProgram = "prover9";
71 platforms = lib.platforms.linux;
72 maintainers = [ ];
73 };
74}