1 files changed, 25 insertions, 11 deletions
diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index 18a16114c507..2e1647b6c71d 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -1,8 +1,10 @@
-{stdenv, fetchurl, polyml, experimentalKernel ? false}:
+{stdenv, fetchurl, polyml, graphviz, fontconfig, liberation_ttf,
+ experimentalKernel ? true}:
 
 let
   pname = "hol4";
-  version = "k.7";
+  version = "k.8";
+  holsubdir = "hol-kananaskis-8";
   kernelFlag = if experimentalKernel then "-expk" else "-stdknl";
 in
 
@@ -10,38 +12,51 @@ stdenv.mkDerivation {
   name = "${pname}-${version}";
 
   src = fetchurl {
-    url = mirror://sourceforge/hol/hol/kananaskis-7/kananaskis-7.tar.gz;
-    sha256 = "0gs1nmjvsjhnndama9v7gids2g86iip53v7d7dm3sfq6jxmqkwkl";
+    url = mirror://sourceforge/hol/hol/kananaskis-8/kananaskis-8.tar.gz;
+    sha256 = "5ce4c1e37301dbc38772694e98f1c7eabf69255908de204b280d8b2b1709e9d0";
   };
 
-  buildInputs = [polyml];
+  buildInputs = [polyml graphviz fontconfig liberation_ttf];
 
   buildCommand = ''
+
+    mkdir chroot-fontconfig
+    cat ${fontconfig}/etc/fonts/fonts.conf > chroot-fontconfig/fonts.conf
+    sed -e 's@</fontconfig>@@' -i chroot-fontconfig/fonts.conf
+    echo "<dir>${liberation_ttf}</dir>" >> chroot-fontconfig/fonts.conf
+    echo "</fontconfig>" >> chroot-fontconfig/fonts.conf
+
+    export FONTCONFIG_FILE=$(pwd)/chroot-fontconfig/fonts.conf
+
     mkdir -p "$out/src"
     cd  "$out/src"
 
     tar -xzf "$src"
-    cd hol4.${version}
+    cd ${holsubdir}
 
     substituteInPlace tools/Holmake/Holmake_types.sml \
       --replace "\"/bin/mv\"" "\"mv\"" \
       --replace "\"/bin/cp\"" "\"cp\""
 
+    for f in tools/buildutils.sml help/src-sml/DOT;
+    do
+      substituteInPlace $f --replace "\"/usr/bin/dot\"" "\"${graphviz}/bin/dot\""
+    done
+
     #sed -ie "/compute/,999 d" tools/build-sequence # for testing
 
     poly < tools/smart-configure.sml
-    
+
     bin/build ${kernelFlag} -symlink
 
     mkdir -p "$out/bin"
-    ln -st $out/bin  $out/src/hol4.${version}/bin/*
+    ln -st $out/bin  "$out/src/${holsubdir}/bin/"*
     # ln -s $out/src/hol4.${version}/bin $out/bin
   '';
 
   meta = {
-    description = "HOL4, an interactive theorem prover based on Higher-Order Logic.";
+    description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
-
       HOL4 is the latest version of the HOL interactive proof
       assistant for higher order logic: a programming environment in
       which theorems can be proved and proof tools
@@ -52,7 +67,6 @@ stdenv.mkDerivation {
       engines. HOL4 is particularly suitable as a platform for
       implementing combinations of deduction, execution and property
       checking.
-
     '';
     homepage = "http://hol.sourceforge.net/";
     license = "BSD";