diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 478 |
1 files changed, 272 insertions, 206 deletions
@@ -6,7 +6,7 @@ # ################################## -VERSION=8.4beta2 +VERSION=8.4 VOMAGIC=08400 STATEMAGIC=58400 DATE=`LC_ALL=C LANG=C date +"%B %Y"` @@ -81,10 +81,6 @@ usage () { 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" @@ -119,10 +115,6 @@ 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 @@ -254,18 +246,6 @@ while : ; do 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;; -makecmd|--makecmd) makecmd="$2" shift;; -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; @@ -292,17 +272,19 @@ case $DATEPGM in "") echo "I can't find the program \"date\" in your path." echo "Please give me the current date" read COMPILEDATE;; - *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;; + *) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;; esac # Architecture case $arch_spec in no) - # First we test if we are running a Cygwin system + # First we test if we are running a Cygwin or Mingw/Msys system if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then ARCH="win32" CYGWIN=yes + elif [ `uname -s | cut -c -7` = "MINGW32" ]; then + ARCH="win32" else # If not, we determine the architecture if test -x /bin/uname ; then @@ -437,12 +419,26 @@ if test ! -f "$CAMLC" ; then exit 1 fi -# Under Windows, OCaml only understands Windows filenames (C:\...) -case $ARCH in - win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;; +# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml) +# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept + +mk_win_path () { + case $ARCH,$CYGWIN in + win32,yes) cygpath -m "$1" ;; + win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;; + *) echo "$1" ;; + esac +} + +case $ARCH,$src_spec in + win32,yes) echo "Error: the -src option is currently not supported on Windows" + exit 1;; + win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;; esac -CAMLVERSION=`"$bytecamlc" -version` +# Beware of the final \r in Win32 +CAMLVERSION=`"$CAMLC" -version | tr -d "\r"` +CAMLLIB=`"$CAMLC" -where | tr -d "\r"` case $CAMLVERSION in 1.*|2.*|3.0*|3.10*|3.11.[01]) @@ -454,7 +450,7 @@ case $CAMLVERSION in echo " Configuration script failed!" exit 1 fi;; - 3.11.2|3.12*) + 3.11.2|3.12*|4.*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) @@ -468,16 +464,9 @@ 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*) + OCAML31*|OCAML4*) # Compilation debug flag coq_debug_flag_opt="-g" ;; @@ -485,7 +474,7 @@ if [ "$coq_debug_flag" = "-g" ]; then fi # Native dynlink -if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then +if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then HASNATDYNLINK=true else HASNATDYNLINK=false @@ -520,7 +509,8 @@ esac # (this should become configurable some day) CAMLP4BIN=${CAMLBIN} -if [ "$usecamlp5" = "yes" ]; then +case $usecamlp5 in + yes) CAMLP4=camlp5 CAMLP4MOD=gramlib if [ "$camlp5dir" != "" ]; then @@ -539,38 +529,47 @@ if [ "$usecamlp5" = "yes" ]; then CAMLP4LIB=+site-lib/camlp5 FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5 else - echo "Objective Caml $CAMLVERSION found but no Camlp5 installed." - echo "Configuration script failed!" - exit 1 + echo "No Camlp5 installation found. Looking for Camlp4 instead..." + usecamlp5=no fi +esac - camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - case `$camlp4oexec -v 2>&1` in - *4.0*|*5.00*) +# If we're (still...) going to use Camlp5, let's check its version + +case $usecamlp5 in + yes) + camlp4oexec=`echo "$camlp4oexec" | tr 4 5` + case `"$camlp4oexec" -v 2>&1` in + *"version 4.0"*|*5.00*) echo "Camlp5 version < 5.01 not supported." echo "Configuration script failed!" exit 1;; esac +esac + +# We might now try to use Camlp4, either by explicit choice or +# by lack of proper Camlp5 installation -else # let's use camlp4 +case $usecamlp5 in + no) CAMLP4=camlp4 CAMLP4MOD=camlp4lib CAMLP4LIB=+camlp4 FULLCAMLP4LIB=${CAMLLIB}/camlp4 if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then - echo "Objective Caml $CAMLVERSION found but no Camlp4 installed." + echo "No Camlp4 installation found." echo "Configuration script failed!" exit 1 fi camlp4oexec=${camlp4oexec}rf - if [ "`$camlp4oexec 2>&1`" != "" ]; then + if [ "`"$camlp4oexec" 2>&1`" != "" ]; then echo "Error: $camlp4oexec not found or not executable." echo "Configuration script failed!" exit 1 fi -fi +esac # do we have a native compiler: test of ocamlopt and its version @@ -595,18 +594,17 @@ fi # OS dependent libraries -case $ARCH in +OSDEPLIBS="-cclib -lunix" +case $ARCH,$CYGWIN in sun4*) OS=`uname -r` case $OS in 5*) OS="Sun Solaris $OS" - OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";; + OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";; *) OS="Sun OS $OS" - OSDEPLIBS="-cclib -lunix" esac;; - win32) OS="Win32" - OSDEPLIBS="-cclib -lunix" + win32,yes) OS="Win32 (Cygwin)" cflags="-mno-cygwin $cflags";; - *) OSDEPLIBS="-cclib -lunix" + win32,*) OS="Win32 (MinGW)";; esac # lablgtk2 and CoqIDE @@ -628,11 +626,11 @@ 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 + no) + if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then + lablgtkdir_spec=yes + elif [ -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 @@ -656,10 +654,10 @@ else else echo "LablGtk2 found, native threads: native CoqIde will be available." COQIDE=opt - if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration; + if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration; then - cflags=$cflags" `pkg-config --cflags ige-mac-integration`" - IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"' + cflags=$cflags" `pkg-config --cflags gtk-mac-integration`" + IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"' IDEARCHFILE=ide/ide_mac_stubs.o IDEARCHDEF=QUARTZ elif [ "$ARCH" = "win32" ]; @@ -685,9 +683,6 @@ esac # strip command case $ARCH in - win32) - # true -> strip : it exists under cygwin ! - STRIPCOMMAND="strip";; Darwin) if [ "$HASNATDYNLINK" = "true" ] then STRIPCOMMAND="true" @@ -703,13 +698,6 @@ case $ARCH in 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" @@ -727,26 +715,28 @@ 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}` + win32) COQSRC=`mk_win_path "$COQSRC"` + CAMLBIN=`mk_win_path "$CAMLBIN"` + CAMLP4BIN=`mk_win_path "$CAMLP4BIN"` +esac + +case $src_spec in + no) COQTOP=${COQSRC} esac case $ARCH$CYGWIN in win32) - W32PREF='C:\\coq\\' - bindir_def=${W32PREF}bin - libdir_def=${W32PREF}lib - configdir_def=${W32PREF}config - datadir_def=${W32PREF}share - mandir_def=${W32PREF}man - docdir_def=${W32PREF}doc - emacslib_def=${W32PREF}emacs - coqdocdir_def=${W32PREF}latex;; + W32PREF='C:\coq\' + bindir_def="${W32PREF}bin" + libdir_def="${W32PREF}lib" + configdir_def="${W32PREF}config" + datadir_def="${W32PREF}share" + mandir_def="${W32PREF}man" + docdir_def="${W32PREF}doc" + emacslib_def="${W32PREF}emacs" + coqdocdir_def="${W32PREF}latex";; *) bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq @@ -755,7 +745,7 @@ case $ARCH$CYGWIN in mandir_def=/usr/local/share/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;; + coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;; esac emacs_def=emacs @@ -764,7 +754,7 @@ 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]? " + *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def" read BINDIR case $BINDIR in "") BINDIR=$bindir_def;; @@ -781,7 +771,7 @@ case $libdir_spec/$prefix_spec/$local in *) LIBDIR=$prefix/lib/coq ;; esac ;; */*/true) LIBDIR=$COQTOP ;; - *) printf "Where should I install the Coq library [$libdir_def]? " + *) printf "Where should I install the Coq library [%s]? " "$libdir_def" read LIBDIR libdir_spec=yes case $LIBDIR in @@ -790,11 +780,6 @@ case $libdir_spec/$prefix_spec/$local in esac;; esac -case $libdir_spec in - yes) LIBDIR_OPTION="Some \"$LIBDIR\"";; - *) LIBDIR_OPTION="None";; -esac - case $configdir_spec/$prefix_spec/$local in yes/*/*) CONFIGDIR=$configdir;; */yes/*) configdir_spec=yes @@ -804,7 +789,7 @@ case $configdir_spec/$prefix_spec/$local in esac;; */*/true) CONFIGDIR=$COQTOP/ide configdir_spec=yes;; - *) printf "Where should I install the Coqide configuration files [$configdir_def]? " + *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def" read CONFIGDIR case $CONFIGDIR in "") CONFIGDIR=$configdir_def;; @@ -812,17 +797,12 @@ case $configdir_spec/$prefix_spec/$local in esac;; esac -case $configdir_spec in - yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";; - *) CONFIGDIR_OPTION="None";; -esac - case $datadir_spec/$prefix_spec/$local in yes/*/*) DATADIR=$datadir;; */yes/*) DATADIR=$prefix/share/coq;; */*/true) DATADIR=$COQTOP/ide datadir_spec=yes;; - *) printf "Where should I install the Coqide data files [$datadir_def]? " + *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def" read DATADIR case $DATADIR in "") DATADIR=$datadir_def;; @@ -830,17 +810,11 @@ case $datadir_spec/$prefix_spec/$local in esac;; esac -case $datadir_spec in - yes) DATADIR_OPTION="Some \"$DATADIR\"";; - *) DATADIR_OPTION="None";; -esac - - case $mandir_spec/$prefix_spec/$local in yes/*/*) MANDIR=$mandir;; */yes/*) MANDIR=$prefix/share/man ;; */*/true) MANDIR=$COQTOP/man ;; - *) printf "Where should I install the Coq man pages [$mandir_def]? " + *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def" read MANDIR case $MANDIR in "") MANDIR=$mandir_def;; @@ -852,7 +826,7 @@ case $docdir_spec/$prefix_spec/$local in yes/*/*) DOCDIR=$docdir;; */yes/*) DOCDIR=$prefix/share/doc/coq;; */*/true) DOCDIR=$COQTOP/doc;; - *) printf "Where should I install the Coq documentation [$docdir_def]? " + *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def" read DOCDIR case $DOCDIR in "") DOCDIR=$docdir_def;; @@ -868,7 +842,7 @@ case $emacslib_spec/$prefix_spec/$local in *) EMACSLIB=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) EMACSLIB=$COQTOP/tools/emacs ;; - *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? " + *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def" read EMACSLIB case $EMACSLIB in "") EMACSLIB=$emacslib_def;; @@ -884,7 +858,7 @@ case $coqdocdir_spec/$prefix_spec/$local in *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; - *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? " + *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def" read COQDOCDIR case $COQDOCDIR in "") COQDOCDIR=$coqdocdir_def;; @@ -914,14 +888,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in esac # case $emacs_spec in -# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? " +# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def" # read EMACS # case $EMACS in -# "") EMACS=$emacs_def;; +# "") EMACS="$emacs_def";; # *) true;; # esac;; -# yes) EMACS=$emacs;; +# yes) EMACS="$emacs";; # esac @@ -1016,51 +990,63 @@ config_template="$COQSRC/config/Makefile.template" ### 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 +escape_string () { + "$ocamlexec" "tools/escape_string.ml" "$1" } # Escaped version of browser command -export BROWSER -BROWSER=`VAR=BROWSER escape_var` +BROWSER=`escape_string "$BROWSER"` + +# Under Windows, we now escape the backslashes that will ends in +# ocaml strings (coq_config.ml) or in Makefile variables. -# 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'` - CONFIGDIR=`echo $CONFIGDIR |sed -e 's|\\\|\\\\\\\|g'` - DATADIR=`echo $DATADIR |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'` + COQTOP=`escape_string "$COQTOP"` + BINDIR=`escape_string "$BINDIR"` + COQSRC=`escape_string "$COQSRC"` + LIBDIR=`escape_string "$LIBDIR"` + CONFIGDIR=`escape_string "$CONFIGDIR"` + DATADIR=`escape_string "$DATADIR"` + CAMLBIN=`escape_string "$CAMLBIN"` + CAMLLIB=`escape_string "$CAMLLIB"` + MANDIR=`escape_string "$MANDIR"` + DOCDIR=`escape_string "$DOCDIR"` + EMACSLIB=`escape_string "$EMACSLIB"` + COQDOCDIR=`escape_string "$COQDOCDIR"` + CAMLP4BIN=`escape_string "$CAMLP4BIN"` + CAMLP4LIB=`escape_string "$CAMLP4LIB"` + LABLGTKINCLUDES=`escape_string "$LABLGTKINCLUDES"` + COQRUNBYTEFLAGS=`escape_string "$COQRUNBYTEFLAGS"` + COQTOOLSBYTEFLAGS=`escape_string "$COQTOOLSBYTEFLAGS"` + BUILDLDPATH=`escape_string "$BUILDLDPATH"` + ocamlexec=`escape_string "$ocamlexec"` + bytecamlc=`escape_string "$bytecamlc"` + nativecamlc=`escape_string "$nativecamlc"` + ocamlmklibexec=`escape_string "$ocamlmklibexec"` + ocamldepexec=`escape_string "$ocamldepexec"` + ocamldocexec=`escape_string "$ocamldocexec"` + ocamllexexec=`escape_string "$ocamllexexec"` + ocamlyaccexec=`escape_string "$ocamlyaccexec"` + camlp4oexec=`escape_string "$camlp4oexec"` ;; esac +case $libdir_spec in + yes) LIBDIR_OPTION="Some \"$LIBDIR\"";; + *) LIBDIR_OPTION="None";; +esac + +case $configdir_spec in + yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";; + *) CONFIGDIR_OPTION="None";; +esac + +case $datadir_spec in + yes) DATADIR_OPTION="Some \"$DATADIR\"";; + *) DATADIR_OPTION="None";; +esac + ##################################################### # Building the $COQTOP/config/coq_config.ml file ##################################################### @@ -1139,63 +1125,143 @@ chmod a-w "$mlconfig_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|CONFIGDIRDIRECTORY|$CONFIGDIR|" \ - -e "s|DATADIRDIRECTORY|$DATADIR|" \ - -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|CAMLP4VARIANT|$CAMLP4|" \ - -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|IDEARCHFLAGS|$IDEARCHFLAGS|" \ - -e "s|IDEARCHFILE|$IDEARCHFILE|" \ - -e "s|IDEARCHDEF|$IDEARCHDEF|" \ - -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ - -e "s|WITHDOCOPT|$with_doc|" \ - -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \ - "$config_template" > "$config_file" +cat << END_OF_MAKEFILE > $config_file +###### config/Makefile : Configuration file for Coq ############## +# # +# This file is generated by the script "configure" # +# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! # +# If something is wrong below, then rerun the script "configure" # +# with the good options (see the file INSTALL). # +# # +################################################################## + +#Variable used to detect whether ./configure has run successfully. +COQ_CONFIGURED=yes + +# Local use (no installation) +LOCAL=$local + +# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun") +COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS +COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS +$BUILDLDPATH + +# Paths for true installation +# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and +# do_Makefile will reside +# LIBDIR=path where the Coq library will reside +# MANDIR=path where to install manual pages +# EMACSDIR=path where to put Coq's Emacs mode (coq.el) +BINDIR="$BINDIR" +COQLIBINSTALL="$LIBDIR" +CONFIGDIR="$CONFIGDIR" +DATADIR="$DATADIR" +MANDIR="$MANDIR" +DOCDIR="$DOCDIR" +EMACSLIB="$EMACSLIB" +EMACS=$EMACS + +# Path to Coq distribution +COQSRC="$COQSRC" +VERSION=$VERSION + +# Ocaml version number +CAMLVERSION=$CAMLTAG + +# Ocaml libraries +CAMLLIB="$CAMLLIB" + +# Ocaml .h directory +CAMLHLIB="$CAMLLIB" + +# Camlp4 : flavor, binaries, libraries ... +# NB : CAMLP4BIN can be empty if camlp4 is in the PATH +# NB : avoid using CAMLP4LIB (conflict under Windows) +CAMLP4BIN="$CAMLP4BIN" +CAMLP4=$CAMLP4 +CAMLP4O=$camlp4oexec +CAMLP4COMPAT=$CAMLP4COMPAT +MYCAMLP4LIB="$CAMLP4LIB" + +# LablGTK +COQIDEINCLUDES=$LABLGTKINCLUDES + +# Objective-Caml compile command +OCAML="$ocamlexec" +OCAMLC="$bytecamlc" +OCAMLMKLIB="$ocamlmklibexec" +OCAMLOPT="$nativecamlc" +OCAMLDEP="$ocamldepexec" +OCAMLDOC="$ocamldocexec" +OCAMLLEX="$ocamllexexec" +OCAMLYACC="$ocamlyaccexec" + +# Caml link command and Caml make top command +CAMLLINK="$bytecamlc" +CAMLOPTLINK="$nativecamlc" +CAMLMKTOP="$ocamlmktopexec" + +# Caml flags +CAMLFLAGS=-rectypes $coq_annotate_flag + +# Compilation debug flags +CAMLDEBUG=$coq_debug_flag +CAMLDEBUGOPT=$coq_debug_flag_opt + +# User compilation flag +USERFLAGS= + +# Flags for GCC +CFLAGS=$cflags + +# Compilation profile flag +CAMLTIMEPROF=$coq_profile_flag + +# The best compiler: native (=opt) or bytecode (=byte) if no native compiler +BEST=$best_compiler + +# Your architecture +# Can be obtain by UNIX command arch +ARCH=$ARCH +HASNATDYNLINK=$NATDYNLINKFLAG + +# Supplementary libs for some systems, currently: +# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket +# . others : -cclib -lunix +OSDEPLIBS=$OSDEPLIBS + +# executable files extension, currently: +# Unix systems: +# Win32 systems : .exe +EXE=$EXE +DLLEXT=$DLLEXT + +# the command MKDIR (try to replace it with mkdirhier if you have problems) +MKDIR=mkdir -p + +# where to put the coqdoc.sty style file +COQDOCDIR="$COQDOCDIR" + +#the command STRIP +# Unix systems and profiling: true +# Unix systems and no profiling: strip +STRIP=$STRIPCOMMAND + +# CoqIde (no/byte/opt) +HASCOQIDE=$COQIDE +IDEOPTFLAGS=$IDEARCHFLAGS +IDEOPTDEPS=$IDEARCHFILE +IDEOPTINT=$IDEARCHDEF + +# Defining REVISION +CHECKEDOUT=$checkedout + +# Option to control compilation and installation of the documentation +WITHDOC=$with_doc + +# make or sed are bogus and believe lines not terminating by a return +# are inexistent +END_OF_MAKEFILE chmod a-w "$config_file" |