Add HOL Light and its dependencies.

Add pkgs/applications/science/logic/hol_light
and pkgs/applications/science/emacs-modes/hol_light

Some functionalities of HOL Light requires the compiled sources of
OCaml.  For now we provide a new package ocaml_with_sources.  After
this shuold be merged with the current version of OCaml already
present in nixpkgs.


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

pkgs/applications/editors/emacs-modes/hol_light/default.nix

@@ -0,0 +1,25 @@
+{stdenv, fetchsvn}:
+
+let
+  revision = "73";
+in
+
+stdenv.mkDerivation {
+  name = "hol_light_mode-${revision}";
+
+  src = fetchsvn {
+    url = http://seanmcl-ocaml-lib.googlecode.com/svn/trunk/workshop/software/emacs;
+    rev = revision;
+    sha256 = "3ca83098960439da149a47e1caff32536601559a77f04822be742a390c67feb7";
+  };
+
+  installPhase = ''
+    DEST=$out/share/emacs/site-lisp
+    ensureDir $DEST
+    cp -a * $DEST
+  '';
+
+  meta = {
+    description = "A HOL Light mode for emacs";
+  };
+}

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

@@ -0,0 +1,55 @@
+{stdenv, ocaml_with_sources, hol_light, dmtcp, nettools, openssh}:
+# nettools and openssh needed for dmtcp restarting script.
+
+let
+  selfcheckpoint_core_ml = ./selfcheckpoint_core.ml;
+  selfcheckpoint_multivariate_ml = ./selfcheckpoint_multivariate.ml;
+  selfcheckpoint_complex_ml = ./selfcheckpoint_complex.ml;
+in
+
+stdenv.mkDerivation {
+  name = "hol_light_binaries-${hol_light.version}";
+
+  buildInputs = [ dmtcp ocaml_with_sources nettools openssh];
+
+  buildCommand = ''
+    HOL_DIR=${hol_light}/src/hol_light
+    BIN_DIR=$out/bin
+    ensureDir $BIN_DIR
+
+    # HOL Light Core
+    dmtcp_coordinator --background
+    echo 'Unix.system "dmtcp_command -k";;\n' |
+      dmtcp_checkpoint -q -c "$BIN_DIR" \
+        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_core_ml}
+    substituteInPlace dmtcp_restart_script.sh \
+      --replace dmtcp_restart "dmtcp_restart --quiet"
+    mv dmtcp_restart_script.sh $BIN_DIR/hol_light
+    dmtcp_command -q
+
+    # HOL Light Multivariate
+    dmtcp_coordinator --background
+    echo 'Unix.system "dmtcp_command -k";;\n' |
+      dmtcp_checkpoint -q -c "$BIN_DIR" \
+        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_multivariate_ml}
+    substituteInPlace dmtcp_restart_script.sh \
+      --replace dmtcp_restart "dmtcp_restart --quiet"
+    mv dmtcp_restart_script.sh $BIN_DIR/hol_light_multivariate
+    dmtcp_command -q
+
+    # HOL Light Complex
+    dmtcp_coordinator --background
+    echo 'Unix.system "dmtcp_command -k";;\n' |
+      dmtcp_checkpoint -q -c "$BIN_DIR" \
+        ocaml -I "$HOL_DIR" -init ${selfcheckpoint_complex_ml}
+    substituteInPlace dmtcp_restart_script.sh \
+      --replace dmtcp_restart "dmtcp_restart --quiet"
+    mv dmtcp_restart_script.sh $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

@@ -0,0 +1,72 @@
+{stdenv, fetchurl, ocaml_with_sources}:
+
+let
+  pname = "hol_light";
+  version = "100110";
+  webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+
+  dmtcp_checkpoint = ''
+
+(* ------------------------------------------------------------------------- *)
+(* Non-destructive checkpoint using DMTCP.                                   *)
+(* ------------------------------------------------------------------------- *)
+
+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 ];
+
+  buildCommand = ''
+    ensureDir "$out/src"
+    cd "$out/src"
+
+    tar -xzf "$src"
+    cd hol_light
+
+    substituteInPlace hol.ml --replace \
+      "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
+      "\"$out/src/hol_light\""
+
+    substituteInPlace Examples/update_database.ml --replace \
+      "Filename.concat ocaml_source_dir" \
+      "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
+
+    echo '${dmtcp_checkpoint}' >> make.ml
+
+    make
+  '';
+
+  meta = {
+    description = "An 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 = webpage;
+    license = "BSD";
+  };
+}

pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix

@@ -0,0 +1,33 @@
+{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/selfcheckpoint_complex.ml

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

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

@@ -0,0 +1,29 @@
+(* ========================================================================= *)
+(* 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/top-level/all-packages.nix

@@ -7083,6 +7083,10 @@ let
       inherit fetchurl stdenv emacs;
     };
 
+    hol_light_mode = import ../applications/editors/emacs-modes/hol_light {
+      inherit fetchsvn stdenv;
+    };
+
     magit = import ../applications/editors/emacs-modes/magit {
       inherit fetchurl stdenv emacs texinfo;
     };
@@ -8744,6 +8748,24 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  hol_light = import ../applications/science/logic/hol_light {
+    inherit stdenv fetchurl ocaml_with_sources;
+  };
+
+  hol_light_binaries =
+  import ../applications/science/logic/hol_light/binaries.nix {
+    inherit stdenv ocaml_with_sources hol_light nettools openssh;
+    dmtcp = dmtcp_devel;
+  };
+
+  # 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 =
+  import ../applications/science/logic/hol_light/ocaml-with-sources.nix {
+    inherit stdenv fetchurl;
+  };
+
   isabelle = import ../applications/science/logic/isabelle {
     inherit (pkgs) stdenv fetchurl nettools perl polyml emacs emacsPackages;
   };