Improve hol_light:

*   Upgrade hol_light to the latest svn version on google code (r57).

  *   Improve and semplify the mechanism for the generation of checkpointed binaries.

  *   Make hol to work with camlp5 and thus with recent version of ocaml (>=3.10, <=3.11).

  *   Remove ocaml_with_sources which is not needed anymore.

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

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

@@ -1,55 +1,60 @@
-{stdenv, ocaml_with_sources, hol_light, dmtcp, nettools, openssh}:
+{stdenv, hol_light, dmtcp}:
-# nettools and openssh needed for dmtcp restarting script.
 
 let
-  selfcheckpoint_core_ml = ./selfcheckpoint_core.ml;
+  cmd_core = ''
-  selfcheckpoint_multivariate_ml = ./selfcheckpoint_multivariate.ml;
+    #use "${./start_hol.ml}";;
-  selfcheckpoint_complex_ml = ./selfcheckpoint_complex.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 ocaml_with_sources nettools openssh];
+  buildInputs = [ dmtcp hol_light hol_light.ocaml ];
 
   buildCommand = ''
-    HOL_DIR=${hol_light}/src/hol_light
+    HOL_DIR="${hol_light}/src/hol_light"
-    BIN_DIR=$out/bin
+    BIN_DIR="$out/bin"
-    ensureDir $BIN_DIR
+    ensureDir "$BIN_DIR"
 
     # HOL Light Core
-    dmtcp_coordinator --background
+    (echo '${cmd_core}' | dmtcp_checkpoint --quiet ${hol_light}/bin/start_hol_light) || exit 0
-    echo 'Unix.system "dmtcp_command -k";;\n' |
+    mv ckpt* "$BIN_DIR/hol_light.ckpt"
-      dmtcp_checkpoint -q -c "$BIN_DIR" \
+    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light" \
-        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_core_ml}
+      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-    substituteInPlace dmtcp_restart_script.sh \
+      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light.ckpt"
-      --replace dmtcp_restart "dmtcp_restart --quiet"
+    chmod +x "$BIN_DIR/hol_light"
-    mv dmtcp_restart_script.sh $BIN_DIR/hol_light
-    dmtcp_command -q
 
     # HOL Light Multivariate
-    dmtcp_coordinator --background
+    cp "$BIN_DIR/hol_light.ckpt" .
-    echo 'Unix.system "dmtcp_command -k";;\n' |
+    (echo '${cmd_multivariate}' | dmtcp_restart --quiet hol_light.ckpt) || exit 0
-      dmtcp_checkpoint -q -c "$BIN_DIR" \
+    mv hol_light.ckpt "$BIN_DIR/hol_light_multivariate.ckpt"
-        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_multivariate_ml}
+    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_multivariate" \
-    substituteInPlace dmtcp_restart_script.sh \
+      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-      --replace dmtcp_restart "dmtcp_restart --quiet"
+      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_multivariate.ckpt"
-    mv dmtcp_restart_script.sh $BIN_DIR/hol_light_multivariate
+    chmod +x "$BIN_DIR/hol_light_multivariate"
-    dmtcp_command -q
 
     # HOL Light Complex
-    dmtcp_coordinator --background
+    cp "$BIN_DIR/hol_light_multivariate.ckpt" .
-    echo 'Unix.system "dmtcp_command -k";;\n' |
+    (echo '${cmd_complex}' | dmtcp_restart --quiet hol_light_multivariate.ckpt) || exit 0
-      dmtcp_checkpoint -q -c "$BIN_DIR" \
+    mv hol_light_multivariate.ckpt "$BIN_DIR/hol_light_complex.ckpt"
-        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_complex_ml}
+    substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_complex" \
-    substituteInPlace dmtcp_restart_script.sh \
+      --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
-      --replace dmtcp_restart "dmtcp_restart --quiet"
+      --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_complex.ckpt"
-    mv dmtcp_restart_script.sh $BIN_DIR/hol_light_complex
+    chmod +x "$BIN_DIR/hol_light_complex"
-    dmtcp_command -q
   '';
-
-  meta = {
-    description = "Preload binaries for HOL Light.";
-    license = "BSD";
-  };
 }

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

@@ -1,56 +1,40 @@
-{stdenv, fetchurl, ocaml_with_sources}:
+{stdenv, fetchsvn, ocaml, camlp5_transitional}:
 
-let
+stdenv.mkDerivation rec {
-  pname = "hol_light";
+  name = "hol_light-${version}";
-  version = "100110";
+  version = "20100820svn57";
-  webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
 
-  dmtcp_checkpoint = ''
+  inherit ocaml;
+  camlp5 = camlp5_transitional;
 
-(* ------------------------------------------------------------------------- *)
+  src = fetchsvn {
-(* Non-destructive checkpoint using DMTCP.                                   *)
+    url = http://hol-light.googlecode.com/svn/trunk;
-(* ------------------------------------------------------------------------- *)
+    rev = "57";
-
+    sha256 = "d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
-let dmtcp_checkpoint 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;
-   try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
-   Format.print_string complete_banner;
-   Format.print_newline(); Format.print_newline());;
-  '';
-
-in
-
-stdenv.mkDerivation {
-  name = "${pname}-${version}";
-  inherit version;
-
-  src = fetchurl {
-    url = "${webpage}${pname}_${version}.tgz";
-    sha256 = "1jkn9vpl3n9dgb96zwmly32h1p3f9mcf34pg6vm0fyvqp9kbx3ac";
   };
 
-  buildInputs = [ ocaml_with_sources ];
+  buildInputs = [ ocaml camlp5 ];
 
   buildCommand = ''
-    ensureDir "$out/src"
+    export HOL_DIR="$out/src/hol_light"
-    cd "$out/src"
+    ensureDir `dirname $HOL_DIR` "$out/bin"
-
+    cp -a "${src}" "$HOL_DIR"
-    tar -xzf "$src"
+    cd "$HOL_DIR"
-    cd hol_light
+    chmod -R u+rwX .
 
     substituteInPlace hol.ml --replace \
       "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
-      "\"$out/src/hol_light\""
+      "\"$HOL_DIR\""
 
-    substituteInPlace Examples/update_database.ml --replace \
+    substituteInPlace Makefile --replace \
-      "Filename.concat ocaml_source_dir" \
+      "+camlp5" \
-      "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
+      "${camlp5}/lib/ocaml/camlp5"
 
-    echo '${dmtcp_checkpoint}' >> make.ml
+    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
   '';
@@ -66,7 +50,8 @@ 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 = webpage;
+    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/ocaml-with-sources.nix

@@ -1,33 +0,0 @@
-{stdenv, fetchurl}:
-
-stdenv.mkDerivation {
-  name = "ocaml-with-sources-3.09.3";
-  src = fetchurl {
-    url = http://caml.inria.fr/pub/distrib/ocaml-3.09/ocaml-3.09.3.tar.bz2;
-    sha256 = "607842b4f4917a759f19541a421370a834f5b948855ca54cef40d22b19a0934f";
-  };
-
-  configureScript = ./configure-3.09.3;
-
-  builder = builtins.toFile "builder.sh" ''
-    source $stdenv/setup
-    ensureDir $out/src; cd $out/src
-    tar -xjf $src
-    mv ocaml-* ocaml
-    cd ocaml
-    CAT=$(type -tp cat)
-    sed -e "s@/bin/cat@$CAT@" -i config/auto-aux/sharpbang
-    $configureScript -no-tk -no-curses -prefix $out
-    make opt.opt
-    make install
-  '';
-
-  meta = {
-    description = "ocaml compiler with compiled sources retained.";
-    longDescription = ''
-      TODO
-    '';
-    homepage = http://caml.inria.fr/;
-    license = "LGP with linking exceptions";
-  };
-}

pkgs/applications/science/logic/hol_light/restart_hol_light

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

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

@@ -1,29 +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 "make.ml";;
-
-(* ------------------------------------------------------------------------- *)
-(* Non-destructive checkpoint using DMTCP.                                   *)
-(* ------------------------------------------------------------------------- *)
-
-let checkpoint 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();
-   loadt "Examples/update_database.ml";
-   print_newline ();
-   Unix.sleep 1;
-   try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
-   Format.print_string complete_banner;
-   Format.print_newline(); Format.print_newline());;
-
-loadt "Multivariate/make_complex.ml";;
-dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;

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

@@ -1,28 +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 "make.ml";;
-
-(* ------------------------------------------------------------------------- *)
-(* Non-destructive checkpoint using DMTCP.                                   *)
-(* ------------------------------------------------------------------------- *)
-
-let checkpoint 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();
-   loadt "Examples/update_database.ml";
-   print_newline ();
-   Unix.sleep 1;
-   try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
-   Format.print_string complete_banner;
-   Format.print_newline(); Format.print_newline());;
-
-dmtcp_checkpoint "";;

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

@@ -1,29 +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 "make.ml";;
-
-(* ------------------------------------------------------------------------- *)
-(* Non-destructive checkpoint using DMTCP.                                   *)
-(* ------------------------------------------------------------------------- *)
-
-let checkpoint 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();
-   loadt "Examples/update_database.ml";
-   print_newline ();
-   Unix.sleep 1;
-   try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
-   Format.print_string complete_banner;
-   Format.print_newline(); Format.print_newline());;
-
-loadt "Multivariate/make.ml";;
-dmtcp_checkpoint "Preloaded with multivariate analysis";;

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

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

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

pkgs/top-level/all-packages.nix

@@ -6783,11 +6783,6 @@ let
 
   hol_light_binaries = callPackage ../applications/science/logic/hol_light/binaries.nix { };
 
-  # This is a special version of OCaml handcrafted especially for
-  # hol_light it should be merged with the current expresion for ocaml
-  # one day.
-  ocaml_with_sources = callPackage ../applications/science/logic/hol_light/ocaml-with-sources.nix { };
-
   isabelle = import ../applications/science/logic/isabelle {
     inherit (pkgs) stdenv fetchurl nettools perl polyml;
     inherit (pkgs.emacs23Packages) proofgeneral;