From 0f1f2115e91edb65ad3b4edea08ffeb96665a5c1 Mon Sep 17 00:00:00 2001
From: Austin Seipp <aseipp@pobox.com>
Date: Sun, 27 Apr 2014 13:25:19 -0500
Subject: [PATCH] hol_light: fix script, upgrade to r189

This also tweaks the version number to just use the SVN revision (rather
than date), since it's unambiguous and increasing anyway.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
---
 .../editors/emacs-modes/hol_light/default.nix | 19 +++++++------
 .../science/logic/hol_light/default.nix       | 28 ++++++++-----------
 2 files changed, 21 insertions(+), 26 deletions(-)

diff --git a/pkgs/applications/editors/emacs-modes/hol_light/default.nix b/pkgs/applications/editors/emacs-modes/hol_light/default.nix
index 24eba20be6cc..c32669239f88 100644
--- a/pkgs/applications/editors/emacs-modes/hol_light/default.nix
+++ b/pkgs/applications/editors/emacs-modes/hol_light/default.nix
@@ -1,15 +1,12 @@
-{stdenv, fetchsvn}:
+{ stdenv, fetchsvn }:
 
-let
-  revision = "73";
-in
-
-stdenv.mkDerivation {
-  name = "hol_light_mode-${revision}";
+stdenv.mkDerivation rec {
+  name    = "hol_light-mode-${version}";
+  version = "73";
 
   src = fetchsvn {
     url = http://seanmcl-ocaml-lib.googlecode.com/svn/trunk/workshop/software/emacs;
-    rev = revision;
+    rev = version;
     sha256 = "3ca83098960439da149a47e1caff32536601559a77f04822be742a390c67feb7";
   };
 
@@ -20,6 +17,10 @@ stdenv.mkDerivation {
   '';
 
   meta = {
-    description = "A HOL Light mode for emacs";
+    description = "A HOL Light mode for Emacs";
+    homepage    = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+    license     = stdenv.lib.licenses.gpl2Plus;
+    platforms   = stdenv.lib.platforms.all;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 54c7174bde7f..3e6440ea9773 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,19 +1,20 @@
-{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}:
+{ stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5 }:
 
 let
   start_script = ''
     #!/bin/sh
     cd "$out/lib/hol_light"
-    exec ${ocaml}/bin/ocaml -I "camlp5 -where" -init make.ml
+    exec ${ocaml}/bin/ocaml -I \`${camlp5}/bin/camlp5 -where\` -init make.ml
   '';
 in
+stdenv.mkDerivation rec {
+  name     = "hol_light-${version}";
+  version  = "189";
 
-stdenv.mkDerivation {
-  name = "hol_light-20140112";
   src = fetchsvn {
     url = http://hol-light.googlecode.com/svn/trunk;
-    rev = "179";
-    sha256 = "1j402s7142fj09bjijrkargwx03fvbdwmn0hgzzmi6s4p1y7gww0";
+    rev = version;
+    sha256 = "1v10l64rs7da2kag3wlb651i09pn83icy9n5z84j8h1iwlxzajdh";
   };
 
   buildInputs = [ ocaml findlib camlp5 ];
@@ -27,16 +28,9 @@ stdenv.mkDerivation {
 
   meta = {
     description = "Interactive theorem prover based on Higher-Order Logic";
-    longDescription = ''
-      HOL Light is a computer program to help users prove interesting
-      mathematical theorems completely formally in Higher-Order Logic.  It sets
-      a very exacting standard of correctness, but provides a number of
-      automated tools and pre-proved mathematical theorems (e.g., about
-      arithmetic, basic set theory and real analysis) to save the user work.
-      It is also fully programmable, so users can extend it with new theorems
-      and inference rules without compromising its soundness.
-    '';
-    homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
-    license = stdenv.lib.licenses.bsd2;
+    homepage    = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+    license     = stdenv.lib.licenses.bsd2;
+    platforms   = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
 }