From 723cd518b9a29be5e1c5f0015aa4a1563af830ac Mon Sep 17 00:00:00 2001
From: laMudri <lamudri@gmail.com>
Date: Tue, 23 Jun 2015 23:17:51 +0100
Subject: [PATCH] hol: k.8 -> k.10, closes #8477

---
 .../science/logic/hol/default.nix             | 30 +++++++++++++------
 1 file changed, 21 insertions(+), 9 deletions(-)

diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index a7cdf7f3097d..f8a57aebb6dc 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -1,22 +1,33 @@
-{stdenv, fetchurl, polyml, graphviz, fontconfig, liberation_ttf,
+{stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf,
  experimentalKernel ? true}:
 
 let
   pname = "hol4";
-  version = "k.8";
-  holsubdir = "hol-kananaskis-8";
+  vnum = "10";
+in
+
+let
+  version = "k.${vnum}";
+  longVersion = "kananaskis-${vnum}";
+  holsubdir = "hol-${longVersion}";
   kernelFlag = if experimentalKernel then "-expk" else "-stdknl";
 in
 
+let
+  polymlEnableShared = with pkgs; lib.overrideDerivation polyml (attrs: {
+    configureFlags = "--enable-shared";
+  });
+in
+
 stdenv.mkDerivation {
   name = "${pname}-${version}";
 
   src = fetchurl {
-    url = mirror://sourceforge/hol/hol/kananaskis-8/kananaskis-8.tar.gz;
-    sha256 = "5ce4c1e37301dbc38772694e98f1c7eabf69255908de204b280d8b2b1709e9d0";
+    url = "mirror://sourceforge/hol/hol/${longVersion}/${holsubdir}.tar.gz";
+    sha256 = "0x2wxksr305h1lrbklf6p42lp09rbhb4rsh74g0l70sgapyiac9b";
   };
 
-  buildInputs = [polyml graphviz fontconfig liberation_ttf];
+  buildInputs = [polymlEnableShared graphviz fontconfig liberation_ttf];
 
   buildCommand = ''
 
@@ -46,7 +57,7 @@ stdenv.mkDerivation {
     #sed -ie "/compute/,999 d" tools/build-sequence # for testing
 
     poly < tools/smart-configure.sml
-    
+
     bin/build ${kernelFlag} -symlink
 
     mkdir -p "$out/bin"
@@ -54,7 +65,7 @@ stdenv.mkDerivation {
     # ln -s $out/src/hol4.${version}/bin $out/bin
   '';
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
       HOL4 is the latest version of the HOL interactive proof
@@ -69,6 +80,7 @@ stdenv.mkDerivation {
       checking.
     '';
     homepage = "http://hol.sourceforge.net/";
-    license = stdenv.lib.licenses.bsd3;
+    license = licenses.bsd3;
+    maintainers = with maintainers; [ mudri ];
   };
 }