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 inherit 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 = {
80 description = "Interactive theorem prover based on Higher-Order Logic";
81 longDescription = ''
82 HOL4 is the latest version of the HOL interactive proof
83 assistant for higher order logic: a programming environment in
84 which theorems can be proved and proof tools
85 implemented. Built-in decision procedures and theorem provers
86 can automatically establish many simple theorems (users may have
87 to prove the hard theorems themselves!) An oracle mechanism
88 gives access to external programs such as SMT and BDD
89 engines. HOL4 is particularly suitable as a platform for
90 implementing combinations of deduction, execution and property
91 checking.
92 '';
93 homepage = "http://hol.sourceforge.net/";
94 license = lib.licenses.bsd3;
95 platforms = lib.platforms.unix;
96 maintainers = with lib.maintainers; [ mudri ];
97 };
98}