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

10 files changed, 113 insertions, 1643 deletions

diff --git a/pkgs/applications/science/logic/hol_light/binaries.nix b/pkgs/applications/science/logic/hol_light/binaries.nix
index 41d2f8237bec..de89a7a5d4e8 100644
--- a/pkgs/applications/science/logic/hol_light/binaries.nix
+++ b/pkgs/applications/science/logic/hol_light/binaries.nix
@@ -1,55 +1,60 @@
-{stdenv, ocaml_with_sources, hol_light, dmtcp, nettools, openssh}:
-# nettools and openssh needed for dmtcp restarting script.
+{stdenv, hol_light, dmtcp}:
 
 let
-  selfcheckpoint_core_ml = ./selfcheckpoint_core.ml;
-  selfcheckpoint_multivariate_ml = ./selfcheckpoint_multivariate.ml;
-  selfcheckpoint_complex_ml = ./selfcheckpoint_complex.ml;
+  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 ocaml_with_sources nettools openssh];
+  buildInputs = [ dmtcp hol_light hol_light.ocaml ];
 
   buildCommand = ''
-    HOL_DIR=${hol_light}/src/hol_light
-    BIN_DIR=$out/bin
-    ensureDir $BIN_DIR
+    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
+    (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
-    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
+    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
-    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
+    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"
   '';
-
-  meta = {
-    description = "Preload binaries for HOL Light.";
-    license = "BSD";
-  };
 }
diff --git a/pkgs/applications/science/logic/hol_light/configure-3.09.3 b/pkgs/applications/science/logic/hol_light/configure-3.09.3
deleted file mode 100755
index c52776894598..000000000000
--- a/pkgs/applications/science/logic/hol_light/configure-3.09.3
+++ /dev/null
@@ -1,1444 +0,0 @@
-#! /bin/sh
-
-#########################################################################
-#                                                                       #
-#                            Objective Caml                             #
-#                                                                       #
-#            Xavier Leroy, projet Cristal, INRIA Rocquencourt           #
-#                                                                       #
-#   Copyright 1999 Institut National de Recherche en Informatique et    #
-#   en Automatique.  All rights reserved.  This file is distributed     #
-#   under the terms of the GNU Library General Public License, with     #
-#   the special exception on linking described in file LICENSE.         #
-#                                                                       #
-#########################################################################
-
-# $Id: configure,v 1.228.2.5 2006/03/30 10:00:19 doligez Exp $
-
-configure_options="$*"
-prefix=/usr/local
-bindir=''
-libdir=''
-mandir=''
-manext=1
-host_type=unknown
-ccoption=''
-cclibs=''
-curseslibs=''
-mathlib='-lm'
-dllib=''
-x11_include_dir=''
-x11_lib_dir=''
-tk_wanted=yes
-pthread_wanted=yes
-tk_defs=''
-tk_libs=''
-tk_x11=yes
-dl_defs=''
-verbose=no
-withcurses=yes
-withsharedlibs=yes
-gcc_warnings="-Wall"
-
-# Try to turn internationalization off, can cause config.guess to malfunction!
-unset LANG
-unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
-
-# Turn off some MacOS X debugging stuff, same reason
-unset RC_TRACE_ARCHIVES RC_TRACE_DYLIBS RC_TRACE_PREBINDING_DISABLED
-
-# Parse command-line arguments
-
-while : ; do
-  case "$1" in
-    "") break;;
-    -prefix|--prefix)
-        prefix=$2; shift;;
-    -bindir|--bindir)
-        bindir=$2; shift;;
-    -libdir|--libdir)
-        libdir=$2; shift;;
-    -mandir|--mandir)
-        case "$2" in
-          */man[1-9ln])
-            mandir=`echo $2 | sed -e 's|^\(.*\)/man.$|\1|'`
-            manext=`echo $2 | sed -e 's/^.*\(.\)$/\1/'`;;
-          *)
-            mandir=$2
-            manext=1;;
-        esac
-        shift;;
-    -host*|--host*)
-        host_type=$2; shift;;
-    -cc*)
-        ccoption="$2"; shift;;
-    -lib*)
-        cclibs="$2 $cclibs"; shift;;
-    -no-curses)
-        withcurses=no;;
-    -no-shared-libs)
-        withsharedlibs=no;;
-    -x11include*|--x11include*)
-        x11_include_dir=$2; shift;;
-    -x11lib*|--x11lib*)
-        x11_lib_dir=$2; shift;;
-    -with-pthread*|--with-pthread*)
-        ;; # Ignored for backward compatibility
-    -no-pthread*|--no-pthread*)
-        pthread_wanted=no;;
-    -no-tk|--no-tk)
-        tk_wanted=no;;
-    -tkdefs*|--tkdefs*)
-        tk_defs=$2; shift;;
-    -tklibs*|--tklibs*)
-        tk_libs=$2; shift;;
-    -tk-no-x11|--tk-no-x11)
-        tk_x11=no;;
-    -dldefs*|--dldefs*)
-        dl_defs="$2"; shift;;
-    -dllibs*|--dllibs*)
-        dllib="$2"; shift;;
-    -verbose|--verbose)
-        verbose=yes;;
-    *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
-  esac
-  shift
-done
-
-# Sanity checks
-
-case "$prefix" in
-  /*) ;;
-   *) echo "The -prefix directory must be absolute." 1>&2; exit 2;;
-esac
-case "$bindir" in
-  /*) ;;
-  "") ;;
-   *) echo "The -bindir directory must be absolute." 1>&2; exit 2;;
-esac
-case "$libdir" in
-  /*) ;;
-  "") ;;
-   *) echo "The -libdir directory must be absolute." 1>&2; exit 2;;
-esac
-case "$mandir" in
-  /*) ;;
-  "") ;;
-   *) echo "The -mandir directory must be absolute." 1>&2; exit 2;;
-esac
-
-# Generate the files
-
-cd config/auto-aux
-rm -f s.h m.h Makefile
-touch s.h m.h Makefile
-
-# Write options to Makefile
-
-echo "# generated by ./configure $configure_options" >> Makefile
-
-# Where to install
-
-echo "PREFIX=$prefix" >> Makefile
-case "$bindir" in
-  "") echo 'BINDIR=$(PREFIX)/bin' >> Makefile
-      bindir="$prefix/bin";;
-   *) echo "BINDIR=$bindir" >> Makefile;;
-esac
-case "$libdir" in
-  "") echo 'LIBDIR=$(PREFIX)/lib/ocaml' >> Makefile
-      libdir="$prefix/lib/ocaml";;
-   *) echo "LIBDIR=$libdir" >> Makefile;;
-esac
-echo 'STUBLIBDIR=$(LIBDIR)/stublibs' >> Makefile
-case "$mandir" in
-  "") echo 'MANDIR=$(PREFIX)/man' >> Makefile
-      mandir="$prefix/man";;
-   *) echo "MANDIR=$mandir" >> Makefile;;
-esac
-echo "MANEXT=$manext" >> Makefile
-
-# Determine the system type
-
-if test "$host_type" = "unknown"; then
-  if host_type=`../gnu/config.guess`; then :; else
-    echo "Cannot guess host type"
-    echo "You must specify one with the -host option"
-    exit 2
-  fi
-fi
-if host=`../gnu/config.sub $host_type`; then :; else
-  echo "Please specify the correct host type with the -host option"
-  exit 2
-fi
-echo "Configuring for a $host ..."
-
-# Do we have gcc?
-
-if test -z "$ccoption"; then
-  if sh ./searchpath gcc; then
-    echo "gcc found"
-    cc=gcc
-  else
-    cc=cc
-  fi
-else
-  cc="$ccoption"
-fi
-
-# Check for buggy versions of GCC
-
-buggycc="no"
-
-case "$host,$cc" in
-  i[3456]86-*-*,gcc*)
-    case `$cc --version` in
-      2.7.2.1) cat <<'EOF'
-
-WARNING: you are using gcc version 2.7.2.1 on an Intel x86 processor.
-This version of gcc is known to generate incorrect code for the
-Objective Caml runtime system on some Intel x86 machines. (The symptom
-is a crash of boot/ocamlc when compiling stdlib/pervasives.mli.)
-In particular, the version of gcc 2.7.2.1 that comes with
-Linux RedHat 4.x / Intel is affected by this problem.
-Other Linux distributions might also be affected.
-If you are using one of these configurations, you are strongly advised
-to use another version of gcc, such as 2.95, which are
-known to work well with Objective Caml.
-
-Press <enter> to proceed or <interrupt> to stop.
-EOF
-        read reply;;
-      2.96*) cat <<'EOF'
-
-WARNING: you are using gcc version 2.96 on an Intel x86 processor.
-Certain patched versions of gcc 2.96 are known to generate incorrect
-code for the Objective Caml runtime system.  (The symptom is a segmentation
-violation on boot/ocamlc.)  Those incorrectly patched versions can be found
-in RedHat 7.2 and Mandrake 8.0 and 8.1; other Linux distributions
-might also be affected.  (See bug #57760 on bugzilla.redhat.com)
-
-Auto-configuration will now select gcc compiler flags that work around
-the problem.  Still, if you observe segmentation faults while running
-ocamlc or ocamlopt, you are advised to try another version of gcc,
-such as 2.95.3 or 3.2.
-
-EOF
-        buggycc="gcc.2.96";;
-
-            esac;;
-esac
-
-# Configure the bytecode compiler
-
-bytecc="$cc"
-bytecccompopts=""
-bytecclinkopts=""
-ostype="Unix"
-exe=""
-
-case "$bytecc,$host" in
-  cc,*-*-nextstep*)
-    # GNU C extensions disabled, but __GNUC__ still defined!
-    bytecccompopts="-fno-defer-pop $gcc_warnings -U__GNUC__ -posix"
-    bytecclinkopts="-posix";;
-  *,*-*-rhapsody*)
-    # Almost the same as NeXTStep
-    bytecccompopts="-fno-defer-pop $gcc_warnings -DSHRINKED_GNUC"
-    mathlib="";;
-  *,*-*-darwin*)
-    # Almost the same as rhapsody
-    bytecccompopts="-fno-defer-pop -no-cpp-precomp $gcc_warnings"
-    mathlib="";;
-  *,*-*-beos*)
-    bytecccompopts="-fno-defer-pop $gcc_warnings"
-    # No -lm library
-    mathlib="";;
-  gcc,alpha*-*-osf*)
-    bytecccompopts="-fno-defer-pop $gcc_warnings"
-    if cc="$bytecc" sh ./hasgot -mieee; then
-      bytecccompopts="-mieee $bytecccompopts";
-    fi
-    # Put code and static data in lower 4GB
-    bytecclinkopts="-Wl,-T,12000000 -Wl,-D,14000000"
-    # Tell gcc that we can use 32-bit code addresses for threaded code
-    echo "#define ARCH_CODE32" >> m.h;;
-  cc,alpha*-*-osf*)
-    bytecccompopts="-std1 -ieee";;
-  gcc,alpha*-*-linux*)
-    if cc="$bytecc" sh ./hasgot -mieee; then
-      bytecccompopts="-mieee $bytecccompopts";
-    fi;;
-  cc,mips-*-irix6*)
-    # Add -n32 flag to ensure compatibility with native-code compiler
-    bytecccompopts="-n32"
-    # Turn off warning "unused library"
-    bytecclinkopts="-n32 -Wl,-woff,84";;
-  cc*,mips-*-irix6*)
-    # (For those who want to force "cc -64")
-    # Turn off warning "unused library"
-    bytecclinkopts="-Wl,-woff,84";;
-  *,alpha*-*-unicos*)
-    # For the Cray T3E
-    bytecccompopts="-DUMK";;
-  gcc*,powerpc-*-aix*)
-    # Avoid name-space pollution by requiring Unix98-conformant includes
-    bytecccompopts="-fno-defer-pop $gcc_warnings -D_XOPEN_SOURCE=500";;
-  *,powerpc-*-aix*)
-    bytecccompopts="-D_XOPEN_SOURCE=500";;
-  gcc*,*-*-cygwin*)
-    bytecccompopts="-fno-defer-pop $gcc_warnings -U_WIN32"
-    exe=".exe"
-    ostype="Cygwin";;
-  gcc*,x86_64-*-linux*)
-    bytecccompopts="-fno-defer-pop $gcc_warnings"
-    # Tell gcc that we can use 32-bit code addresses for threaded code
-    # unless we are compiled for a shared library (-fPIC option)
-    echo "#ifndef __PIC__" >> m.h
-    echo "#  define ARCH_CODE32" >> m.h
-    echo "#endif" >> m.h;;
-  gcc*)
-    bytecccompopts="-fno-defer-pop $gcc_warnings";;
-esac
-
-# Configure compiler to use in further tests
-
-cc="$bytecc -O $bytecclinkopts"
-export cc cclibs verbose
-
-# Check C compiler
-
-sh ./runtest ansi.c
-case $? in
-  0) echo "The C compiler is ANSI-compliant.";;
-  1) echo "The C compiler $cc is not ANSI-compliant."
-     echo "You need an ANSI C compiler to build Objective Caml."
-     exit 2;;
-  *) echo "Unable to compile the test program."
-     echo "Make sure the C compiler $cc is properly installed."
-     exit 2;;
-esac
-
-# Check the sizes of data types
-
-echo "Checking the sizes of integers and pointers..."
-set `sh ./runtest sizes.c`
-case "$2,$3" in
-  4,4) echo "OK, this is a regular 32 bit architecture."
-       echo "#undef ARCH_SIXTYFOUR" >> m.h;;
-  *,8) echo "Wow! A 64 bit architecture!"
-       echo "#define ARCH_SIXTYFOUR" >> m.h;;
-  *,*) echo "This architecture seems to be neither 32 bits nor 64 bits."
-       echo "Objective Caml won't run on this architecture."
-       exit 2;;
-    *) echo "Unable to compile the test program."
-       echo "Make sure the C compiler $cc is properly installed."
-       exit 2;;
-esac
-if test $1 != 4 && test $2 != 4 && test $4 != 4; then
-  echo "Sorry, we can't find a 32-bit integer type"
-  echo "(sizeof(short) = $4, sizeof(int) = $1, sizeof(long) = $2)"
-  echo "Objective Caml won't run on this architecture."
-  exit 2
-fi
-
-echo "#define SIZEOF_INT $1" >> m.h
-echo "#define SIZEOF_LONG $2" >> m.h
-echo "#define SIZEOF_PTR $3" >> m.h
-echo "#define SIZEOF_SHORT $4" >> m.h
-
-if test $2 = 8; then
-     echo "#define ARCH_INT64_TYPE long" >> m.h
-     echo "#define ARCH_UINT64_TYPE unsigned long" >> m.h
-     echo '#define ARCH_INT64_PRINTF_FORMAT "l"' >> m.h
-     int64_native=true
-else
-  sh ./runtest longlong.c
-  case $? in
-  0) echo "64-bit \"long long\" integer type found (printf with \"%ll\")."
-     echo "#define ARCH_INT64_TYPE long long" >> m.h
-     echo "#define ARCH_UINT64_TYPE unsigned long long" >> m.h
-     echo '#define ARCH_INT64_PRINTF_FORMAT "ll"' >> m.h
-     int64_native=true;;
-  1) echo "64-bit \"long long\" integer type found (printf with \"%q\")."
-     echo "#define ARCH_INT64_TYPE long long" >> m.h
-     echo "#define ARCH_UINT64_TYPE unsigned long long" >> m.h
-     echo '#define ARCH_INT64_PRINTF_FORMAT "q"' >> m.h
-     int64_native=true;;
-  2) echo "64-bit \"long long\" integer type found (but no printf)."
-     echo "#define ARCH_INT64_TYPE long long" >> m.h
-     echo "#define ARCH_UINT64_TYPE unsigned long long" >> m.h
-     echo '#undef ARCH_INT64_PRINTF_FORMAT' >> m.h
-     int64_native=true;;
-  *) echo "No suitable 64-bit integer type found, will use software emulation."
-     echo "#undef ARCH_INT64_TYPE" >> m.h
-     echo "#undef ARCH_UINT64_TYPE" >> m.h
-     echo '#undef ARCH_INT64_PRINTF_FORMAT' >> m.h
-     int64_native=false;;
-  esac
-fi
-
-if test $3 = 8 && test $int64_native = false; then
-  echo "This architecture has 64-bit pointers but no 64-bit integer type."
-  echo "Objective Caml won't run on this architecture."
-  exit 2
-fi
-
-# Determine endianness
-
-sh ./runtest endian.c
-case $? in
-  0) echo "This is a big-endian architecture."
-     echo "#define ARCH_BIG_ENDIAN" >> m.h;;
-  1) echo "This is a little-endian architecture."
-     echo "#undef ARCH_BIG_ENDIAN" >> m.h;;
-  2) echo "This architecture seems to be neither big endian nor little endian."
-     echo "Objective Caml won't run on this architecture."
-     exit 2;;
-  *) echo "Something went wrong during endianness determination."
-     echo "You'll have to figure out endianness yourself"
-     echo "(option ARCH_BIG_ENDIAN in m.h).";;
-esac
-
-# Determine alignment constraints
-
-case "$host" in
-  sparc*-*-*|hppa*-*-*)
-    # On Sparc V9 with certain versions of gcc, determination of double
-    # alignment is not reliable (PR#1521), hence force it.
-    # Same goes for hppa.
-    # But there's a knack (PR#2572):
-    # if we're in 64-bit mode (sizeof(long) == 8),
-    # we must not doubleword-align floats...
-    if test $2 = 8; then
-      echo "Doubles can be word-aligned."
-      echo "#undef ARCH_ALIGN_DOUBLE" >> m.h
-    else
-      echo "Doubles must be doubleword-aligned."
-      echo "#define ARCH_ALIGN_DOUBLE" >> m.h
-    fi;;
-  *)
-    sh ./runtest dblalign.c
-    case $? in
-      0) echo "Doubles can be word-aligned."
-         echo "#undef ARCH_ALIGN_DOUBLE" >> m.h;;
-      1) echo "Doubles must be doubleword-aligned."
-         echo "#define ARCH_ALIGN_DOUBLE" >> m.h;;
-      *) echo "Something went wrong during alignment determination for doubles."
-         echo "I'm going to assume this architecture has alignment constraints over doubles."
-         echo "That's a safe bet: Objective Caml will work even if"
-         echo "this architecture has actually no alignment constraints."
-         echo "#define ARCH_ALIGN_DOUBLE" >> m.h;;
-    esac;;
-esac
-
-if $int64_native; then
-  case "$host" in
-    sparc*-*-*|hppa*-*-*)
-      if test $2 = 8; then
-        echo "64-bit integers can be word-aligned."
-        echo "#undef ARCH_ALIGN_INT64" >> m.h
-      else
-        echo "64-bit integers must be doubleword-aligned."
-        echo "#define ARCH_ALIGN_INT64" >> m.h
-      fi;;
-    *)
-      sh ./runtest int64align.c
-      case $? in
-        0) echo "64-bit integers can be word-aligned."
-           echo "#undef ARCH_ALIGN_INT64" >> m.h;;
-        1) echo "64-bit integers must be doubleword-aligned."
-           echo "#define ARCH_ALIGN_INT64" >> m.h;;
-        *) echo "Something went wrong during alignment determination for 64-bit integers."
-           echo "I'm going to assume this architecture has alignment constraints."
-           echo "That's a safe bet: Objective Caml will work even if"
-           echo "this architecture has actually no alignment constraints."
-           echo "#define ARCH_ALIGN_INT64" >> m.h;;
-      esac
-  esac
-else
-  echo "#undef ARCH_ALIGN_INT64" >> m.h
-fi
-
-# Check semantics of division and modulus
-
-sh ./runtest divmod.c
-case $? in
-  0) echo "Native division and modulus have round-towards-zero semantics, will use them."
-     echo "#undef NONSTANDARD_DIV_MOD" >> m.h;;
-  1) echo "Native division and modulus do not have round-towards-zero semantics, will use software emulation."
-     echo "#define NONSTANDARD_DIV_MOD" >> m.h;;
-  *) echo "Something went wrong while checking native division and modulus, please report it."
-     echo "#define NONSTANDARD_DIV_MOD" >> m.h;;
-esac
-
-# Shared library support
-
-shared_libraries_supported=false
-dl_needs_underscore=false
-sharedcccompopts=''
-mksharedlib=''
-byteccrpath=''
-mksharedlibrpath=''
-
-if test $withsharedlibs = "yes"; then
-  case "$host" in
-    *-*-linux-gnu|*-*-linux|*-*-freebsd[3-9]*|*-*-gnu*)
-      sharedcccompopts="-fPIC"
-      mksharedlib="$bytecc -shared -o"
-      bytecclinkopts="$bytecclinkopts -Wl,-E"
-      byteccrpath="-Wl,-rpath,"
-      mksharedlibrpath="-Wl,-rpath,"
-      shared_libraries_supported=true;;
-    alpha*-*-osf*)
-      case "$bytecc" in
-        gcc*)
-          sharedcccompopts="-fPIC"
-          mksharedlib="$bytecc -shared -o"
-          byteccrpath="-Wl,-rpath,"
-          mksharedlibrpath="-Wl,-rpath,"
-          shared_libraries_supported=true;;
-        cc*)
-          sharedcccompopts=""
-          mksharedlib="ld -shared -expect_unresolved '*' -o"
-          byteccrpath="-Wl,-rpath,"
-          mksharedlibrpath="-rpath "
-          shared_libraries_supported=true;;
-      esac;;
-    *-*-solaris2*)
-      case "$bytecc" in
-        gcc*)
-          sharedcccompopts="-fPIC"
-          if sh ./solaris-ld; then
-            mksharedlib="$bytecc -shared -o"
-            byteccrpath="-R"
-            mksharedlibrpath="-R"
-          else
-            mksharedlib="$bytecc -shared -o"
-            bytecclinkopts="$bytecclinkopts -Wl,-E"
-            byteccrpath="-Wl,-rpath,"
-            mksharedlibrpath="-Wl,-rpath,"
-          fi
-          shared_libraries_supported=true;;
-        *)
-          sharedcccompopts="-KPIC"
-          byteccrpath="-R"
-          mksharedlibrpath="-R"
-          mksharedlib="/usr/ccs/bin/ld -G -o"
-          shared_libraries_supported=true;;
-      esac;;
-    mips*-*-irix[56]*)
-      case "$bytecc" in
-        cc*) sharedcccompopts="";;
-        gcc*) sharedcccompopts="-fPIC";;
-      esac
-      mksharedlib="ld -shared -rdata_shared -o"
-      byteccrpath="-Wl,-rpath,"
-      mksharedlibrpath="-rpath "
-      shared_libraries_supported=true;;
-    powerpc-apple-darwin*)
-      mksharedlib="cc -bundle -flat_namespace -undefined suppress -o"
-      bytecccompopts="$dl_defs $bytecccompopts"
-      #sharedcccompopts="-fnocommon"
-      dl_needs_underscore=true
-      shared_libraries_supported=true;;
-  esac
-fi
-
-# Further machine-specific hacks
-
-case "$host" in
-  ia64-*-linux*|alpha*-*-linux*|x86_64-*-linux*)
-    echo "Will use mmap() instead of malloc() for allocation of major heap chunks."
-    echo "#define USE_MMAP_INSTEAD_OF_MALLOC" >> s.h;;
-esac
-
-# Configure the native-code compiler
-
-arch=none
-model=default
-system=unknown
-
-case "$host" in
-  alpha*-*-osf*)                arch=alpha; system=digital;;
-  alpha*-*-linux*)              arch=alpha; system=linux;;
-  alpha*-*-gnu*)                arch=alpha; system=gnu;;
-  alpha*-*-freebsd*)            arch=alpha; system=freebsd;;
-  alpha*-*-netbsd*)             arch=alpha; system=netbsd;;
-  alpha*-*-openbsd*)            arch=alpha; system=openbsd;;
-  sparc*-*-sunos4.*)            arch=sparc; system=sunos;;
-  sparc*-*-solaris2.*)          arch=sparc; system=solaris;;
-  sparc*-*-*bsd*)               arch=sparc; system=bsd;;
-  sparc*-*-linux*)              arch=sparc; system=linux;;
-  sparc*-*-gnu*)                arch=sparc; system=gnu;;
-  i[3456]86-*-linux*)           arch=i386; system=linux_`sh ./runtest elf.c`;;
-  i[3456]86-*-*bsd*)            arch=i386; system=bsd_`sh ./runtest elf.c`;;
-  i[3456]86-*-nextstep*)        arch=i386; system=nextstep;;
-  i[3456]86-*-solaris*)         arch=i386; system=solaris;;
-  i[3456]86-*-beos*)            arch=i386; system=beos;;
-  i[3456]86-*-cygwin*)          arch=i386; system=cygwin;;
-  i[3456]86-*-darwin*)          arch=i386; system=macosx;;
-  i[3456]86-*-gnu*)             arch=i386; system=gnu;;
-  mips-*-irix6*)                arch=mips; system=irix;;
-  hppa1.1-*-hpux*)              arch=hppa; system=hpux;;
-  hppa2.0*-*-hpux*)             arch=hppa; system=hpux;;
-  hppa*-*-linux*)               arch=hppa; system=linux;;
-  hppa*-*-gnu*)                 arch=hppa; system=gnu;;
-  powerpc-*-linux*)             arch=power; model=ppc; system=elf;;
-  powerpc-*-netbsd*)            arch=power; model=ppc; system=bsd;;
-  powerpc-*-rhapsody*)          arch=power; model=ppc; system=rhapsody;;
-  powerpc-*-darwin*)            arch=power; model=ppc; system=rhapsody;;
-  arm*-*-linux*)                arch=arm; system=linux;;
-  arm*-*-gnu*)                  arch=arm; system=gnu;;
-  ia64-*-linux*)                arch=ia64; system=linux;;
-  ia64-*-gnu*)                  arch=ia64; system=gnu;;
-  ia64-*-freebsd*)              arch=ia64; system=freebsd;;
-  x86_64-*-linux*)              arch=amd64; system=linux;;
-  x86_64-*-gnu*)                arch=amd64; system=gnu;;
-  x86_64-*-freebsd*)            arch=amd64; system=freebsd;;
-  x86_64-*-openbsd*)            arch=amd64; system=openbsd;;
-esac
-
-if test -z "$ccoption"; then
-  case "$arch,$system,$cc" in
-    alpha,digital,gcc*) nativecc=cc;;
-    mips,*,gcc*) nativecc=cc;;
-    *) nativecc="$bytecc";;
-  esac
-else
-  nativecc="$ccoption"
-fi
-
-nativecccompopts=''
-nativecclinkopts=''
-nativeccrpath="$byteccrpath"
-
-case "$arch,$nativecc,$system,$host_type" in
-  alpha,cc*,digital,*) nativecccompopts=-std1;;
-  mips,cc*,irix,*)     nativecccompopts=-n32
-                       nativecclinkopts="-n32 -Wl,-woff,84";;
-  *,*,nextstep,*)      nativecccompopts="$gcc_warnings -U__GNUC__ -posix"
-                       nativecclinkopts="-posix";;
-  *,*,rhapsody,*darwin[1-5].*)
-                       nativecccompopts="$gcc_warnings -DSHRINKED_GNUC";;
-  *,*,rhapsody,*)
-                 nativecccompopts="$gcc_warnings -DDARWIN_VERSION_6 $dl_defs";;
-  *,gcc*,cygwin,*)     nativecccompopts="$gcc_warnings -U_WIN32";;
-  *,gcc*,*,*)          nativecccompopts="$gcc_warnings";;
-esac
-
-asflags=''
-aspp='$(AS)'
-asppflags=''
-asppprofflags='-DPROFILING'
-
-case "$arch,$model,$system" in
-  alpha,*,digital)  asflags='-O2'; asppflags='-O2 -DSYS_$(SYSTEM)';
-                    asppprofflags='-pg -DPROFILING';;
-  alpha,*,linux)    aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  alpha,*,gnu)      aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  alpha,*,freebsd)  aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  alpha,*,netbsd)   aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  alpha,*,openbsd)  aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  mips,*,irix)      asflags='-n32 -O2'; asppflags="$asflags";;
-  sparc,*,bsd)      aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  sparc,*,linux)    aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  sparc,*,gnu)      aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  sparc,*,*)        case "$cc" in
-                      gcc*) aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-                         *) asppflags='-P -DSYS_$(SYSTEM)';;
-                    esac;;
-  i386,*,solaris)   aspp='/usr/ccs/bin/as'; asppflags='-P -DSYS_$(SYSTEM)';;
-  i386,*,*)         aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  hppa,*,*)         aspp="$cc"; asppflags='-traditional -c -DSYS_$(SYSTEM)';;
-  power,*,elf)      aspp='gcc'; asppflags='-c';;
-  power,*,bsd)      aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  power,*,rhapsody) ;;
-  arm,*,linux)      aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  arm,*,gnu)        aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-  ia64,*,*)         asflags=-xexplicit
-                    aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM) -Wa,-xexplicit';;
-  amd64,*,*)        aspp='gcc'; asppflags='-c -DSYS_$(SYSTEM)';;
-esac
-
-cc_profile='-pg'
-case "$arch,$model,$system" in
-  alpha,*,digital) profiling='prof';;
-  i386,*,linux_elf) profiling='prof';;
-  i386,*,gnu) profiling='prof';;
-  i386,*,bsd_elf) profiling='prof';;
-  sparc,*,solaris)
-    profiling='prof'
-    case "$nativecc" in gcc*) ;; *) cc_profile='-xpg';; esac;;
-  amd64,*,linux) profiling='prof';;
-  amd64,*,gnu) profiling='prof';;
-  *) profiling='noprof';;
-esac
-
-# Where is ranlib?
-
-if sh ./searchpath ranlib; then
-  echo "ranlib found"
-  echo "RANLIB=ranlib" >> Makefile
-  echo "RANLIBCMD=ranlib" >> Makefile
-else
-  echo "ranlib not used"
-  echo "RANLIB=ar rs" >> Makefile
-  echo "RANLIBCMD=" >> Makefile
-fi
-
-# Do #! scripts work?
-
-# BRAVO: check disabled for NixOS
-# if (SHELL=/bin/sh; export SHELL; (./sharpbang || ./sharpbang2) >/dev/null); then
-#   echo "#! appears to work in shell scripts"
-  case "$host" in
-    *-*-sunos*|*-*-unicos*)
-      echo "We won't use it, though, because under SunOS and Unicos it breaks"
-      echo "on pathnames longer than 30 characters"
-      echo "SHARPBANGSCRIPTS=false" >> Makefile;;
-    *-*-cygwin*)
-      echo "We won't use it, though, because of conflicts with .exe extension"
-      echo "under Cygwin"
-      echo "SHARPBANGSCRIPTS=false" >> Makefile;;
-    *)
-      echo "SHARPBANGSCRIPTS=true" >> Makefile;;
-  esac
-# else
-#   echo "No support for #! in shell scripts"
-#   echo "SHARPBANGSCRIPTS=false" >> Makefile
-# fi
-
-# Write the OS type (Unix or Cygwin)
-
-echo "#define OCAML_OS_TYPE \"$ostype\"" >> s.h
-echo "#define OCAML_STDLIB_DIR \"$libdir\"" >> s.h
-
-# Use 64-bit file offset if possible
-
-bytecccompopts="$bytecccompopts -D_FILE_OFFSET_BITS=64"
-nativecccompopts="$nativecccompopts -D_FILE_OFFSET_BITS=64"
-
-# Check the semantics of signal handlers
-
-if sh ./hasgot sigaction sigprocmask; then
-  echo "POSIX signal handling found."
-  echo "#define POSIX_SIGNALS" >> s.h
-else
-  if sh ./runtest signals.c; then
-    echo "Signals have the BSD semantics."
-    echo "#define BSD_SIGNALS" >> s.h
-  else
-    echo "Signals have the System V semantics."
-  fi
-  if sh ./hasgot sigsetmask; then
-    echo "sigsetmask() found"
-    echo "#define HAS_SIGSETMASK" >> s.h
-  fi
-fi
-
-# For the sys module
-
-if sh ./hasgot getrusage; then
-  echo "getrusage() found."
-  echo "#define HAS_GETRUSAGE" >> s.h
-fi
-
-if sh ./hasgot times; then
-  echo "times() found."
-  echo "#define HAS_TIMES" >> s.h
-fi
-
-# For the terminfo module
-
-if test "$withcurses" = "yes"; then
-  for libs in "" "-lcurses" "-ltermcap" "-lcurses -ltermcap" "-lncurses"; do
-    if sh ./hasgot $libs tgetent tgetstr tgetnum tputs; then
-      echo "termcap functions found (with libraries '$libs')"
-      echo "#define HAS_TERMCAP" >> s.h
-      curseslibs="${libs}"
-      break
-    fi
-  done
-fi
-
-# Configuration for the libraries
-
-otherlibraries="unix str num dynlink bigarray"
-
-# For the Unix library
-
-has_sockets=no
-if sh ./hasgot socket socketpair bind listen accept connect; then
-  echo "You have BSD sockets."
-  echo "#define HAS_SOCKETS" >> s.h
-  has_sockets=yes
-elif sh ./hasgot -lnsl -lsocket socket socketpair bind listen accept connect; then
-  echo "You have BSD sockets (with libraries '-lnsl -lsocket')"
-  cclibs="$cclibs -lnsl -lsocket"
-  echo "#define HAS_SOCKETS" >> s.h
-  has_sockets=yes
-fi
-
-if sh ./hasgot -i sys/socket.h -t socklen_t; then
-  echo "socklen_t is defined in <sys/socket.h>"
-  echo "#define HAS_SOCKLEN_T" >> s.h
-fi
-
-if sh ./hasgot inet_aton; then
-  echo "inet_aton() found."
-  echo "#define HAS_INET_ATON" >> s.h
-fi
-
-if sh ./hasgot -i sys/types.h -i sys/socket.h -i netinet/in.h \
-               -t 'struct sockaddr_in6' \
-&& sh ./hasgot getaddrinfo getnameinfo inet_pton inet_ntop; then
-  echo "IPv6 is supported."
-  echo "#define HAS_IPV6" >> s.h
-fi
-
-if sh ./hasgot -i unistd.h; then
-  echo "unistd.h found."
-  echo "#define HAS_UNISTD" >> s.h
-fi
-
-if sh ./hasgot -i sys/types.h -t off_t; then
-  echo "off_t is defined in <sys/types.h>"
-  echo "#define HAS_OFF_T" >> s.h
-fi
-
-if sh ./hasgot -i sys/types.h -i dirent.h; then
-  echo "dirent.h found."
-  echo "#define HAS_DIRENT" >> s.h
-fi
-
-if sh ./hasgot rewinddir; then
-  echo "rewinddir() found."
-  echo "#define HAS_REWINDDIR" >> s.h
-fi
-
-if sh ./hasgot lockf; then
-  echo "lockf() found."
-  echo "#define HAS_LOCKF" >> s.h
-fi
-
-if sh ./hasgot mkfifo; then
-  echo "mkfifo() found."
-  echo "#define HAS_MKFIFO" >> s.h
-fi
-
-if sh ./hasgot getcwd; then
-  echo "getcwd() found."
-  echo "#define HAS_GETCWD" >> s.h
-fi
-
-if sh ./hasgot getwd; then
-  echo "getwd() found."
-  echo "#define HAS_GETWD" >> s.h
-fi
-
-if sh ./hasgot getpriority setpriority; then
-  echo "getpriority() found."
-  echo "#define HAS_GETPRIORITY" >> s.h
-fi
-
-if sh ./hasgot -i sys/types.h -i utime.h && sh ./hasgot utime; then
-  echo "utime() found."
-  echo "#define HAS_UTIME" >> s.h
-fi
-
-if sh ./hasgot utimes; then
-  echo "utimes() found."
-  echo "#define HAS_UTIMES" >> s.h
-fi
-
-if sh ./hasgot dup2; then
-  echo "dup2() found."
-  echo "#define HAS_DUP2" >> s.h
-fi
-
-if sh ./hasgot fchmod fchown; then
-  echo "fchmod() found."
-  echo "#define HAS_FCHMOD" >> s.h
-fi
-
-if sh ./hasgot truncate ftruncate; then
-  echo "truncate() found."
-  echo "#define HAS_TRUNCATE" >> s.h
-fi
-
-select_include=''
-if sh ./hasgot -i sys/types.h -i sys/select.h; then
-  echo "sys/select.h found."
-  echo "#define HAS_SYS_SELECT_H" >> s.h
-  select_include='-i sys/select.h'
-fi
-
-has_select=no
-if sh ./hasgot select && \
-   sh ./hasgot -i sys/types.h $select_include -t fd_set ; then
-  echo "select() found."
-  echo "#define HAS_SELECT" >> s.h
-  has_select=yes
-fi
-
-if sh ./hasgot symlink readlink lstat;  then
-  echo "symlink() found."
-  echo "#define HAS_SYMLINK" >> s.h
-fi
-
-has_wait=no
-if sh ./hasgot waitpid;  then
-  echo "waitpid() found."
-  echo "#define HAS_WAITPID" >> s.h
-  has_wait=yes
-fi
-
-if sh ./hasgot wait4;  then
-  echo "wait4() found."
-  echo "#define HAS_WAIT4" >> s.h
-  has_wait=yes
-fi
-
-if sh ./hasgot -i limits.h && sh ./runtest getgroups.c; then
-  echo "getgroups() found."
-  echo "#define HAS_GETGROUPS" >> s.h
-fi
-
-if sh ./hasgot -i termios.h &&
-   sh ./hasgot tcgetattr tcsetattr tcsendbreak tcflush tcflow; then
-  echo "POSIX termios found."
-  echo "#define HAS_TERMIOS" >> s.h
-fi
-
-# Async I/O under OSF1 3.x are so buggy that the test program hangs...
-testasyncio=true
-if test -f /usr/bin/uname; then
-  case "`/usr/bin/uname -s -r`" in
-    "OSF1 V3."*) testasyncio=false;;
-  esac
-fi
-if $testasyncio && sh ./runtest async_io.c; then
-  echo "Asynchronous I/O are supported."
-  echo "#define HAS_ASYNC_IO" >> s.h
-fi
-
-has_setitimer=no
-if sh ./hasgot setitimer; then
-  echo "setitimer() found."
-  echo "#define HAS_SETITIMER" >> s.h
-  has_setitimer="yes"
-fi
-
-if sh ./hasgot gethostname; then
-  echo "gethostname() found."
-  echo "#define HAS_GETHOSTNAME" >> s.h
-fi
-
-if sh ./hasgot -i sys/utsname.h && sh ./hasgot uname; then
-  echo "uname() found."
-  echo "#define HAS_UNAME" >> s.h
-fi
-
-has_gettimeofday=no
-if sh ./hasgot gettimeofday; then
-  echo "gettimeofday() found."
-  echo "#define HAS_GETTIMEOFDAY" >> s.h
-  has_gettimeofday="yes"
-fi
-
-if sh ./hasgot mktime; then
-  echo "mktime() found."
-  echo "#define HAS_MKTIME" >> s.h
-fi
-
-case "$host" in
-  *-*-cygwin*) ;;  # setsid emulation under Cygwin breaks the debugger
-  *) if sh ./hasgot setsid; then
-       echo "setsid() found."
-       echo "#define HAS_SETSID" >> s.h
-     fi;;
-esac
-
-if sh ./hasgot putenv; then
-  echo "putenv() found."
-  echo "#define HAS_PUTENV" >> s.h
-fi
-
-if sh ./hasgot -i locale.h && sh ./hasgot setlocale; then
-  echo "setlocale() and <locale.h> found."
-  echo "#define HAS_LOCALE" >> s.h
-fi
-
-if sh ./hasgot -i mach-o/dyld.h && sh ./hasgot NSLinkModule; then
-  echo "NSLinkModule() found. Using darwin dynamic loading."
-  echo "#define HAS_NSLINKMODULE" >> s.h
-elif sh ./hasgot $dllib dlopen; then
-  echo "dlopen() found."
-elif sh ./hasgot $dllib -ldl dlopen; then
-  echo "dlopen() found in -ldl."
-  dllib="$dllib -ldl"
-else
-  shared_libraries_supported=no
-fi
-
-if $shared_libraries_supported; then
-  echo "Dynamic loading of shared libraries is supported."
-  echo "#define SUPPORT_DYNAMIC_LINKING" >> s.h
-  if $dl_needs_underscore; then
-    echo '#define DL_NEEDS_UNDERSCORE' >>s.h
-  fi
-fi
-
-if sh ./hasgot -i sys/types.h -i sys/mman.h && sh ./hasgot mmap munmap; then
-  echo "mmap() found."
-  echo "#define HAS_MMAP" >> s.h
-fi
-
-nargs=none
-for i in 5 6; do
-  if sh ./trycompile -DNUM_ARGS=${i} gethostbyname.c; then nargs=$i; break; fi
-done
-if test $nargs != "none"; then
-  echo "gethostbyname_r() found (with ${nargs} arguments)."
-  echo "#define HAS_GETHOSTBYNAME_R $nargs" >> s.h
-fi
-
-nargs=none
-for i in 7 8; do
-  if sh ./trycompile -DNUM_ARGS=${i} gethostbyaddr.c; then nargs=$i; break; fi
-done
-if test $nargs != "none"; then
-  echo "gethostbyaddr_r() found (with ${nargs} arguments)."
-  echo "#define HAS_GETHOSTBYADDR_R $nargs" >> s.h
-fi
-
-# Determine if the debugger is supported
-
-if test "$has_sockets" = "yes"; then
-  echo "Replay debugger supported."
-  debugger="ocamldebugger"
-else
-  echo "No replay debugger (missing system calls)"
-  debugger=""
-fi
-
-
-# Determine if system stack overflows can be detected
-
-case "$arch,$system" in
-  i386,linux_elf|amd64,linux)
-    echo "System stack overflow can be detected."
-    echo "#define HAS_STACK_OVERFLOW_DETECTION" >> s.h;;
-  *)
-    echo "Cannot detect system stack overflow.";;
-esac
-
-# Determine the target architecture for the "num" library
-
-case "$host" in
-  alpha*-*-*)    bng_arch=alpha; bng_asm_level=1;;
-  i[3456]86-*-*) bng_arch=ia32
-                 if sh ./trycompile ia32sse2.c
-                 then bng_asm_level=2
-                 else bng_asm_level=1
-                 fi;;
-  mips-*-*)      bng_arch=mips; bng_asm_level=1;;
-  powerpc-*-*)   bng_arch=ppc; bng_asm_level=1;;
-  sparc*-*-*)    bng_arch=sparc; bng_asm_level=1;;
-  x86_64-*-*)    bng_arch=amd64; bng_asm_level=1;;
-  *)             bng_arch=generic; bng_asm_level=0;;
-esac
-
-echo "BNG_ARCH=$bng_arch" >> Makefile
-echo "BNG_ASM_LEVEL=$bng_asm_level" >> Makefile
-
-# Determine if the POSIX threads library is supported
-
-systhread_support=false
-
-if test "$pthread_wanted" = "yes"; then
-  case "$host" in
-    *-*-solaris*)  pthread_link="-lpthread -lposix4";;
-    *-*-freebsd*)  pthread_link="-pthread";;
-    *-*-openbsd*)  pthread_link="-pthread";;
-    *)             pthread_link="-lpthread";;
-  esac
-  if ./hasgot -i pthread.h $pthread_link pthread_self; then
-    echo "POSIX threads library supported."
-    systhread_support=true
-    otherlibraries="$otherlibraries systhreads"
-    bytecccompopts="$bytecccompopts -D_REENTRANT"
-    nativecccompopts="$nativecccompopts -D_REENTRANT"
-    case "$host" in
-      *-*-freebsd*)
-          bytecccompopts="$bytecccompopts -D_THREAD_SAFE"
-          nativecccompopts="$nativecccompopts -D_THREAD_SAFE";;
-      *-*-openbsd*)
-          bytecccompopts="$bytecccompopts -pthread"
-          asppflags="$asppflags -pthread"
-          nativecccompopts="$nativecccompopts -pthread";;
-    esac
-    echo "Options for linking with POSIX threads: $pthread_link"
-    echo "PTHREAD_LINK=$pthread_link" >> Makefile
-    if sh ./hasgot $pthread_link sigwait; then
-      echo "sigwait() found"
-      echo "#define HAS_SIGWAIT" >> s.h
-    fi
-  else
-    echo "POSIX threads not found."
-    pthread_link=""
-  fi
-fi
-
-# Determine if the bytecode thread library is supported
-
-if test "$has_select" = "yes" \
-&& test "$has_setitimer" = "yes" \
-&& test "$has_gettimeofday" = "yes" \
-&& test "$has_wait" = "yes"; then
-  echo "Bytecode threads library supported."
-  otherlibraries="$otherlibraries threads"
-else
-  echo "Bytecode threads library not supported (missing system calls)"
-fi
-
-# Determine the location of X include files and libraries
-
-x11_include="not found"
-x11_link="not found"
-
-for dir in \
-    $x11_include_dir          \
-    ; \
-do
-  if test -f $dir/X11/X.h; then
-    x11_include=$dir
-    break
-  fi
-done
-
-if test "$x11_include" = "not found"; then
-  x11_try_lib_dir=''
-else
-  x11_try_lib_dir=`echo $x11_include | sed -e 's|include|lib|'`
-fi
-
-for dir in \
-    $x11_lib_dir          \
-    $x11_try_lib_dir      \
-    ; \
-do
-  if test -f $dir/libX11.a || \
-     test -f $dir/libX11.so || \
-     test -f $dir/libX11.dll.a || \
-     test -f $dir/libX11.sa; then
-    if test $dir = /usr/lib; then
-      x11_link="-lX11"
-    else
-      x11_link="-L$dir -lX11"
-      x11_libs="-L$dir"
-    fi
-    break
-  fi
-done
-
-
-if test "$x11_include" = "not found" || test "$x11_link" = "not found"
-then
-  echo "X11 not found, the \"graph\" library will not be supported."
-  x11_include=""
-else
-  echo "Location of X11 include files: $x11_include/X11"
-  echo "Options for linking with X11: $x11_link"
-  otherlibraries="$otherlibraries graph"
-  if test "$x11_include" = "/usr/include"; then
-    x11_include=""
-  else
-    x11_include="-I$x11_include"
-  fi
-  echo "X11_INCLUDES=$x11_include" >> Makefile
-  echo "X11_LINK=$x11_link" >> Makefile
-fi
-
-# See if we can compile the dbm library
-
-dbm_include="not found"
-dbm_link="not found"
-use_gdbm_ndbm=no
-
-for dir in /usr/include /usr/include/db1 /usr/include/gdbm; do
-  if test -f $dir/ndbm.h; then
-    dbm_include=$dir
-    if sh ./hasgot dbm_open; then
-      dbm_link=""
-    elif sh ./hasgot -lndbm dbm_open; then
-      dbm_link="-lndbm"
-    elif sh ./hasgot -ldb1 dbm_open; then
-      dbm_link="-ldb1"
-    elif sh ./hasgot -lgdbm dbm_open; then
-      dbm_link="-lgdbm"
-    elif sh ./hasgot -lgdbm_compat -lgdbm dbm_open; then
-      dbm_link="-lgdbm_compat -lgdbm"
-    fi
-    break
-  fi
-  if test -f $dir/gdbm-ndbm.h; then
-    dbm_include=$dir
-    use_gdbm_ndbm=yes
-    if sh ./hasgot -lgdbm_compat -lgdbm dbm_open; then
-      dbm_link="-lgdbm_compat -lgdbm"
-    fi
-    break
-  fi
-done
-if test "$dbm_include" = "not found" || test "$dbm_link" = "not found"; then
-  echo "NDBM not found, the \"dbm\" library will not be supported."
-else
-  echo "NDBM found (in $dbm_include)"
-  if test "$dbm_include" = "/usr/include"; then
-    dbm_include=""
-  else
-    dbm_include="-I$dbm_include"
-  fi
-  echo "DBM_INCLUDES=$dbm_include" >> Makefile
-  echo "DBM_LINK=$dbm_link" >> Makefile
-  if test "$use_gdbm_ndbm" = "yes"; then
-    echo "#define DBM_USES_GDBM_NDBM" >> s.h
-  fi
-  otherlibraries="$otherlibraries dbm"
-fi
-
-# Look for tcl/tk
-
-echo "Configuring LablTk..."
-
-if test $tk_wanted = no; then
-  has_tk=false
-elif test $tk_x11 = no; then
-  has_tk=true
-elif test "$x11_include" = "not found" || test "$x11_link" = "not found"; then
-  echo "X11 not found."
-  has_tk=false
-else
-  tk_x11_include="$x11_include"
-  tk_x11_libs="$x11_libs -lX11"
-  has_tk=true
-fi
-
-if test $has_tk = true; then
-  tcl_version=''
-  tcl_version=`sh ./runtest $tk_defs $tk_x11_include tclversion.c`
-  for tk_incs in \
-    ;
-  do if test -z "$tcl_version"; then
-    tk_defs="$tk_incs"
-    tcl_version=`sh ./runtest $tk_defs $tk_x11_include tclversion.c`
-  fi; done
-  if test -n "$tcl_version" && test "x$tcl_version" != "xnone"; then
-    echo "tcl.h and tk.h version $tcl_version found with \"$tk_defs\"."
-    case $tcl_version in
-    7.5) tclmaj=7 tclmin=5 tkmaj=4 tkmin=1 ;;
-    7.6) tclmaj=7 tclmin=6 tkmaj=4 tkmin=2 ;;
-    8.0) tclmaj=8 tclmin=0 tkmaj=8 tkmin=0 ;;
-    8.1) tclmaj=8 tclmin=1 tkmaj=8 tkmin=1 ;;
-    8.2) tclmaj=8 tclmin=2 tkmaj=8 tkmin=2 ;;
-    8.3) tclmaj=8 tclmin=3 tkmaj=8 tkmin=3 ;;
-    8.4) tclmaj=8 tclmin=4 tkmaj=8 tkmin=4 ;;
-    *) echo "This version is not known."; has_tk=false ;;
-    esac
-  else
-    echo "tcl.h and/or tk.h not found."
-    has_tk=false
-  fi
-fi
-
-tkauxlibs="$mathlib $dllib"
-tcllib=''
-tklib=''
-if test $has_tk = true; then
-  if test -n "$tk_libs" && \
-     sh ./hasgot $tk_libs $tk_x11_libs $tkauxlibs Tcl_DoOneEvent
-  then tk_libs="$tk_libs $dllib"
-  elif sh ./hasgot $tk_libs -ltcl$tclmaj.$tclmin $tkauxlibs Tcl_DoOneEvent
-  then
-    tk_libs="$tk_libs -ltk$tkmaj.$tkmin -ltcl$tclmaj.$tclmin $dllib"
-  elif sh ./hasgot $tk_libs -ltcl$tclmaj$tclmin $tkauxlibs Tcl_DoOneEvent
-  then
-    tk_libs="$tk_libs -ltk$tkmaj$tkmin -ltcl$tclmaj$tclmin $dllib"
-  elif test -z "$tk_libs" && tk_libs=-L/usr/local/lib && \
-    sh ./hasgot $tk_libs -ltcl$tclmaj.$tclmin $tkauxlibs Tcl_DoOneEvent
-  then
-    tk_libs="$tk_libs -ltk$tkmaj.$tkmin -ltcl$tclmaj.$tclmin $dllib"
-  elif sh ./hasgot $tk_libs -ltcl$tclmaj$tclmin $tkauxlibs Tcl_DoOneEvent
-  then
-    tk_libs="$tk_libs -ltk$tkmaj$tkmin -ltcl$tclmaj$tclmin $dllib"
-  elif sh ./hasgot -L/sw/lib $tk_libs -ltcl$tclmaj.$tclmin $tkauxlibs \
-                   Tcl_DoOneEvent
-  then tk_libs="-L/sw/lib -ltk$tkmaj.$tkmin -ltcl$tclmaj.$tclmin $dllib"
-  else
-    echo "Tcl library not found."
-    has_tk=false
-  fi
-fi
-if test $has_tk = true; then
-  if sh ./hasgot $tk_libs $tk_x11_libs $tkauxlibs Tk_SetGrid; then
-    echo "Tcl/Tk libraries found."
-  elif sh ./hasgot -L/sw/lib $tk_libs $tk_x11_libs $tkauxlibs Tk_SetGrid; then
-    tk_libs="-L/sw/lib $tk_libs"
-    echo "Tcl/Tk libraries found."
-  else
-    echo "Tcl library found."
-    echo "Tk library not found."
-    has_tk=false
-  fi
-fi
-
-if test $has_tk = true; then
-  if test $tk_x11 = yes; then
-    echo "TK_DEFS=$tk_defs "'$(X11_INCLUDES)' >> Makefile
-    echo "TK_LINK=$tk_libs "'$(X11_LINK)' >> Makefile
-  else
-    echo "TK_DEFS=$tk_defs" >> Makefile
-    echo "TK_LINK=$tk_libs" >> Makefile
-  fi
-  otherlibraries="$otherlibraries labltk"
-else
-  echo "Configuration failed, LablTk will not be built."
-fi
-
-# Begin Camlp4
-(
-cd ../../camlp4/config
-EXE=$exe ./configure_batch -prefix "$prefix" -bindir "$bindir" -libdir "$libdir" -mandir "$mandir" -ocaml-top ../.. > /dev/null
-)
-
-case $? in
-    0) echo "Camlp4 correctly configured.";;
-    *) echo "Warning: Camlp4 configuration terminated with error code $?";;
-esac
-# End Camlp4
-
-# Final twiddling of compiler options to work around known bugs
-
-nativeccprofopts="$nativecccompopts"
-case "$buggycc" in
-  gcc.2.96)
-    bytecccompopts="$bytecccompopts -fomit-frame-pointer"
-    nativecccompopts="$nativecccompopts -fomit-frame-pointer";;
-esac
-
-# Finish generated files
-
-cclibs="$cclibs $mathlib"
-
-echo "BYTECC=$bytecc" >> Makefile
-echo "BYTECCCOMPOPTS=$bytecccompopts" >> Makefile
-echo "BYTECCLINKOPTS=$bytecclinkopts" >> Makefile
-echo "BYTECCLIBS=$cclibs $dllib $curseslibs $pthread_link" >> Makefile
-echo "BYTECCRPATH=$byteccrpath" >> Makefile
-echo "EXE=$exe" >> Makefile
-echo "SUPPORTS_SHARED_LIBRARIES=$shared_libraries_supported" >> Makefile
-echo "SHAREDCCCOMPOPTS=$sharedcccompopts" >> Makefile
-echo "MKSHAREDLIB=$mksharedlib" >> Makefile
-echo "MKSHAREDLIBRPATH=$mksharedlibrpath" >> Makefile
-echo "ARCH=$arch" >> Makefile
-echo "MODEL=$model" >> Makefile
-echo "SYSTEM=$system" >> Makefile
-echo "NATIVECC=$nativecc" >> Makefile
-echo "NATIVECCCOMPOPTS=$nativecccompopts" >> Makefile
-echo "NATIVECCPROFOPTS=$nativeccprofopts" >> Makefile
-echo "NATIVECCLINKOPTS=$nativecclinkopts" >> Makefile
-echo "NATIVECCRPATH=$nativeccrpath" >> Makefile
-echo "NATIVECCLIBS=$cclibs $dllib" >> Makefile
-echo "ASFLAGS=$asflags" >> Makefile
-echo "ASPP=$aspp" >> Makefile
-echo "ASPPFLAGS=$asppflags" >> Makefile
-echo "ASPPPROFFLAGS=$asppprofflags" >> Makefile
-echo "PROFILING=$profiling" >> Makefile
-echo "DYNLINKOPTS=$dllib" >> Makefile
-echo "OTHERLIBRARIES=$otherlibraries" >> Makefile
-echo "DEBUGGER=$debugger" >> Makefile
-echo "CC_PROFILE=$cc_profile" >> Makefile
-echo "SYSTHREAD_SUPPORT=$systhread_support" >>Makefile
-
-rm -f tst hasgot.c
-rm -f ../m.h ../s.h ../Makefile
-mv m.h s.h Makefile ..
-
-# Print a summary
-
-echo
-echo "** Configuration summary **"
-echo
-echo "Directories where Objective Caml will be installed:"
-echo "        binaries.................. $bindir"
-echo "        standard library.......... $libdir"
-echo "        manual pages.............. $mandir (with extension .$manext)"
-
-echo "Configuration for the bytecode compiler:"
-echo "        C compiler used........... $bytecc"
-echo "        options for compiling..... $bytecccompopts"
-echo "        options for linking....... $bytecclinkopts $cclibs $dllib $curseslibs $pthread_link"
-if $shared_libraries_supported; then
-echo "        shared libraries are supported"
-echo "        options for compiling..... $sharedcccompopts $bytecccompopts"
-echo "        command for building...... $mksharedlib lib.so $mksharedlibrpath/a/path objs"
-else
-echo "        shared libraries not supported"
-fi
-
-echo "Configuration for the native-code compiler:"
-if test "$arch" = "none"; then
-  echo "        (not supported on this platform)"
-else
-  if test "$model" = "default"; then
-    echo "        hardware architecture..... $arch"
-  else
-    echo "        hardware architecture..... $arch ($model)"
-  fi
-  if test "$system" = "unknown"; then : ; else
-  echo "        OS variant................ $system"
-  fi
-  echo "        C compiler used........... $nativecc"
-  echo "        options for compiling..... $nativecccompopts"
-  echo "        options for linking....... $nativecclinkopts $cclibs"
-  echo "        assembler ................ \$(AS) $asflags"
-  echo "        preprocessed assembler ... $aspp $asppflags"
-  if test "$profiling" = "prof"; then
-  echo "        profiling with gprof ..... supported"
-  else
-  echo "        profiling with gprof ..... not supported"
-  fi
-fi
-
-if test "$debugger" = "ocamldebugger"; then
-  echo "Source-level replay debugger: supported"
-else
-  echo "Source-level replay debugger: not supported"
-fi
-
-echo "Additional libraries supported:"
-echo "        $otherlibraries"
-
-echo "Configuration for the \"num\" library:"
-echo "        target architecture ...... $bng_arch (asm level $bng_asm_level)"
-
-if test "$x11_include" != "not found" && test "$x11_lib" != "not found"; then
-echo "Configuration for the \"graph\" library:"
-echo "        options for compiling .... $x11_include"
-echo "        options for linking ...... $x11_link"
-fi
-
-if test $has_tk = true; then
-echo "Configuration for the \"labltk\" library:"
-echo "        use tcl/tk version ....... $tcl_version"
-echo "        options for compiling .... $tk_defs"
-echo "        options for linking ...... $tk_libs"
-else
-echo "The \"labltk\" library: not supported"
-fi
-
-echo
-echo "** Objective Caml configuration completed successfully **"
-echo
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 61b9ba585b88..48ed8526d25d 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,56 +1,40 @@
-{stdenv, fetchurl, ocaml_with_sources}:
+{stdenv, fetchsvn, ocaml, camlp5_transitional}:
 
-let
-  pname = "hol_light";
-  version = "100110";
-  webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+stdenv.mkDerivation rec {
+  name = "hol_light-${version}";
+  version = "20100820svn57";
 
-  dmtcp_checkpoint = ''
+  inherit ocaml;
+  camlp5 = camlp5_transitional;
 
-(* ------------------------------------------------------------------------- *)
-(* 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";
+  src = fetchsvn {
+    url = http://hol-light.googlecode.com/svn/trunk;
+    rev = "57";
+    sha256 = "d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
   };
 
-  buildInputs = [ ocaml_with_sources ];
+  buildInputs = [ ocaml camlp5 ];
 
   buildCommand = ''
-    ensureDir "$out/src"
-    cd "$out/src"
-
-    tar -xzf "$src"
-    cd hol_light
+    export HOL_DIR="$out/src/hol_light"
+    ensureDir `dirname $HOL_DIR` "$out/bin"
+    cp -a "${src}" "$HOL_DIR"
+    cd "$HOL_DIR"
+    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 \
-      "Filename.concat ocaml_source_dir" \
-      "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
+    substituteInPlace Makefile --replace \
+      "+camlp5" \
+      "${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" ];
   };
 }
diff --git a/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix b/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix
deleted file mode 100644
index 7e6d8becc9dd..000000000000
--- a/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix
+++ /dev/null
@@ -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";
-  };
-}
diff --git a/pkgs/applications/science/logic/hol_light/restart_hol_light b/pkgs/applications/science/logic/hol_light/restart_hol_light
new file mode 100644
index 000000000000..d4fe70368d97
--- /dev/null
+++ b/pkgs/applications/science/logic/hol_light/restart_hol_light
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec @DMTCP_RESTART@ --quiet @CKPT_FILE@
diff --git a/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml b/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml
deleted file mode 100644
index d522f4919c28..000000000000
--- a/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml
+++ /dev/null
@@ -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";;
diff --git a/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml b/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml
deleted file mode 100644
index 432b676ba2f6..000000000000
--- a/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml
+++ /dev/null
@@ -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 "";;
\ No newline at end of file
diff --git a/pkgs/applications/science/logic/hol_light/selfcheckpoint_multivariate.ml b/pkgs/applications/science/logic/hol_light/selfcheckpoint_multivariate.ml
deleted file mode 100644
index d805b4af2343..000000000000
--- a/pkgs/applications/science/logic/hol_light/selfcheckpoint_multivariate.ml
+++ /dev/null
@@ -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";;
diff --git a/pkgs/applications/science/logic/hol_light/start_hol.ml b/pkgs/applications/science/logic/hol_light/start_hol.ml
new file mode 100644
index 000000000000..c8f4b2279df2
--- /dev/null
+++ b/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";;
diff --git a/pkgs/applications/science/logic/hol_light/start_hol_light b/pkgs/applications/science/logic/hol_light/start_hol_light
new file mode 100644
index 000000000000..638cf8d3e772
--- /dev/null
+++ b/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@ "$@"