Update hol_light and cleanup:

* Update hol_light to rev 90
* Remove dmtcp checkpoint (it doesn't work properly).
* General cleanup and simplification

svn path=/nixpkgs/trunk/; revision=27290

pkgs/applications/science/logic/hol_light/default.nix

@@ -1,43 +1,36 @@
-{stdenv, writeText, writeTextFile, ocaml, findlib, camlp5_transitional, hol_light_sources}:
+{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}:
 
-let
-  version = hol_light_sources.version;
+stdenv.mkDerivation rec {
+  name = "hol_light-20110423";
+  src = fetchsvn {
+    url = http://hol-light.googlecode.com/svn/trunk;
+    rev = "90";
+    sha256 = "e10f32392eb94de559495f2a2977da9e325ff1f39edbcd28db701a1801566c89";
+  };
 
-  camlp5 = camlp5_transitional;
+  buildInputs = [ ocaml findlib camlp5 ];
 
-  hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src";
+  start_script = ''
+    #!/bin/sh
+    cd "$out/lib/hol_light"
+    exec ${ocaml}/bin/ocaml -I "$(ocamlfind query camlp5)" -init make.ml
+  '';
 
-  pa_j_cmo = stdenv.mkDerivation {
-    name = "pa_j.cmo";
-    inherit ocaml camlp5; 
-    buildInputs = [ ocaml camlp5 findlib ];
-    buildCommand = ''
+  buildPhase = ''
+    make pa_j.ml
     ocamlc -c \
       -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
       -I "$(ocamlfind query camlp5)" \
-        -o $out \
-        "${hol_light_src_dir}/pa_j_`ocamlc -version | cut -c1-4`.ml"
+      pa_j.ml
   '';
-    };
 
-  start_ml = writeText "start.ml" ''
-    Topdirs.dir_directory "${hol_light_src_dir}";;
-    Topdirs.dir_directory ("${camlp5}/lib/ocaml/"^Sys.ocaml_version^"/site-lib/camlp5");;
-    Topdirs.dir_load Format.std_formatter "camlp5o.cma";;
-    Topdirs.dir_load Format.std_formatter "${pa_j_cmo}";;
-    #use "${hol_light_src_dir}/make.ml";;
+  installPhase = ''
+    ensureDir "$out/lib/hol_light" "$out/bin"
+    cp -a  . $out/lib/hol_light
+    echo "${start_script}" > "$out/bin/hol_light"
+    chmod a+x "$out/bin/hol_light"
   '';
-in
-writeTextFile {
-  name = "hol_light-${version}";
-  destination = "/bin/start_hol_light";
-  executable = true;
-  text = ''
-      #!/bin/sh
-      exec ${ocaml}/bin/ocaml -init ${start_ml}
-    '';
-} // {
-  inherit (hol_light_sources) version src;
+
   meta = {
     description = "An interactive theorem prover based on Higher-Order Logic.";
     longDescription = ''

pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix

@@ -1,99 +0,0 @@
-{stdenv, writeTextFile, hol_light, dmtcp}:
-let
-  mkRestartScript = checkpointFile:
-    let filename = "hol_light_${checkpointFile.variant}_dmtcp"; in
-    writeTextFile {
-      name = "${filename}-${hol_light.version}";
-      destination = "/bin/${filename}";
-      executable = true;
-      text = ''
-        #!/bin/sh
-	exec ${dmtcp}/bin/dmtcp_restart --quiet ${checkpointFile}
-      '';
-    };
-
-  mkCkptFile =
-    { variant
-    , banner
-    , loads
-    , startCkpt ? null
-    , buildCommand ? ''
-        cp ${startCkpt} hol_light_restart.ckpt
-        (echo "$loadScript" | dmtcp_restart --quiet hol_light_restart.ckpt) || exit 0
-        cp hol_light_restart.ckpt $out
-      ''
-    }:
-    stdenv.mkDerivation rec {
-      name = "hol_light_${variant}_dmtcp.checkpoint-${hol_light.version}";
-      inherit variant banner buildCommand;
-      buildInputs = [ dmtcp hol_light ];
-      loadScript = ''
-        ${loads}
-        dmtcp_checkpoint "${banner}";;
-      '';
-    };
-in
-rec {
-  hol_light_core_dmtcp = mkRestartScript hol_light_core_dmtcp_ckpt;
-  hol_light_sosa_dmtcp = mkRestartScript hol_light_sosa_dmtcp_ckpt;
-  hol_light_card_dmtcp = mkRestartScript hol_light_card_dmtcp_ckpt;
-  hol_light_multivariate_dmtcp = mkRestartScript hol_light_multivariate_dmtcp_ckpt;
-  hol_light_complex_dmtcp = mkRestartScript hol_light_complex_dmtcp_ckpt;
-
-  hol_light_core_dmtcp_ckpt = mkCkptFile rec {
-    variant = "core";
-    banner = "";
-    loads = ''
-      #use "${./dmtcp_selfdestruct.ml}";;
-    '';
-    buildCommand = ''
-      (echo "$loadScript" | dmtcp_checkpoint --quiet ${hol_light}/bin/start_hol_light) || exit 0
-      mv ckpt* $out
-    '';
-  };
-
-  hol_light_multivariate_dmtcp_ckpt = mkCkptFile {
-    variant = "multivariate";
-    banner = "Preloaded with multivariate analysis";
-    loads = ''
-      loadt "Multivariate/make.ml";;
-    '';
-    startCkpt = hol_light_core_dmtcp_ckpt;
-  };
-
-  hol_light_sosa_dmtcp_ckpt = mkCkptFile {
-    variant = "sosa";
-    banner = "Preloaded with analysis and SOS";
-    loads = ''
-      loadt "Library/analysis.ml";;
-      loadt "Library/transc.ml";;
-      loadt "Examples/sos.ml";;
-      loadt "update_database.ml";;
-    '';
-    startCkpt = hol_light_core_dmtcp_ckpt;
-  };
-
-  hol_light_card_dmtcp_ckpt = mkCkptFile {
-    variant = "card";
-    banner = "Preloaded with cardinal arithmetic";
-    loads = ''
-      loadt "Library/card.ml";;
-      loadt "update_database.ml";;
-    '';
-    startCkpt = hol_light_core_dmtcp_ckpt;
-  };
-
-  hol_light_complex_dmtcp_ckpt = mkCkptFile {
-    variant = "complex";
-    banner = "Preloaded with multivariate-based complex analysis";
-    loads = ''
-      loadt "Multivariate/complexes.ml";;
-      loadt "Multivariate/canal.ml";;
-      loadt "Multivariate/transcendentals.ml";;
-      loadt "Multivariate/realanalysis.ml";;
-      loadt "Multivariate/cauchy.ml";;
-      loadt "Multivariate/complex_database.ml";;
-    '';
-    startCkpt = hol_light_multivariate_dmtcp_ckpt;
-  };
-}

pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml

@@ -1,19 +0,0 @@
-(* ------------------------------------------------------------------------- *)
-(* Create a standalone HOL image. Assumes that we are running under Linux    *)
-(* and have the program "dmtcp" available to create checkpoints.             *)
-(* ------------------------------------------------------------------------- *)
-
-let dmtcp_checkpoint, dmtcp_selfdestruct =
-  let call_dmtcp opts bannerstring =
-    let longer_banner = startup_banner ^ " with DMTCP" in
-    let complete_banner =
-      if bannerstring = "" then longer_banner
-      else longer_banner^"\n        "^bannerstring in
-    (Gc.compact(); Unix.sleep 1;
-     Format.print_string "Checkpointing..."; Format.print_newline();
-     try ignore(Unix.system ("dmtcp_command -bc " ^ opts))
-     with Unix.Unix_error _ -> ();
-     Format.print_string complete_banner;
-     Format.print_newline(); Format.print_newline())
-  in
-  call_dmtcp "", call_dmtcp "-q";;

pkgs/applications/science/logic/hol_light/parser_setup.patch

@@ -1,34 +0,0 @@
-diff -Nuar hol_light/hol.ml hol_light.nixos/hol.ml
---- hol_light/hol.ml	2010-11-03 23:09:01.000000000 +0100
-+++ hol_light.nixos/hol.ml	2010-11-03 23:10:31.000000000 +0100
-@@ -11,8 +11,8 @@
- 
- let hol_version = "2.20++";;
- 
--let hol_dir = ref
--  (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
-+let hol_dir = ref "@HOL_LIGHT_SRC_DIR@";;
-+Topdirs.dir_directory "@HOL_LIGHT_SRC_DIR@";;
- 
- (* ------------------------------------------------------------------------- *)
- (* Should eventually change to "ref(Filename.temp_dir_name)".                *)
-@@ -23,19 +23,6 @@
- let temp_path = ref "/tmp";;
- 
- (* ------------------------------------------------------------------------- *)
--(* Load in parsing extensions.                                               *)
--(* For Ocaml < 3.10, use the built-in camlp4                                 *)
--(* and for Ocaml >= 3.10, use camlp5 instead.                                *)
--(* ------------------------------------------------------------------------- *)
--
--if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
--then (Topdirs.dir_directory "+camlp5";
--      Topdirs.dir_load Format.std_formatter "camlp5o.cma")
--else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
--
--Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
--
--(* ------------------------------------------------------------------------- *)
- (* Load files from system and/or user-settable directories.                  *)
- (* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual  *)
- (* $ character at the start of a directory.                                  *)

pkgs/applications/science/logic/hol_light/sources.nix

@@ -1,28 +0,0 @@
-{stdenv, fetchsvn}:
-
-stdenv.mkDerivation rec {
-  name = "hol_light_sources-${version}";
-  version = "20110417";
-
-  src = fetchsvn {
-    url = http://hol-light.googlecode.com/svn/trunk;
-    rev = "89";
-    sha256 = "a14a7ce61002443daac85583362f9f6f5509b22d441effaeb378e0f2c29185e5";
-  };
-
-  buildCommand = ''
-    export HOL_DIR="$out/lib/hol_light"
-    ensureDir "$HOL_DIR"
-    cp -a "${src}" "$HOL_DIR/src"
-    cd "$HOL_DIR/src"
-    chmod +wX -R .
-    patch -p1 < ${./parser_setup.patch}
-    substituteInPlace hol.ml --subst-var-by HOL_LIGHT_SRC_DIR "$HOL_DIR/src"
-  '';
-
-  meta = {
-    description = "Sources for the HOL Light theorem prover";
-    homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
-    license = "BSD";
-  };
-}

pkgs/top-level/all-packages.nix

@@ -7649,14 +7649,10 @@ let
   hol = callPackage ../applications/science/logic/hol { };
 
   hol_light = callPackage ../applications/science/logic/hol_light {
-    inherit (ocamlPackages) findlib camlp5_transitional;
+    inherit (ocamlPackages) findlib;
+    camlp5 = ocamlPackages.camlp5_strict;
   };
 
-  hol_light_sources = callPackage ../applications/science/logic/hol_light/sources.nix { };
-
-  hol_light_checkpoint_dmtcp =
-     recurseIntoAttrs (callPackage ../applications/science/logic/hol_light/dmtcp_checkpoint.nix { });
-
   isabelle = import ../applications/science/logic/isabelle {
     inherit (pkgs) stdenv fetchurl nettools perl polyml;
     inherit (pkgs.emacs23Packages) proofgeneral;