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>

1 files changed, 11 insertions, 17 deletions

diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 54c7174bde7..3e6440ea977 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 ];
   };
 }