diff options
| -rw-r--r-- | pkgs/applications/science/logic/coq/8.3.nix | 82 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/coq/configure.8.3.patch | 1112 | ||||
| -rw-r--r-- | pkgs/applications/science/logic/coq/no-codesign.patch | 19 | ||||
| -rw-r--r-- | pkgs/top-level/aliases.nix | 3 | ||||
| -rw-r--r-- | pkgs/top-level/all-packages.nix | 17 | ||||
| -rw-r--r-- | pkgs/top-level/coq-packages.nix | 7 | ||||
| -rw-r--r-- | pkgs/top-level/ocaml-packages.nix | 2 |
7 files changed, 14 insertions, 1228 deletions
diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix deleted file mode 100644 index 341267b2cebe..000000000000 --- a/pkgs/applications/science/logic/coq/8.3.nix +++ /dev/null @@ -1,82 +0,0 @@ -# - coqide compilation can be disabled by setting lablgtk to null; -# - The csdp program used for the Micromega tactic is statically referenced. -# However, coq can build without csdp by setting it to null. -# In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found. - -{ stdenv, lib, make, fetchurl -, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null }: - -assert lib.versionOlder ocaml.version "4"; - -let - version = "8.3pl4"; - buildIde = lablgtk != null; - ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; - idePatch = if buildIde then '' - substituteInPlace scripts/coqmktop.ml --replace \ - "\"-I\"; \"+lablgtk2\"" \ - "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\"" - '' else ""; - csdpPatch = if csdp != null then '' - substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" - substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.search_exe_in_path \"csdp\"" "Some \"${csdp}/bin/csdp\"" - '' else ""; -in - -stdenv.mkDerivation { - name = "coq-${version}"; - - src = fetchurl { - url = "https://coq.inria.fr/V${version}/files/coq-${version}.tar.gz"; - sha256 = "17d3lmchmqir1rawnr52g78srg4wkd7clzpzfsivxc4y1zp6rwkr"; - }; - - buildInputs = [ make ocaml findlib camlp5 ncurses lablgtk ]; - - prefixKey = "-prefix "; - - preConfigure = '' - configureFlagsArray=( - -opt - -camldir ${ocaml}/bin - -camlp5dir $(ocamlfind query camlp5) - ${ideFlags} - ) - ''; - - buildFlags = "world"; # Debug with "world VERBOSE=1"; - - patches = [ ./configure.8.3.patch ]; - - postPatch = '' - UNAME=$(type -tp uname) - RM=$(type -tp rm) - substituteInPlace configure --replace "/bin/uname" "$UNAME" - substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" - ${idePatch} - ${csdpPatch} - ''; - - # This post install step is needed to build ssrcoqide from the ssreflect package - # It could be made optional, but I see little harm in including it in the default - # distribution -- roconnor - # This will likely no longer be necessary for coq >= 8.4. -- roconnor - postInstall = if buildIde then '' - cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/ - '' else ""; - - meta = with stdenv.lib; { - description = "Coq proof assistant"; - longDescription = '' - Coq is a formal proof management system. It provides a formal language - to write mathematical definitions, executable algorithms and theorems - together with an environment for semi-interactive development of - machine-checked proofs. - ''; - homepage = http://coq.inria.fr; - license = licenses.lgpl21; - branch = "8.3"; - maintainers = with maintainers; [ roconnor vbgl ]; - platforms = with platforms; linux; - }; -} diff --git a/pkgs/applications/science/logic/coq/configure.8.3.patch b/pkgs/applications/science/logic/coq/configure.8.3.patch deleted file mode 100644 index 431cccac4b0b..000000000000 --- a/pkgs/applications/science/logic/coq/configure.8.3.patch +++ /dev/null @@ -1,1112 +0,0 @@ -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 -- camlp4oexec=$CAMLBIN/camlp4o - esac - - if test ! -f "$CAMLC" ; then -@@ -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 - 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 <dir>" -+ printf "\tSet installation directory to <dir>\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 <command>" -+ printf "\tUse <command> 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 <file>" -+ echo "-with-ar <file>" -+ echo "-with-ranlib <file>" -+ 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 <<EOF -+ prerr_endline(String.escaped(Sys.getenv"$VAR"));; -+EOF -+} -+ -+# Escaped version of browser command -+export BROWSER -+BROWSER=`VAR=BROWSER escape_var` -+ -+# damned backslashes under M$Windows -+case $ARCH in -+ win32) -+ COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` -+ BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` -+ COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'` -+ LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` -+ CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` -+ CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` -+ MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` -+ DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'` -+ EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` -+ COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` -+ CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` -+ CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'` -+ LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'` -+ COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` -+ COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` -+ BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'` -+ ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'` -+ bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'` -+ nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'` -+ ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'` -+ ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'` -+ ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'` -+ ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'` -+ ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'` -+ camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'` -+ ;; -+esac -+ -+##################################################### -+# Building the $COQTOP/config/coq_config.ml file -+##################################################### -+ -+rm -f "$mlconfig_file" -+cat << END_OF_COQ_CONFIG > $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/no-codesign.patch b/pkgs/applications/science/logic/coq/no-codesign.patch deleted file mode 100644 index 0f917fbf56d4..000000000000 --- a/pkgs/applications/science/logic/coq/no-codesign.patch +++ /dev/null @@ -1,19 +0,0 @@ -diff --git a/Makefile.build b/Makefile.build -index 2963a3d..876479c 100644 ---- a/Makefile.build -+++ b/Makefile.build -@@ -101,13 +101,8 @@ BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) - OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) - DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils - --ifeq ($(ARCH),Darwin) --LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" --CODESIGN=codesign -s - --else - LINKMETADATA= - CODESIGN=true --endif - - define bestocaml - $(if $(OPT),\ - diff --git a/pkgs/top-level/aliases.nix b/pkgs/top-level/aliases.nix index f06044829b4d..1617f9330b49 100644 --- a/pkgs/top-level/aliases.nix +++ b/pkgs/top-level/aliases.nix @@ -329,7 +329,7 @@ mapAliases ({ callPackage_i686 = pkgsi686Linux.callPackage; inherit (ocaml-ng) # added 2016-09-14 - ocamlPackages_3_11_2 ocamlPackages_3_12_1 + ocamlPackages_3_12_1 ocamlPackages_4_00_1 ocamlPackages_4_01_0 ocamlPackages_4_02 ocamlPackages_4_03 ocamlPackages_latest; @@ -348,7 +348,6 @@ mapAliases ({ gst-ffmpeg = pkgs.gst-ffmpeg; }; } // (with ocaml-ng; { # added 2016-09-14 - ocaml_3_11_2 = ocamlPackages_3_11_2.ocaml; ocaml_3_12_1 = ocamlPackages_3_12_1.ocaml; ocaml_4_00_1 = ocamlPackages_4_00_1.ocaml; ocaml_4_01_0 = ocamlPackages_4_01_0.ocaml; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 2ed05e4972f1..632b88c8012c 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -21148,12 +21148,11 @@ with pkgs; boogie = dotnetPackages.Boogie; inherit (callPackage ./coq-packages.nix { - inherit (ocaml-ng) ocamlPackages_3_12_1 - ocamlPackages_4_02 + inherit (ocaml-ng) ocamlPackages_4_02 ocamlPackages_4_05 ; }) mkCoqPackages - coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8 + coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8 coqPackages_8_5 coqPackages_8_6 coqPackages_8_7 coqPackages_8_8 coqPackages coq ; @@ -21232,7 +21231,17 @@ with pkgs; ltl2ba = callPackage ../applications/science/logic/ltl2ba {}; - inherit (ocaml-ng.ocamlPackages_3_11_2) matita; + #inherit (ocaml-ng.ocamlPackages_3_11_2) matita; + + # Current version is 0.5.8. Official website says: + + # Version 0.5.9, released on December 23, 2014, is an update of version 0.5.8 + # to compile with the latter OCaml version and libraries. + # It is unsupported, but still used for teaching at the University of Bologna. + + # It should allow us removing the dependency on OCaml 3.11 but I haven't been + # able to confirm because Matita depends on lablgtkmathview-0.7.2 which + # already reports as broken. matita_130312 = lowPrio ocamlPackages.matita_130312; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index bc21137903af..305d9ba351ba 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -1,6 +1,5 @@ { lib, callPackage, newScope, recurseIntoAttrs , gnumake3 -, ocamlPackages_3_12_1 , ocamlPackages_4_02 , ocamlPackages_4_05 }: @@ -56,12 +55,6 @@ in rec { let self = mkCoqPackages' self coq; in filterCoqPackages coq self; - coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { - make = gnumake3; - inherit (ocamlPackages_3_12_1) ocaml findlib; - camlp5 = ocamlPackages_3_12_1.camlp5_transitional; - lablgtk = ocamlPackages_3_12_1.lablgtk_2_14; - }; coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix { inherit (ocamlPackages_4_02) ocaml findlib lablgtk; camlp5 = ocamlPackages_4_02.camlp5_transitional; diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index 026bab235065..ee0f554efa3f 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -1065,8 +1065,6 @@ in rec inherit mkOcamlPackages; - ocamlPackages_3_11_2 = mkOcamlPackages (callPackage ../development/compilers/ocaml/3.11.2.nix { }) (self: super: { lablgtk = self.lablgtk_2_14; }); - ocamlPackages_3_12_1 = mkOcamlPackages (callPackage ../development/compilers/ocaml/3.12.1.nix { }) (self: super: { camlimages = self.camlimages_4_0; }); ocamlPackages_4_00_1 = mkOcamlPackages (callPackage ../development/compilers/ocaml/4.00.1.nix { }) (self: super: { }); |