tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 stdenv,
4 pkgs,
5 fetchurl,
6 graphviz,
7 fontconfig,
8 liberation_ttf,
9 experimentalKernel ? true,
10}:
11
12let
13 pname = "hol4";
14 vnum = "14";
15
16 version = "k.${vnum}";
17 longVersion = "kananaskis-${vnum}";
18 holsubdir = "hol-${longVersion}";
19 kernelFlag = if experimentalKernel then "--expk" else "--stdknl";
20
21 polymlEnableShared =
22 with pkgs;
23 lib.overrideDerivation polyml (attrs: {
24 configureFlags = [ "--enable-shared" ];
25 });
26in
27
28stdenv.mkDerivation {
29 name = "${pname}-${version}";
30
31 src = fetchurl {
32 url = "mirror://sourceforge/hol/hol/${longVersion}/${holsubdir}.tar.gz";
33 sha256 = "6Mc/qsEjzxGqzt6yP6x/1Tmqpwc1UDGlwV1Gl+4pMsY=";
34 };
35
36 buildInputs = [
37 polymlEnableShared
38 graphviz
39 fontconfig
40 liberation_ttf
41 ];
42
43 buildCommand = ''
44
45 mkdir chroot-fontconfig
46 cat ${fontconfig.out}/etc/fonts/fonts.conf > chroot-fontconfig/fonts.conf
47 sed -e 's@</fontconfig>@@' -i chroot-fontconfig/fonts.conf
48 echo "<dir>${liberation_ttf}</dir>" >> chroot-fontconfig/fonts.conf
49 echo "</fontconfig>" >> chroot-fontconfig/fonts.conf
50
51 export FONTCONFIG_FILE=$(pwd)/chroot-fontconfig/fonts.conf
52
53 mkdir -p "$out/src"
54 cd "$out/src"
55
56 tar -xzf "$src"
57 cd ${holsubdir}
58
59 substituteInPlace tools/Holmake/Holmake_types.sml \
60 --replace "\"/bin/" "\"" \
61
62
63 for f in tools/buildutils.sml help/src-sml/DOT;
64 do
65 substituteInPlace $f --replace "\"/usr/bin/dot\"" "\"${graphviz}/bin/dot\""
66 done
67
68 #sed -i -e "/compute/,999 d" tools/build-sequence # for testing
69
70 poly < tools/smart-configure.sml
71
72 bin/build ${kernelFlag}
73
74 mkdir -p "$out/bin"
75 ln -st $out/bin $out/src/${holsubdir}/bin/*
76 # ln -s $out/src/hol4.${version}/bin $out/bin
77 '';
78
79 meta = with lib; {
80 broken = (stdenv.hostPlatform.isLinux && stdenv.hostPlatform.isAarch64);
81 description = "Interactive theorem prover based on Higher-Order Logic";
82 longDescription = ''
83 HOL4 is the latest version of the HOL interactive proof
84 assistant for higher order logic: a programming environment in
85 which theorems can be proved and proof tools
86 implemented. Built-in decision procedures and theorem provers
87 can automatically establish many simple theorems (users may have
88 to prove the hard theorems themselves!) An oracle mechanism
89 gives access to external programs such as SMT and BDD
90 engines. HOL4 is particularly suitable as a platform for
91 implementing combinations of deduction, execution and property
92 checking.
93 '';
94 homepage = "http://hol.sourceforge.net/";
95 license = licenses.bsd3;
96 platforms = platforms.unix;
97 maintainers = with maintainers; [ mudri ];
98 };
99}