Update HOL Light to version 20100820 (rev57 on google code).

Also replace the monolitic derivation hol_light_binaries with smaller
derivations.  Now the installation works as follows:

# Install the base system and a script "start_hol_light"
$ nix-env -i hol_light_sources hol_light

# Install a checkpointed executable with the core library preloaded
$ nix-env -i hol_light_core_dmtcp

# Install HOL Light binaries preloaded with other specific libraries:
$ nix-env -i hol_light_multivariate_dmtcp
$ nix-env -i hol_light_complex_dmtcp
$ nix-env -i hol_light_sosa_dmtcp
$ nix-env -i hol_light_card_dmtcp


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

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

@@ -1,60 +0,0 @@
-{stdenv, hol_light, dmtcp}:
-
-let
-  cmd_core = ''
-    #use "${./start_hol.ml}";;
-    dmtcp_selfdestruct "";;
-  '';
-  cmd_multivariate = ''
-    loadt "Multivariate/make.ml";;
-    dmtcp_checkpoint "Preloaded with multivariate analysis";;
-  '';
-  cmd_complex = ''
-    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";;
-    loadt "update_database.ml";;
-    dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;
-  '';
-in
-
-stdenv.mkDerivation {
-  name = "hol_light_binaries-${hol_light.version}";
-
-  buildInputs = [ dmtcp hol_light hol_light.ocaml ];
-
-  buildCommand = ''
-    HOL_DIR="${hol_light}/src/hol_light"
-    BIN_DIR="$out/bin"
-    ensureDir "$BIN_DIR"
-
-    # HOL Light Core
-    (echo '${cmd_core}' | dmtcp_checkpoint --quiet ${hol_light}/bin/start_hol_light) || exit 0
-    mv ckpt* "$BIN_DIR/hol_light.ckpt"
-    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light" \
-      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light.ckpt"
-    chmod +x "$BIN_DIR/hol_light"
-
-    # HOL Light Multivariate
-    cp "$BIN_DIR/hol_light.ckpt" .
-    (echo '${cmd_multivariate}' | dmtcp_restart --quiet hol_light.ckpt) || exit 0
-    mv hol_light.ckpt "$BIN_DIR/hol_light_multivariate.ckpt"
-    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_multivariate" \
-      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_multivariate.ckpt"
-    chmod +x "$BIN_DIR/hol_light_multivariate"
-
-    # HOL Light Complex
-    cp "$BIN_DIR/hol_light_multivariate.ckpt" .
-    (echo '${cmd_complex}' | dmtcp_restart --quiet hol_light_multivariate.ckpt) || exit 0
-    mv hol_light_multivariate.ckpt "$BIN_DIR/hol_light_complex.ckpt"
-    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_complex" \
-      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_complex.ckpt"
-    chmod +x "$BIN_DIR/hol_light_complex"
-  '';
-}

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

@@ -1,44 +1,43 @@
-{stdenv, fetchsvn, ocaml, camlp5_transitional}:
+{stdenv, writeText, writeTextFile, ocaml, camlp5_transitional, hol_light_sources}:
 
-stdenv.mkDerivation rec {
+let
-  name = "hol_light-${version}";
+  version = hol_light_sources.version;
-  version = "20100820svn57";
 
-  inherit ocaml;
   camlp5 = camlp5_transitional;
 
-  src = fetchsvn {
+  hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src";
-    url = http://hol-light.googlecode.com/svn/trunk;
+
-    rev = "57";
+  pa_j_cmo = stdenv.mkDerivation {
-    sha256 = "d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
+    name = "pa_j.cmo";
+    inherit ocaml camlp5; 
+    buildInputs = [ ocaml camlp5 ];
+    buildCommand = ''
+      ocamlc -c \
+        -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
+        -I "${camlp5}/lib/ocaml/camlp5" \
+        -o $out \
+        "${hol_light_src_dir}/pa_j_`ocamlc -version | cut -c1-4`.ml"
+      '';
     };
 
-  buildInputs = [ ocaml camlp5 ];
+  start_ml = writeText "start.ml" ''
-
+    Topdirs.dir_directory "${hol_light_src_dir}";;
-  buildCommand = ''
+    Topdirs.dir_directory "${camlp5}/lib/ocaml/camlp5";;
-    export HOL_DIR="$out/src/hol_light"
+    Topdirs.dir_load Format.std_formatter "camlp5o.cma";;
-    ensureDir `dirname $HOL_DIR` "$out/bin"
+    Topdirs.dir_load Format.std_formatter "${pa_j_cmo}";;
-    cp -a "${src}" "$HOL_DIR"
+    #use "${hol_light_src_dir}/make.ml";;
-    cd "$HOL_DIR"
-    chmod -R u+rwX .
-
-    substituteInPlace hol.ml --replace \
-      "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
-      "\"$HOL_DIR\""
-
-    substituteInPlace Makefile --replace \
-      "+camlp5" \
-      "${camlp5}/lib/ocaml/camlp5"
-
-    substitute ${./start_hol_light} "$out/bin/start_hol_light" \
-      --subst-var-by OCAML "${ocaml}" \
-      --subst-var-by CAMLP5 "${camlp5_transitional}" \
-      --subst-var HOL_DIR
-    chmod +x "$out/bin/start_hol_light"
-
-    make
   '';
-
+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 = ''
@@ -52,6 +51,5 @@ soundness.
     '';
     homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
     license = "BSD";
-    ocamlVersions = [ "3.10.0" "3.11.1" ];
   };
 }

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

@@ -0,0 +1,99 @@
+{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

@@ -0,0 +1,19 @@
+(* ------------------------------------------------------------------------- *)
+(* 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

@@ -0,0 +1,35 @@
+diff -Nuar hol_light/hol.ml hol_light.nixos/hol.ml
+--- hol_light/hol.ml	2010-09-12 18:57:28.000000000 +0200
++++ hol_light.nixos/hol.ml	2010-09-12 19:09:09.000000000 +0200
+@@ -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,20 +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" or v = "3.11"
+-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/restart_hol_light

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-exec @DMTCP_RESTART@ --quiet @CKPT_FILE@

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

@@ -0,0 +1,28 @@
+{stdenv, fetchsvn}:
+
+stdenv.mkDerivation rec {
+  name = "hol_light_sources-${version}";
+  version = "20100820";
+
+  src = fetchsvn {
+    url = http://hol-light.googlecode.com/svn/trunk;
+    rev = "57";
+    sha256 = "d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
+  };
+
+  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/applications/science/logic/hol_light/start_hol.ml

@@ -1,37 +0,0 @@
-(* ========================================================================= *)
-(* Create a standalone HOL image. Assumes that we are running under Linux    *)
-(* and have the program "dmtcp" available to create checkpoints.             *)
-(*                                                                           *)
-(*              (c) Copyright, John Harrison 1998-2007                       *)
-(*              (c) Copyright, Marco Maggesi 2010                            *)
-(* ========================================================================= *)
-
-(* Use this instead of #use "make.ml";; for quick tests. *)
-(*
-let a = 1;
-#load "unix.cma";;
-let startup_banner = "Bogus banner\n";;
-Format.print_string "Hello!"; Format.print_newline();;
-*)
-
-#use "make.ml";;
-
-(* ------------------------------------------------------------------------- *)
-(* Checkpoint using DMTCP.                                                   *)
-(* dmtcp_selfdestruct is similar to dmtcp_checkpoint but terminates          *)
-(* HOL Light and shuts down the dmtcp coordinator.                           *)
-(* ------------------------------------------------------------------------- *)
-
-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 4;
-     Format.print_string "Checkpointing..."; Format.print_newline();
-     try ignore(Unix.system ("dmtcp_command -bc " ^ opts)) with _ -> ();
-     Format.print_string complete_banner;
-     Format.print_newline(); Format.print_newline())
-  in
-  call_dmtcp "", call_dmtcp "-q";;

pkgs/applications/science/logic/hol_light/start_hol_light

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-exec @OCAML@/bin/ocaml -I @CAMLP5@/lib/ocaml/camlp5 -I @HOL_DIR@ "$@"

pkgs/top-level/all-packages.nix

@@ -6691,7 +6691,10 @@ let
 
   hol_light = callPackage ../applications/science/logic/hol_light { };
 
-  hol_light_binaries = callPackage ../applications/science/logic/hol_light/binaries.nix { };
+  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;