diff --git a/pkgs/applications/science/logic/coq/configure.patch b/pkgs/applications/science/logic/coq/configure.patch index 3989ea5c601..431cccac4b0 100644 --- a/pkgs/applications/science/logic/coq/configure.patch +++ b/pkgs/applications/science/logic/coq/configure.patch @@ -1,7 +1,7 @@ -diff -Nuar coq-8.3/configure coq-8.3.nixos/configure ---- coq-8.3/configure 2010-10-14 16:02:46.000000000 +0200 -+++ coq-8.3.nixos/configure 2010-11-04 09:57:16.000000000 +0100 -@@ -394,7 +394,6 @@ +diff -Nuar coq-8.3pl3-orig/configure coq-8.3pl3/configure +--- coq-8.3pl3-orig/configure 2011-12-19 22:57:30.000000000 +0100 ++++ coq-8.3pl3/configure 2012-03-17 16:38:16.000000000 +0100 +@@ -395,7 +395,6 @@ ocamlyaccexec=$CAMLBIN/ocamlyacc ocamlmktopexec=$CAMLBIN/ocamlmktop ocamlmklibexec=$CAMLBIN/ocamlmklib @@ -9,12 +9,1104 @@ diff -Nuar coq-8.3/configure coq-8.3.nixos/configure esac if test ! -f "$CAMLC" ; then -@@ -637,7 +636,7 @@ +@@ -628,7 +627,7 @@ no) LABLGTKLIB=+lablgtk2 # Pour le message LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile yes) LABLGTKLIB="$lablgtkdir" # Pour le message - LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile -+ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile ++ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile esac;; no) LABLGTKINCLUDES="";; esac +diff -Nuar coq-8.3pl3-orig/configure~ coq-8.3pl3/configure~ +--- coq-8.3pl3-orig/configure~ 1970-01-01 01:00:00.000000000 +0100 ++++ coq-8.3pl3/configure~ 2011-12-19 22:57:30.000000000 +0100 +@@ -0,0 +1,1088 @@ ++#!/bin/sh ++ ++################################## ++# ++# Configuration script for Coq ++# ++################################## ++ ++VERSION=8.3pl3 ++VOMAGIC=08300 ++STATEMAGIC=58300 ++DATE=`LANG=C date +"%B %Y"` ++ ++# Create the bin/ directory if non-existent ++test -d bin || mkdir bin ++ ++# a local which command for sh ++which () { ++IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames) ++for i in $PATH; do ++ if test -z "$i"; then i=.; fi ++ if [ -f "$i/$1" ] ; then ++ IFS=" " ++ echo "$i/$1" ++ break ++ fi ++done ++} ++ ++usage () { ++ printf "Available options for configure are:\n" ++ echo "-help" ++ printf "\tDisplays this help page\n" ++ echo "-prefix " ++ printf "\tSet installation directory to \n" ++ echo "-local" ++ printf "\tSet installation directory to the current source tree\n" ++ echo "-coqrunbyteflags" ++ printf "\tSet link flags for VM-dependent bytecode (coqtop)\n" ++ echo "-coqtoolsbyteflags" ++ printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n" ++ echo "-custom" ++ printf "\tGenerate all bytecode executables with -custom (not recommended)\n" ++ echo "-src" ++ printf "\tSpecifies the source directory\n" ++ echo "-bindir" ++ echo "-libdir" ++ echo "-mandir" ++ echo "-docdir" ++ printf "\tSpecifies where to install bin/lib/man/doc files resp.\n" ++ echo "-emacslib" ++ echo "-emacs" ++ printf "\tSpecifies where emacs files are to be installed\n" ++ echo "-coqdocdir" ++ printf "\tSpecifies where Coqdoc style files are to be installed\n" ++ echo "-camldir" ++ printf "\tSpecifies the path to the OCaml library\n" ++ echo "-lablgtkdir" ++ printf "\tSpecifies the path to the Lablgtk library\n" ++ echo "-camlp5dir" ++ printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n" ++ echo "-arch" ++ printf "\tSpecifies the architecture\n" ++ echo "-opt" ++ printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n" ++ echo "-natdynlink (yes|no)" ++ printf "\tSpecifies whether or not to use dynamic loading of native code\n" ++ echo "-coqide (opt|byte|no)" ++ printf "\tSpecifies whether or not to compile Coqide\n" ++ echo "-browser " ++ printf "\tUse to open URL %%s\n" ++ echo "-with-doc (yes|no)" ++ printf "\tSpecifies whether or not to compile the documentation\n" ++ echo "-with-geoproof (yes|no)" ++ printf "\tSpecifies whether or not to use Geoproof binding\n" ++ echo "-with-cc " ++ echo "-with-ar " ++ echo "-with-ranlib " ++ printf "\tTells configure where to find gcc/ar/ranlib executables\n" ++ echo "-byte-only" ++ printf "\tCompiles only bytecode version of Coq\n" ++ echo "-debug" ++ printf "\tAdd debugging information in the Coq executables\n" ++ echo "-profile" ++ printf "\tAdd profiling information in the Coq executables\n" ++ echo "-annotate" ++ printf "\tCompiles Coq with -dtypes option\n" ++} ++ ++ ++# Default OCaml binaries ++bytecamlc=ocamlc ++nativecamlc=ocamlopt ++ocamlmklibexec=ocamlmklib ++ocamlexec=ocaml ++ocamldepexec=ocamldep ++ocamldocexec=ocamldoc ++ocamllexexec=ocamllex ++ocamlyaccexec=ocamlyacc ++ocamlmktopexec=ocamlmktop ++camlp4oexec=camlp4o ++ ++ ++coq_debug_flag= ++coq_debug_flag_opt= ++coq_profile_flag= ++coq_annotate_flag= ++best_compiler=opt ++cflags="-fno-defer-pop -Wall -Wno-unused" ++natdynlink=yes ++ ++gcc_exec=gcc ++ar_exec=ar ++ranlib_exec=ranlib ++ ++local=false ++coqrunbyteflags_spec=no ++coqtoolsbyteflags_spec=no ++custom_spec=no ++src_spec=no ++prefix_spec=no ++bindir_spec=no ++libdir_spec=no ++mandir_spec=no ++docdir_spec=no ++emacslib_spec=no ++emacs_spec=no ++camldir_spec=no ++lablgtkdir_spec=no ++coqdocdir_spec=no ++arch_spec=no ++coqide_spec=no ++browser_spec=no ++wwwcoq_spec=no ++with_geoproof=false ++with_doc=all ++with_doc_spec=no ++force_caml_version=no ++force_caml_version_spec=no ++ ++COQSRC=`pwd` ++ ++# Parse command-line arguments ++ ++while : ; do ++ case "$1" in ++ "") break;; ++ -help|--help) usage ++ exit;; ++ -prefix|--prefix) prefix_spec=yes ++ prefix="$2" ++ shift;; ++ -local|--local) local=true;; ++ -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes ++ coqrunbyteflags="$2" ++ shift;; ++ -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes ++ coqtoolsbyteflags="$2" ++ shift;; ++ -custom|--custom) custom_spec=yes ++ shift;; ++ -src|--src) src_spec=yes ++ COQSRC="$2" ++ shift;; ++ -bindir|--bindir) bindir_spec=yes ++ bindir="$2" ++ shift;; ++ -libdir|--libdir) libdir_spec=yes ++ libdir="$2" ++ shift;; ++ -mandir|--mandir) mandir_spec=yes ++ mandir="$2" ++ shift;; ++ -docdir|--docdir) docdir_spec=yes ++ docdir="$2" ++ shift;; ++ -emacslib|--emacslib) emacslib_spec=yes ++ emacslib="$2" ++ shift;; ++ -emacs |--emacs) emacs_spec=yes ++ emacs="$2" ++ shift;; ++ -coqdocdir|--coqdocdir) coqdocdir_spec=yes ++ coqdocdir="$2" ++ shift;; ++ -camldir|--camldir) camldir_spec=yes ++ camldir="$2" ++ shift;; ++ -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes ++ lablgtkdir="$2" ++ shift;; ++ -camlp5dir|--camlp5dir) ++ camlp5dir="$2" ++ shift;; ++ -arch|--arch) arch_spec=yes ++ arch=$2 ++ shift;; ++ -opt|--opt) bytecamlc=ocamlc.opt ++ camlp4oexec=camlp4o # can't add .opt since dyn load'll be required ++ nativecamlc=ocamlopt.opt;; ++ -natdynlink|--natdynlink) case "$2" in ++ yes) natdynlink=yes;; ++ *) natdynlink=no ++ esac ++ shift;; ++ -coqide|--coqide) coqide_spec=yes ++ case "$2" in ++ byte|opt) COQIDE=$2;; ++ *) COQIDE=no ++ esac ++ shift;; ++ -browser|--browser) browser_spec=yes ++ BROWSER=$2 ++ shift;; ++ -coqwebsite|--coqwebsite) wwwcoq_spec=yes ++ WWWCOQ=$2 ++ shift;; ++ -with-doc|--with-doc) with_doc_spec=yes ++ case "$2" in ++ yes|all) with_doc=all;; ++ *) with_doc=no ++ esac ++ shift;; ++ -with-geoproof|--with-geoproof) ++ case "$2" in ++ yes) with_geoproof=true;; ++ no) with_geoproof=false;; ++ esac ++ shift;; ++ -with-cc|-with-gcc|--with-cc|--with-gcc) ++ gcc_spec=yes ++ gcc_exec=$2 ++ shift;; ++ -with-ar|--with-ar) ++ ar_spec=yes ++ ar_exec=$2 ++ shift;; ++ -with-ranlib|--with-ranlib) ++ ranlib_spec=yes ++ ranlib_exec=$2 ++ shift;; ++ -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; ++ -debug|--debug) coq_debug_flag=-g;; ++ -profile|--profile) coq_profile_flag=-p;; ++ -annotate|--annotate) coq_annotate_flag=-dtypes;; ++ -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) ++ force_caml_version_spec=yes ++ force_caml_version=yes;; ++ *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;; ++ esac ++ shift ++done ++ ++if [ $prefix_spec = yes -a $local = true ] ; then ++ echo "Options -prefix and -local are incompatible." ++ echo "Configure script failed!" ++ exit 1 ++fi ++ ++# compile date ++DATEPGM=`which date` ++case $DATEPGM in ++ "") echo "I can't find the program \"date\" in your path." ++ echo "Please give me the current date" ++ read COMPILEDATE;; ++ *) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;; ++esac ++ ++# Architecture ++ ++case $arch_spec in ++ no) ++ # First we test if we are running a Cygwin system ++ if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then ++ ARCH="win32" ++ else ++ # If not, we determine the architecture ++ if test -x /bin/arch ; then ++ ARCH=`/bin/arch` ++ elif test -x /usr/bin/arch ; then ++ ARCH=`/usr/bin/arch` ++ elif test -x /usr/ucb/arch ; then ++ ARCH=`/usr/ucb/arch` ++ elif test -x /bin/uname ; then ++ ARCH=`/bin/uname -s` ++ elif test -x /usr/bin/uname ; then ++ ARCH=`/usr/bin/uname -s` ++ else ++ echo "I can not automatically find the name of your architecture." ++ printf "%s"\ ++ "Give me a name, please [win32 for Win95, Win98 or WinNT]: " ++ read ARCH ++ fi ++ fi;; ++ yes) ARCH=$arch ++esac ++ ++# executable extension ++ ++case $ARCH in ++ win32) ++ EXE=".exe" ++ DLLEXT=".dll";; ++ *) EXE="" ++ DLLEXT=".so" ++esac ++ ++# Is the source tree checked out from a recognised ++# version control system ? ++if test -e .svn/entries ; then ++ checkedout=svn ++elif [ -d '{arch}' ]; then ++ checkedout=gnuarch ++elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then ++ checkedout=git ++else ++ checkedout=0 ++fi ++ ++# make command ++ ++MAKE=`which make` ++if [ "$MAKE" != "" ]; then ++ MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` ++ MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` ++ MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` ++ if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then ++ echo "You have GNU Make $MAKEVERSION. Good!" ++ else ++ OK="no" ++ if [ -x ./make ]; then ++ MAKEVERSION=`./make -v | head -1` ++ if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi ++ fi ++ if [ $OK = "no" ]; then ++ echo "GNU Make >= 3.81 is needed." ++ echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz" ++ echo "then locally installed on a Unix-style system by issuing:" ++ echo " tar xzvf make-3.81.tar.gz" ++ echo " cd make-3.81" ++ echo " ./configure" ++ echo " make" ++ echo " mv make .." ++ echo " cd .." ++ echo "Restart then the configure script and later use ./make instead of make." ++ exit 1 ++ else ++ echo "You have locally installed GNU Make 3.81. Good!" ++ fi ++ fi ++else ++ echo "Cannot find GNU Make >= 3.81." ++fi ++ ++# Browser command ++ ++if [ "$browser_spec" = "no" ]; then ++ case $ARCH in ++ win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;; ++ *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;; ++ esac ++fi ++ ++if [ "$wwwcoq_spec" = "no" ]; then ++ WWWCOQ="http://coq.inria.fr/" ++fi ++ ++######################################### ++# Objective Caml programs ++ ++case $camldir_spec in ++ no) CAMLC=`which $bytecamlc` ++ case "$CAMLC" in ++ "") echo "$bytecamlc is not present in your path!" ++ echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: " ++ read CAMLC ++ ++ case "$CAMLC" in ++ "") CAMLC=/usr/local/bin/$bytecamlc;; ++ */ocamlc|*/ocamlc.opt) true;; ++ */) CAMLC="${CAMLC}"$bytecamlc;; ++ *) CAMLC="${CAMLC}"/$bytecamlc;; ++ esac ++ esac ++ CAMLBIN=`dirname "$CAMLC"`;; ++ yes) CAMLC=$camldir/$bytecamlc ++ ++ CAMLBIN=`dirname "$CAMLC"` ++ bytecamlc="$CAMLC" ++ nativecamlc=$CAMLBIN/$nativecamlc ++ ocamlexec=$CAMLBIN/ocaml ++ ocamldepexec=$CAMLBIN/ocamldep ++ ocamldocexec=$CAMLBIN/ocamldoc ++ ocamllexexec=$CAMLBIN/ocamllex ++ ocamlyaccexec=$CAMLBIN/ocamlyacc ++ ocamlmktopexec=$CAMLBIN/ocamlmktop ++ ocamlmklibexec=$CAMLBIN/ocamlmklib ++ camlp4oexec=$CAMLBIN/camlp4o ++esac ++ ++if test ! -f "$CAMLC" ; then ++ echo "I can not find the executable '$CAMLC'. Have you installed it?" ++ echo "Configuration script failed!" ++ exit 1 ++fi ++ ++# Under Windows, OCaml only understands Windows filenames (C:\...) ++case $ARCH in ++ win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;; ++esac ++ ++CAMLVERSION=`"$bytecamlc" -version` ++ ++case $CAMLVERSION in ++ 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*) ++ echo "Your version of Objective-Caml is $CAMLVERSION." ++ if [ "$force_caml_version" = "yes" ]; then ++ echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." ++ else ++ echo " You need Objective-Caml 3.10.2 or later." ++ echo " Configuration script failed!" ++ exit 1 ++ fi;; ++ ?*) ++ CAMLP4COMPAT="-loc loc" ++ echo "You have Objective-Caml $CAMLVERSION. Good!";; ++ *) ++ echo "I found the Objective-Caml compiler but cannot find its version number!" ++ echo "Is it installed properly?" ++ echo "Configuration script failed!" ++ exit 1;; ++esac ++ ++CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` ++ ++# For coqmktop & bytecode compiler ++ ++case $ARCH in ++ win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB ++ CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;; ++ *) ++ CAMLLIB=`"$CAMLC" -where` ++esac ++ ++if [ "$coq_debug_flag" = "-g" ]; then ++ case $CAMLTAG in ++ OCAML31*) ++ # Compilation debug flag ++ coq_debug_flag_opt="-g" ++ ;; ++ esac ++fi ++ ++# Native dynlink ++if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then ++ HASNATDYNLINK=true ++else ++ HASNATDYNLINK=false ++fi ++ ++case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in ++ true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy ++ NATDYNLINKFLAG=os5fixme;; ++ #Possibly a problem on 10.6.0/10.6.1/10.6.2 ++ #May just be a 32 vs 64 problem for all 10.6.* ++ true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 ++ NATDYNLINKFLAG=os5fixme;; ++ true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 ++ NATDYNLINKFLAG=os5fixme;; ++ true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 ++ NATDYNLINKFLAG=os5fixme;; ++ true,Darwin,10.*,3.11.*) ++ if [ `getconf LONG_BIT` = "32" ]; then ++ # Still a problem for x86_32 ++ NATDYNLINKFLAG=os5fixme ++ else ++ # Not a problem for x86_64 ++ NATDYNLINKFLAG=$HASNATDYNLINK ++ fi;; ++ *) ++ NATDYNLINKFLAG=$HASNATDYNLINK;; ++esac ++ ++# Camlp4 / Camlp5 configuration ++ ++if [ "$camlp5dir" != "" ]; then ++ CAMLP4=camlp5 ++ CAMLP4LIB=$camlp5dir ++ if [ ! -f $camlp5dir/camlp5.cma ]; then ++ echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)." ++ echo "Configuration script failed!" ++ exit 1 ++ fi ++ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` ++else ++ case $CAMLTAG in ++ OCAML31*) ++ if [ -x "${CAMLLIB}/camlp5" ]; then ++ CAMLP4LIB=+camlp5 ++ elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then ++ CAMLP4LIB=+site-lib/camlp5 ++ else ++ echo "Objective Caml $CAMLVERSION found but no Camlp5 installed." ++ echo "Configuration script failed!" ++ exit 1 ++ fi ++ CAMLP4=camlp5 ++ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` ++ ;; ++ *) ++ CAMLP4=camlp4 ++ CAMLP4LIB=+camlp4 ++ ;; ++ esac ++fi ++ ++if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then ++ echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK" ++ echo "(depending also on your ocaml version)." ++ echo "Configuration script failed!" ++ exit 1 ++fi ++ ++ ++case $CAMLP4LIB in ++ +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;; ++ *) FULLCAMLP4LIB=$CAMLP4LIB;; ++esac ++ ++# Assume that camlp(4|5) binaries are at the same place as ocaml ones ++# (this should become configurable some day) ++CAMLP4BIN=${CAMLBIN} ++ ++# do we have a native compiler: test of ocamlopt and its version ++ ++if [ "$best_compiler" = "opt" ] ; then ++ if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then ++ CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` ++ if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then ++ case $CAMLOPTVERSION in ++ 3.09.3|3.1?*) ;; ++ *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3," ++ best_compiler=byte ++ echo "only the bytecode version of Coq will be available." ++ esac ++ elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then ++ best_compiler=byte ++ echo "Cannot find native-code $CAMLP4," ++ echo "only the bytecode version of Coq will be available." ++ else ++ if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then ++ echo "Native and bytecode compilers do not have the same version!" ++ fi ++ echo "You have native-code compilation. Good!" ++ fi ++ else ++ best_compiler=byte ++ echo "You have only bytecode compilation." ++ fi ++fi ++ ++# OS dependent libraries ++ ++case $ARCH in ++ sun4*) OS=`uname -r` ++ case $OS in ++ 5*) OS="Sun Solaris $OS" ++ OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";; ++ *) OS="Sun OS $OS" ++ OSDEPLIBS="-cclib -lunix" ++ esac;; ++ alpha) OSDEPLIBS="-cclib -lunix";; ++ win32) OS="Win32" ++ OSDEPLIBS="-cclib -lunix" ++ cflags="-mno-cygwin $cflags";; ++ *) OSDEPLIBS="-cclib -lunix" ++esac ++ ++# lablgtk2 and CoqIDE ++ ++# -byte-only should imply -coqide byte, unless the user decides otherwise ++ ++if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then ++ coqide_spec=yes ++ COQIDE=byte ++fi ++ ++# Which coqide is asked ? which one is possible ? ++ ++if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then ++ echo "CoqIde disabled as requested." ++else ++ case $lablgtkdir_spec in ++ no) ++ if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then ++ lablgtkdir=${CAMLLIB}/lablgtk2 ++ elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then ++ lablgtkdir=${CAMLLIB}/site-lib/lablgtk2 ++ fi;; ++ yes) ++ if [ ! -f "$lablgtkdir/glib.mli" ]; then ++ echo "Incorrect LablGtk2 library (glib.mli not found)." ++ echo "Configuration script failed!" ++ exit 1 ++ fi;; ++ esac ++ if [ "$lablgtkdir" = "" ]; then ++ echo "LablGtk2 not found: CoqIde will not be available." ++ COQIDE=no ++ elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then ++ echo "LablGtk2 found but too old: CoqIde will not be available." ++ COQIDE=no; ++ elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then ++ echo "LablGtk2 found, bytecode CoqIde will be used as requested." ++ COQIDE=byte ++ elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then ++ echo "LablGtk2 found, no native threads: bytecode CoqIde will be available." ++ COQIDE=byte ++ else ++ echo "LablGtk2 found, native threads: native CoqIde will be available." ++ COQIDE=opt ++ fi ++fi ++ ++case $COQIDE in ++ byte|opt) ++ case $lablgtkdir_spec in ++ no) LABLGTKLIB=+lablgtk2 # Pour le message ++ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile ++ yes) LABLGTKLIB="$lablgtkdir" # Pour le message ++ LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile ++ esac;; ++ no) LABLGTKINCLUDES="";; ++esac ++ ++# strip command ++ ++case $ARCH in ++ win32) ++ # true -> strip : it exists under cygwin ! ++ STRIPCOMMAND="strip";; ++ *) ++ if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] || ++ [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ] ++ then ++ STRIPCOMMAND="true" ++ else ++ STRIPCOMMAND="strip" ++ fi ++esac ++ ++# mktexlsr ++#MKTEXLSR=`which mktexlsr` ++#case $MKTEXLSR in ++# "") MKTEXLSR=true;; ++#esac ++ ++# " ++### Test if documentation can be compiled (latex, hevea) ++ ++if test "$with_doc" = "all" ++then ++ for cmd in "latex" "hevea" ; do ++ if test ! -x "`which $cmd`" ++ then ++ echo "$cmd was not found; documentation will not be available" ++ with_doc=no ++ break ++ fi ++ done ++fi ++ ++########################################### ++# bindir, libdir, mandir, docdir, etc. ++ ++case $src_spec in ++ no) COQTOP=${COQSRC} ++esac ++ ++# OCaml only understand Windows filenames (C:\...) ++case $ARCH in ++ win32) COQTOP=`cygpath -m ${COQTOP}` ++esac ++ ++case $ARCH in ++ win32) ++ bindir_def='C:\coq\bin' ++ libdir_def='C:\coq\lib' ++ mandir_def='C:\coq\man' ++ docdir_def='C:\coq\doc' ++ emacslib_def='C:\coq\emacs' ++ coqdocdir_def='C:\coq\latex';; ++ *) ++ bindir_def=/usr/local/bin ++ libdir_def=/usr/local/lib/coq ++ mandir_def=/usr/local/man ++ docdir_def=/usr/local/share/doc/coq ++ emacslib_def=/usr/local/share/emacs/site-lisp ++ coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;; ++esac ++ ++emacs_def=emacs ++ ++case $bindir_spec/$prefix_spec/$local in ++ yes/*/*) BINDIR=$bindir ;; ++ */yes/*) BINDIR=$prefix/bin ;; ++ */*/true) BINDIR=$COQTOP/bin ;; ++ *) printf "Where should I install the Coq binaries [$bindir_def]? " ++ read BINDIR ++ case $BINDIR in ++ "") BINDIR=$bindir_def;; ++ *) true;; ++ esac;; ++esac ++ ++case $libdir_spec/$prefix_spec/$local in ++ yes/*/*) LIBDIR=$libdir;; ++ */yes/*) ++ case $ARCH in ++ win32) LIBDIR=$prefix ;; ++ *) LIBDIR=$prefix/lib/coq ;; ++ esac ;; ++ */*/true) LIBDIR=$COQTOP ;; ++ *) printf "Where should I install the Coq library [$libdir_def]? " ++ read LIBDIR ++ case $LIBDIR in ++ "") LIBDIR=$libdir_def;; ++ *) true;; ++ esac;; ++esac ++ ++case $mandir_spec/$prefix_spec/$local in ++ yes/*/*) MANDIR=$mandir;; ++ */yes/*) MANDIR=$prefix/man ;; ++ */*/true) MANDIR=$COQTOP/man ;; ++ *) printf "Where should I install the Coq man pages [$mandir_def]? " ++ read MANDIR ++ case $MANDIR in ++ "") MANDIR=$mandir_def;; ++ *) true;; ++ esac;; ++esac ++ ++case $docdir_spec/$prefix_spec/$local in ++ yes/*/*) DOCDIR=$docdir; HTMLREFMANDIR=$DOCDIR/html/refman;; ++ */yes/*) DOCDIR=$prefix/share/doc/coq; HTMLREFMANDIR=$DOCDIR/html/refman;; ++ */*/true) DOCDIR=$COQTOP/doc; HTMLREFMANDIR=$DOCDIR/refman/html;; ++ *) printf "Where should I install the Coq documentation [$docdir_def]? " ++ read DOCDIR ++ case $DOCDIR in ++ "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;; ++ *) true;; ++ esac;; ++esac ++ ++case $emacslib_spec/$prefix_spec/$local in ++ yes/*/*) EMACSLIB=$emacslib;; ++ */yes/*) ++ case $ARCH in ++ win32) EMACSLIB=$prefix/emacs ;; ++ *) EMACSLIB=$prefix/share/emacs/site-lisp ;; ++ esac ;; ++ */*/true) EMACSLIB=$COQTOP/tools/emacs ;; ++ *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? " ++ read EMACSLIB ++ case $EMACSLIB in ++ "") EMACSLIB=$emacslib_def;; ++ *) true;; ++ esac;; ++esac ++ ++case $coqdocdir_spec/$prefix_spec/$local in ++ yes/*/*) COQDOCDIR=$coqdocdir;; ++ */yes/*) ++ case $ARCH in ++ win32) COQDOCDIR=$prefix/latex ;; ++ *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; ++ esac ;; ++ */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; ++ *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? " ++ read COQDOCDIR ++ case $COQDOCDIR in ++ "") COQDOCDIR=$coqdocdir_def;; ++ *) true;; ++ esac;; ++esac ++ ++# Determine if we enable -custom by default (Windows and MacOS) ++CUSTOM_OS=no ++if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then ++ CUSTOM_OS=yes ++fi ++ ++BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!" ++case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in ++ yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";; ++ */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";; ++ */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";; ++ *) ++ COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'" ++ BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";; ++esac ++case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in ++ yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; ++ */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";; ++ *) COQTOOLSBYTEFLAGS="";; ++esac ++ ++# case $emacs_spec in ++# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? " ++# read EMACS ++ ++# case $EMACS in ++# "") EMACS=$emacs_def;; ++# *) true;; ++# esac;; ++# yes) EMACS=$emacs;; ++# esac ++ ++ ++ ++########################################### ++# Summary of the configuration ++ ++echo "" ++echo " Coq top directory : $COQTOP" ++echo " Architecture : $ARCH" ++if test ! -z "$OS" ; then ++ echo " Operating system : $OS" ++fi ++echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS" ++echo " Coq tools bytecode link flags : $COQTOOLSBYTEFLAGS" ++echo " OS dependent libraries : $OSDEPLIBS" ++echo " Objective-Caml/Camlp4 version : $CAMLVERSION" ++echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN" ++echo " Objective-Caml library in : $CAMLLIB" ++echo " Camlp4 library in : $CAMLP4LIB" ++if test "$best_compiler" = opt ; then ++echo " Native dynamic link support : $HASNATDYNLINK" ++fi ++if test "$COQIDE" != "no"; then ++echo " Lablgtk2 library in : $LABLGTKLIB" ++fi ++if test "$with_doc" = "all"; then ++echo " Documentation : All" ++else ++echo " Documentation : None" ++fi ++echo " CoqIde : $COQIDE" ++echo " Web browser : $BROWSER" ++echo " Coq web site : $WWWCOQ" ++echo "" ++ ++echo " Paths for true installation:" ++echo " binaries will be copied in $BINDIR" ++echo " library will be copied in $LIBDIR" ++echo " man pages will be copied in $MANDIR" ++echo " documentation will be copied in $DOCDIR" ++echo " emacs mode will be copied in $EMACSLIB" ++echo "" ++ ++################################################## ++# Building the $COQTOP/dev/ocamldebug-coq file ++################################################## ++ ++OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq ++ ++if test "$coq_debug_flag" = "-g" ; then ++ rm -f $OCAMLDEBUGCOQ ++ sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ ++ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ ++ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ ++ -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ ++ $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ ++ chmod a-w,a+x $OCAMLDEBUGCOQ ++fi ++ ++#################################################### ++# Fixing lablgtk types (before/after 2.6.0) ++#################################################### ++ ++if [ ! "$COQIDE" = "no" ]; then ++ if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then ++ if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then ++ cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli ++ else ++ cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli ++ fi ++ else ++ cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli ++ fi ++fi ++ ++############################################## ++# Creation of configuration files ++############################################## ++ ++mlconfig_file="$COQSRC/config/coq_config.ml" ++config_file="$COQSRC/config/Makefile" ++config_template="$COQSRC/config/Makefile.template" ++ ++ ++### Warning !! ++### After this line, be careful when using variables, ++### since some of them (e.g. $COQSRC) will be escaped ++ ++ ++# An escaped version of a variable ++escape_var () { ++"$ocamlexec" 2>&1 1>/dev/null < $mlconfig_file ++(* DO NOT EDIT THIS FILE: automatically generated by ../configure *) ++ ++let local = $local ++let coqrunbyteflags = "$COQRUNBYTEFLAGS" ++let coqlib = "$LIBDIR" ++let coqsrc = "$COQSRC" ++let ocaml = "$ocamlexec" ++let ocamlc = "$bytecamlc" ++let ocamlopt = "$nativecamlc" ++let ocamlmklib = "$ocamlmklibexec" ++let ocamldep = "$ocamldepexec" ++let ocamldoc = "$ocamldocexec" ++let ocamlyacc = "$ocamlyaccexec" ++let ocamllex = "$ocamllexexec" ++let camlbin = "$CAMLBIN" ++let camllib = "$CAMLLIB" ++let camlp4 = "$CAMLP4" ++let camlp4o = "$camlp4oexec" ++let camlp4bin = "$CAMLP4BIN" ++let camlp4lib = "$CAMLP4LIB" ++let camlp4compat = "$CAMLP4COMPAT" ++let coqideincl = "$LABLGTKINCLUDES" ++let cflags = "$cflags" ++let best = "$best_compiler" ++let arch = "$ARCH" ++let has_coqide = "$COQIDE" ++let has_natdynlink = $HASNATDYNLINK ++let natdynlinkflag = "$NATDYNLINKFLAG" ++let osdeplibs = "$OSDEPLIBS" ++let version = "$VERSION" ++let caml_version = "$CAMLVERSION" ++let date = "$DATE" ++let compile_date = "$COMPILEDATE" ++let vo_magic_number = $VOMAGIC ++let state_magic_number = $STATEMAGIC ++let exec_extension = "$EXE" ++let with_geoproof = ref $with_geoproof ++let browser = "$BROWSER" ++let wwwcoq = "$WWWCOQ" ++let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" ++let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/" ++let localwwwrefman = "file://$HTMLREFMANDIR/" ++ ++END_OF_COQ_CONFIG ++ ++# to be sure printf is found on windows when spaces occur in PATH variable ++PRINTF=`which printf` ++ ++# Subdirectories of theories/ added in coq_config.ml ++subdirs () { ++ (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file") ++} ++ ++echo "let theories_dirs = [" >> "$mlconfig_file" ++subdirs theories ++echo "]" >> "$mlconfig_file" ++ ++echo "let plugins_dirs = [" >> "$mlconfig_file" ++subdirs plugins ++echo "]" >> "$mlconfig_file" ++ ++chmod a-w "$mlconfig_file" ++ ++ ++############################################### ++# Building the $COQTOP/config/Makefile file ++############################################### ++ ++rm -f "$config_file" ++ ++sed -e "s|LOCALINSTALLATION|$local|" \ ++ -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \ ++ -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \ ++ -e "s|COQSRCDIRECTORY|$COQSRC|" \ ++ -e "s|COQVERSION|$VERSION|" \ ++ -e "s|BINDIRDIRECTORY|$BINDIR|" \ ++ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ ++ -e "s|BUILDLDPATH=|$BUILDLDPATH|" \ ++ -e "s|MANDIRDIRECTORY|$MANDIR|" \ ++ -e "s|DOCDIRDIRECTORY|$DOCDIR|" \ ++ -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ ++ -e "s|EMACSCOMMAND|$EMACS|" \ ++ -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \ ++ -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \ ++ -e "s|ARCHITECTURE|$ARCH|" \ ++ -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \ ++ -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ ++ -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \ ++ -e "s|CAMLTAG|$CAMLTAG|" \ ++ -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ ++ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ ++ -e "s|CAMLP4TOOL|$camlp4oexec|" \ ++ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ ++ -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \ ++ -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \ ++ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ ++ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ ++ -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \ ++ -e "s|CCOMPILEFLAGS|$cflags|" \ ++ -e "s|BESTCOMPILER|$best_compiler|" \ ++ -e "s|DLLEXTENSION|$DLLEXT|" \ ++ -e "s|EXECUTEEXTENSION|$EXE|" \ ++ -e "s|BYTECAMLC|$bytecamlc|" \ ++ -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \ ++ -e "s|NATIVECAMLC|$nativecamlc|" \ ++ -e "s|OCAMLEXEC|$ocamlexec|" \ ++ -e "s|OCAMLDEPEXEC|$ocamldepexec|" \ ++ -e "s|OCAMLDOCEXEC|$ocamldocexec|" \ ++ -e "s|OCAMLLEXEXEC|$ocamllexexec|" \ ++ -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \ ++ -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \ ++ -e "s|CCEXEC|$gcc_exec|" \ ++ -e "s|AREXEC|$ar_exec|" \ ++ -e "s|RANLIBEXEC|$ranlib_exec|" \ ++ -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ ++ -e "s|COQIDEOPT|$COQIDE|" \ ++ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ ++ -e "s|WITHDOCOPT|$with_doc|" \ ++ -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \ ++ "$config_template" > "$config_file" ++ ++chmod a-w "$config_file" ++ ++################################################## ++# The end ++#################################################### ++ ++echo "If anything in the above is wrong, please restart './configure'." ++echo ++echo "*Warning* To compile the system for a new architecture" ++echo " don't forget to do a 'make archclean' before './configure'." ++ ++# $Id: configure 14833 2011-12-19 21:57:30Z notin $ diff --git a/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch b/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch deleted file mode 100644 index 5176aa33ec8..00000000000 --- a/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch +++ /dev/null @@ -1,84 +0,0 @@ -From: glondu -Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000) -Subject: Fix mixed implicit and normal rules -X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85 - -Fix mixed implicit and normal rules - -This fixes build with GNU Make 3.82. See threads: - - https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html - http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912 - -git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7 ---- - -diff --git a/Makefile b/Makefile -index b1edc01..ea73c51 100644 ---- a/Makefile -+++ b/Makefile -@@ -160,9 +160,19 @@ else - stage1 $(STAGE1_TARGETS) : always - $(call stage-template,1) - -+ifneq (,$(STAGE1_IMPLICITS)) -+$(STAGE1_IMPLICITS) : always -+ $(call stage-template,1) -+endif -+ - stage2 $(STAGE2_TARGETS) : stage1 - $(call stage-template,2) - -+ifneq (,$(STAGE2_IMPLICITS)) -+$(STAGE2_IMPLICITS) : stage1 -+ $(call stage-template,2) -+endif -+ - # Nota: - # - world is one of the targets in $(STAGE2_TARGETS), hence launching - # "make" or "make world" leads to recursion into stage1 then stage2 -diff --git a/Makefile.common b/Makefile.common -index cc38980..46bf217 100644 ---- a/Makefile.common -+++ b/Makefile.common -@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y") - - SOURCEDOCDIR=dev/source-doc - --CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot -+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot - - ### Targets forwarded by Makefile to a specific stage: - -@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot - STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ - $(GENFILES) \ - source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ -- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o -+ $(STAGE1_ML4:.ml4=.ml4-preprocessed) -+ -+STAGE1_IMPLICITS:= - - ifdef CM_STAGE1 -- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - ## Enumeration of targets that require being done at stage2 -@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ - printers debug initplugins plugins \ - world install coqide coqide-files coq coqlib \ - coqlight states check init theories theories-light \ -- $(DOC_TARGETS) $(VO_TARGETS) validate \ -- %.vo %.glob states/% install-% %.ml4-preprocessed \ -+ $(DOC_TARGETS) $(VO_TARGETS) validate -+ -+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ - $(DOC_TARGET_PATTERNS) - - ifndef CM_STAGE1 -- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index ce285418ad8..3fef10b44fb 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -29,8 +29,7 @@ stdenv.mkDerivation { buildFlags = "world"; # Debug with "world VERBOSE=1"; - #patches = [ ./configure.patch ./coq-8.3-make-3.82-compat.patch ]; - patches = [ /root/configure.patch ]; + patches = [ ./configure.patch ]; postPatch = '' UNAME=$(type -tp uname)