From 970b3402e9062668c8679e8297303103f1513899 Mon Sep 17 00:00:00 2001
From: Peter Simons <simons@cryp.to>
Date: Wed, 25 Aug 2010 19:50:24 +0000
Subject: [PATCH] pkgs/applications/science/logic/hol: initial version

svn path=/nixpkgs/trunk/; revision=23430
---
 .../science/logic/hol/default.nix             | 55 +++++++++++++++++++
 pkgs/top-level/all-packages.nix               |  2 +
 2 files changed, 57 insertions(+)
 create mode 100644 pkgs/applications/science/logic/hol/default.nix

diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
new file mode 100644
index 000000000000..63040b7fdd52
--- /dev/null
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -0,0 +1,55 @@
+{stdenv, fetchurl, polyml}:
+
+stdenv.mkDerivation {
+  name = "hol";
+
+  src = fetchurl {
+    #url = "http://downloads.sourceforge.net/project/hol/hol/kananaskis-5/kananaskis-5.tar.gz";
+    url = mirror://sourceforge/hol/hol/kananaskis-5/kananaskis-5.tar.gz;
+    sha256 = "1qjfx5ii80v17yr04hz70n8aa46892fjc4qcxs9gs7nh3hw7rvmx";
+  };
+
+  buildInputs = [polyml];
+
+  buildCommand = ''
+    ensureDir "$out/src"
+    cd  "$out/src"
+
+    tar -xzf "$src"
+    cd hol
+
+    substituteInPlace tools-poly/Holmake/Holmake.sml --replace \
+      "\"/bin/mv\"" \
+      "\"mv\""
+
+    #sed -ie "/compute/,999 d" tools/build-sequence # for testing
+
+    poly < tools/smart-configure.sml
+    
+    bin/build -expk -symlink
+
+    ensureDir "$out/bin"
+    ln -st $out/bin  $out/src/hol/bin/*
+    # ln -s $out/src/hol/bin $out/bin
+  '';
+
+  meta = {
+    description = "HOL4, an 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
+      implemented. Built-in decision procedures and theorem provers
+      can automatically establish many simple theorems (users may have
+      to prove the hard theorems themselves!) An oracle mechanism
+      gives access to external programs such as SMT and BDD
+      engines. HOL4 is particularly suitable as a platform for
+      implementing combinations of deduction, execution and property
+      checking.
+
+    '';
+    homepage = "http://hol.sourceforge.net/";
+    license = "BSD";
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 8775ba7b76d3..7ea75b48faf1 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6759,6 +6759,8 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  hol = callPackage ../applications/science/logic/hol { };
+
   hol_light = callPackage ../applications/science/logic/hol_light { };
 
   hol_light_binaries = callPackage ../applications/science/logic/hol_light/binaries.nix { };