From 1ed2297c4d2c6145359f679510be0ccc39e351e1 Mon Sep 17 00:00:00 2001 From: maggesi Date: Mon, 15 Feb 2010 11:00:02 +0000 Subject: [PATCH] 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. git-svn-id: https://svn.nixos.org/repos/nix/nixpkgs/trunk@20008 70bd8c7a-acb8-0310-9f0d-9cc1c95dcdbb --- .../editors/emacs-modes/hol_light/default.nix | 25 + .../science/logic/hol_light/binaries.nix | 55 + .../science/logic/hol_light/configure-3.09.3 | 1444 ++++++++++++++++++++ .../science/logic/hol_light/default.nix | 72 + .../science/logic/hol_light/ocaml-with-sources.nix | 33 + .../logic/hol_light/selfcheckpoint_complex.ml | 29 + .../science/logic/hol_light/selfcheckpoint_core.ml | 28 + .../logic/hol_light/selfcheckpoint_multivariate.ml | 29 + pkgs/top-level/all-packages.nix | 22 + 9 files changed, 1737 insertions(+) create mode 100644 pkgs/applications/editors/emacs-modes/hol_light/default.nix create mode 100644 pkgs/applications/science/logic/hol_light/binaries.nix create mode 100755 pkgs/applications/science/logic/hol_light/configure-3.09.3 create mode 100644 pkgs/applications/science/logic/hol_light/default.nix create mode 100644 pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix create mode 100644 pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml create mode 100644 pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml create mode 100644 pkgs/applications/science/logic/hol_light/selfcheckpoint_multivariate.ml diff --git a/pkgs/applications/editors/emacs-modes/hol_light/default.nix b/pkgs/applications/editors/emacs-modes/hol_light/default.nix new file mode 100644 index 000000000..9dba1d599 --- /dev/null +++ b/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"; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/binaries.nix b/pkgs/applications/science/logic/hol_light/binaries.nix new file mode 100644 index 000000000..41d2f8237 --- /dev/null +++ b/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"; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/configure-3.09.3 b/pkgs/applications/science/logic/hol_light/configure-3.09.3 new file mode 100755 index 000000000..c52776894 --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/configure-3.09.3 @@ -0,0 +1,1444 @@ +#! /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 to proceed or 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 " + 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 " + 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 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 new file mode 100644 index 000000000..61b9ba585 --- /dev/null +++ b/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"; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix b/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix new file mode 100644 index 000000000..7e6d8becc --- /dev/null +++ b/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"; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml b/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml new file mode 100644 index 000000000..d522f4919 --- /dev/null +++ b/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";; diff --git a/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml b/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml new file mode 100644 index 000000000..432b676ba --- /dev/null +++ b/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 "";; \ 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 new file mode 100644 index 000000000..d805b4af2 --- /dev/null +++ b/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";; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index b60b86266..d9f00ae81 100644 --- a/pkgs/top-level/all-packages.nix +++ b/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; }; -- 2.11.4.GIT