summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure744
1 files changed, 470 insertions, 274 deletions
diff --git a/configure b/configure
index 16b2a82a..f7bdf154 100755
--- a/configure
+++ b/configure
@@ -6,10 +6,10 @@
#
##################################
-VERSION=8.3pl4
-VOMAGIC=08300
-STATEMAGIC=58300
-DATE=`LANG=C date +"%B %Y"`
+VERSION=8.4pl2
+VOMAGIC=08400
+STATEMAGIC=58400
+DATE=`LC_ALL=C LANG=C date +"%B %Y"`
# Create the bin/ directory if non-existent
test -d bin || mkdir bin
@@ -35,31 +35,36 @@ usage () {
printf "\tSet installation directory to <dir>\n"
echo "-local"
printf "\tSet installation directory to the current source tree\n"
- echo "-coqrunbyteflags"
+ echo "-coqrunbyteflags <flags>"
printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
- echo "-coqtoolsbyteflags"
+ echo "-coqtoolsbyteflags <flags>"
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"
+ echo "-src <dir>"
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"
+ echo "-bindir <dir>"
+ echo "-libdir <dir>"
+ echo "-configdir <dir>"
+ echo "-datadir <dir>"
+ echo "-mandir <dir>"
+ echo "-docdir <dir>"
+ printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
+ echo "-emacslib <dir>"
printf "\tSpecifies where emacs files are to be installed\n"
- echo "-coqdocdir"
+ echo "-coqdocdir <dir>"
printf "\tSpecifies where Coqdoc style files are to be installed\n"
- echo "-camldir"
+ echo "-camldir <dir>"
printf "\tSpecifies the path to the OCaml library\n"
- echo "-lablgtkdir"
+ echo "-lablgtkdir <dir>"
printf "\tSpecifies the path to the Lablgtk library\n"
- echo "-camlp5dir"
+ echo "-usecamlp5"
+ printf "\tSpecifies to use camlp5 instead of camlp4\n"
+ echo "-usecamlp4"
+ printf "\tSpecifies to use camlp4 instead of camlp5\n"
+ echo "-camlp5dir <dir>"
printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
- echo "-arch"
+ echo "-arch <arch>"
printf "\tSpecifies the architecture\n"
echo "-opt"
printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
@@ -67,16 +72,14 @@ usage () {
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 "-nomacintegration"
+ printf "\tSpecifies to not try to build coqide mac integration\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"
@@ -85,6 +88,8 @@ usage () {
printf "\tAdd profiling information in the Coq executables\n"
echo "-annotate"
printf "\tCompiles Coq with -dtypes option\n"
+ echo "-makecmd <command>"
+ printf "\tName of GNU Make command.\n"
}
@@ -109,10 +114,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
@@ -121,6 +122,8 @@ src_spec=no
prefix_spec=no
bindir_spec=no
libdir_spec=no
+configdir_spec=no
+datadir_spec=no
mandir_spec=no
docdir_spec=no
emacslib_spec=no
@@ -130,6 +133,7 @@ lablgtkdir_spec=no
coqdocdir_spec=no
arch_spec=no
coqide_spec=no
+nomacintegration_spec=no
browser_spec=no
wwwcoq_spec=no
with_geoproof=false
@@ -137,6 +141,7 @@ with_doc=all
with_doc_spec=no
force_caml_version=no
force_caml_version_spec=no
+usecamlp5=yes
COQSRC=`pwd`
@@ -157,8 +162,7 @@ while : ; do
-coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
coqtoolsbyteflags="$2"
shift;;
- -custom|--custom) custom_spec=yes
- shift;;
+ -custom|--custom) custom_spec=yes;;
-src|--src) src_spec=yes
COQSRC="$2"
shift;;
@@ -168,6 +172,12 @@ while : ; do
-libdir|--libdir) libdir_spec=yes
libdir="$2"
shift;;
+ -configdir|--configdir) configdir_spec=yes
+ configdir="$2"
+ shift;;
+ -datadir|--datadir) datadir_spec=yes
+ datadir="$2"
+ shift;;
-mandir|--mandir) mandir_spec=yes
mandir="$2"
shift;;
@@ -179,6 +189,7 @@ while : ; do
shift;;
-emacs |--emacs) emacs_spec=yes
emacs="$2"
+ printf "Warning: obsolete -emacs option\n"
shift;;
-coqdocdir|--coqdocdir) coqdocdir_spec=yes
coqdocdir="$2"
@@ -189,7 +200,12 @@ while : ; do
-lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
lablgtkdir="$2"
shift;;
+ -usecamlp5|--usecamlp5)
+ usecamlp5=yes;;
+ -usecamlp4|--usecamlp4)
+ usecamlp5=no;;
-camlp5dir|--camlp5dir)
+ usecamlp5=yes
camlp5dir="$2"
shift;;
-arch|--arch) arch_spec=yes
@@ -209,6 +225,8 @@ while : ; do
*) COQIDE=no
esac
shift;;
+ -nomacintegration) nomacintegration_spec=yes
+ shift;;
-browser|--browser) browser_spec=yes
BROWSER=$2
shift;;
@@ -227,18 +245,8 @@ 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;;
-debug|--debug) coq_debug_flag=-g;;
-profile|--profile) coq_profile_flag=-p;;
@@ -263,28 +271,31 @@ 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"`;;
+ *) 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/arch ; then
+ if test -x /bin/uname ; then
+ ARCH=`/bin/uname -s`
+ elif test -x /usr/bin/uname ; then
+ ARCH=`/usr/bin/uname -s`
+ elif 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"\
@@ -319,7 +330,7 @@ fi
# make command
-MAKE=`which make`
+MAKE=`which ${makecmd:-make}`
if [ "$MAKE" != "" ]; then
MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
@@ -328,6 +339,8 @@ if [ "$MAKE" != "" ]; then
echo "You have GNU Make $MAKEVERSION. Good!"
else
OK="no"
+ #Extra support for local installation of make 3.81
+ #will be useless when make >= 3.81 will be standard
if [ -x ./make ]; then
MAKEVERSION=`./make -v | head -1`
if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
@@ -356,7 +369,8 @@ fi
if [ "$browser_spec" = "no" ]; then
case $ARCH in
- win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
+ win32) BROWSER='start %s' ;;
+ Darwin) BROWSER='open %s' ;;
*) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
esac
fi
@@ -404,24 +418,38 @@ 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.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*)
+ 1.*|2.*|3.0*|3.10*|3.11.[01])
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 " You need Objective-Caml 3.11.2 or later."
echo " Configuration script failed!"
exit 1
fi;;
- ?*)
+ 3.11.2|3.12*|4.*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -435,16 +463,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"
;;
@@ -452,13 +473,13 @@ 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
fi
-case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
+case $HASNATDYNLINK,$ARCH,`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
@@ -483,75 +504,86 @@ esac
# Camlp4 / Camlp5 configuration
-if [ "$camlp5dir" != "" ]; then
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day)
+CAMLP4BIN=${CAMLBIN}
+
+case $usecamlp5 in
+ yes)
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
+ CAMLP4MOD=gramlib
+ if [ "$camlp5dir" != "" ]; then
+ if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
+ CAMLP4LIB=$camlp5dir
+ FULLCAMLP4LIB=$camlp5dir
+ else
+ echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+ echo "Configuration script failed!"
+ exit 1
+ fi
+ elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
+ CAMLP4LIB=+camlp5
+ FULLCAMLP4LIB=${CAMLLIB}/camlp5
+ elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
+ CAMLP4LIB=+site-lib/camlp5
+ FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
+ else
+ echo "No Camlp5 installation found. Looking for Camlp4 instead..."
+ usecamlp5=no
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
+
+# 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
-fi
+esac
-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
+# We might now try to use Camlp4, either by explicit choice or
+# by lack of proper Camlp5 installation
+case $usecamlp5 in
+ no)
+ CAMLP4=camlp4
+ CAMLP4MOD=camlp4lib
+ CAMLP4LIB=+camlp4
+ FULLCAMLP4LIB=${CAMLLIB}/camlp4
-case $CAMLP4LIB in
- +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
- *) FULLCAMLP4LIB=$CAMLP4LIB;;
-esac
+ if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
+ echo "No Camlp4 installation found."
+ echo "Configuration script failed!"
+ exit 1
+ fi
-# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-# (this should become configurable some day)
-CAMLP4BIN=${CAMLBIN}
+ camlp4oexec=${camlp4oexec}rf
+ if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
+ echo "Error: $camlp4oexec not found or not executable."
+ echo "Configuration script failed!"
+ exit 1
+ fi
+esac
# 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
+ if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.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!"
+ 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
@@ -561,23 +593,22 @@ fi
# OS dependent libraries
+OSDEPLIBS="-cclib -lunix"
case $ARCH 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;;
- alpha) OSDEPLIBS="-cclib -lunix";;
- win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix"
- cflags="-mno-cygwin $cflags";;
- *) OSDEPLIBS="-cclib -lunix"
esac
# lablgtk2 and CoqIDE
+IDEARCHFLAGS=
+IDEARCHFILE=
+IDEARCHDEF=X11
+
# -byte-only should imply -coqide byte, unless the user decides otherwise
if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then
@@ -591,15 +622,31 @@ 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 lablgtkdirtmp=$(ocamlfind query lablgtk2 2> /dev/null); then
+ if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then
+ lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind"
+ lablgtkdir=$lablgtkdirtmp
+ LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
+ else
+ echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)."
+ fi
+ fi
+ if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.mli" -a -f "${CAMLLIB}/glib.mli" ]; then
+ lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory"
lablgtkdir=${CAMLLIB}/lablgtk2
- elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
- lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
+ LABLGTKLIB=+lablgtk2 # Pour le message utilisateur
fi;;
yes)
- if [ ! -f "$lablgtkdir/glib.mli" ]; then
- echo "Incorrect LablGtk2 library (glib.mli not found)."
+ if [ ! -d "$lablgtkdir" ]; then
+ echo "$lablgtkdir is not a valid directory."
+ echo "Configuration script failed!"
+ exit 1
+ elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then
+ lablgtkdirfoundmsg="LablGtk2 directory found"
+ LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
+ else
+ echo "Headers missing in LablGtk2 library (glib.cmi/glib.mli not found)."
echo "Configuration script failed!"
exit 1
fi;;
@@ -608,40 +655,50 @@ else
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."
+ echo "$lablgtkdirfoundmsg 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."
+ echo "$lablgtkdirfoundmsg, 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."
+ echo "$lablgtkdirfoundmsg, no native threads: bytecode CoqIde will be available."
COQIDE=byte
- else
- echo "LablGtk2 found, native threads: native CoqIde will be available."
+ else
+ echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available."
COQIDE=opt
+ if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null);
+ then
+ IDEARCHFLAGS=lablgtkosx.cmxa
+ IDEARCHDEF=QUARTZ
+ elif [ "$ARCH" = "win32" ];
+ then
+ IDEARCHFLAGS=
+ IDEARCHFILE=ide/ide_win32_stubs.o
+ IDEARCHDEF=WIN32
+ fi
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="";;
+ LABLGTKINCLUDES="-I $LABLGTKLIB";;
+ no)
+ LABLGTKINCLUDES="";;
esac
+[ x$lablgtkosxdir = x ] || LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir"
+
# strip command
case $ARCH in
- win32)
- # true -> strip : it exists under cygwin !
- STRIPCOMMAND="strip";;
+ Darwin) if [ "$HASNATDYNLINK" = "true" ]
+ then
+ STRIPCOMMAND="true"
+ else
+ STRIPCOMMAND="strip"
+ fi;;
*)
- if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
- [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
+ if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
then
STRIPCOMMAND="true"
else
@@ -649,13 +706,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"
@@ -673,30 +723,37 @@ 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 $ARCH in
+case $src_spec in
+ no) COQTOP=${COQSRC}
+esac
+
+case $ARCH$CYGWIN 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';;
+ 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
- mandir_def=/usr/local/man
+ configdir_def=/etc/xdg/coq
+ datadir_def=/usr/local/share/coq
+ 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
@@ -705,7 +762,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;;
@@ -716,24 +773,56 @@ esac
case $libdir_spec/$prefix_spec/$local in
yes/*/*) LIBDIR=$libdir;;
*/yes/*)
+ libdir_spec=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]? "
+ *) printf "Where should I install the Coq library [%s]? " "$libdir_def"
read LIBDIR
+ libdir_spec=yes
case $LIBDIR in
"") LIBDIR=$libdir_def;;
*) true;;
esac;;
esac
+case $configdir_spec/$prefix_spec/$local in
+ yes/*/*) CONFIGDIR=$configdir;;
+ */yes/*) configdir_spec=yes
+ case $ARCH in
+ win32) CONFIGDIR=$prefix/config;;
+ *) CONFIGDIR=$prefix/etc/xdg/coq;;
+ esac;;
+ */*/true) CONFIGDIR=$COQTOP/ide
+ configdir_spec=yes;;
+ *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
+ read CONFIGDIR
+ case $CONFIGDIR in
+ "") CONFIGDIR=$configdir_def;;
+ *) configdir_spec=yes;;
+ esac;;
+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 [%s]? " "$datadir_def"
+ read DATADIR
+ case $DATADIR in
+ "") DATADIR=$datadir_def;;
+ *) datadir_spec=yes;;
+ esac;;
+esac
+
case $mandir_spec/$prefix_spec/$local in
yes/*/*) MANDIR=$mandir;;
- */yes/*) MANDIR=$prefix/man ;;
+ */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;;
@@ -742,13 +831,13 @@ case $mandir_spec/$prefix_spec/$local in
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]? "
+ yes/*/*) DOCDIR=$docdir;;
+ */yes/*) DOCDIR=$prefix/share/doc/coq;;
+ */*/true) DOCDIR=$COQTOP/doc;;
+ *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
read DOCDIR
case $DOCDIR in
- "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;;
+ "") DOCDIR=$docdir_def;;
*) true;;
esac;;
esac
@@ -761,7 +850,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;;
@@ -777,7 +866,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;;
@@ -787,7 +876,7 @@ esac
# Determine if we enable -custom by default (Windows and MacOS)
CUSTOM_OS=no
-if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
CUSTOM_OS=yes
fi
@@ -807,14 +896,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
@@ -841,6 +930,9 @@ fi
if test "$COQIDE" != "no"; then
echo " Lablgtk2 library in : $LABLGTKLIB"
fi
+if test "$IDEARCHDEF" = "QUARTZ"; then
+echo " Mac OS integration is on"
+fi
if test "$with_doc" = "all"; then
echo " Documentation : All"
else
@@ -854,6 +946,8 @@ echo ""
echo " Paths for true installation:"
echo " binaries will be copied in $BINDIR"
echo " library will be copied in $LIBDIR"
+echo " config files will be copied in $CONFIGDIR"
+echo " data files will be copied in $DATADIR"
echo " man pages will be copied in $MANDIR"
echo " documentation will be copied in $DOCDIR"
echo " emacs mode will be copied in $EMACSLIB"
@@ -904,49 +998,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'`
- 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
#####################################################
@@ -957,8 +1065,10 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
let local = $local
let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let coqlib = "$LIBDIR"
-let coqsrc = "$COQSRC"
+let coqlib = $LIBDIR_OPTION
+let configdir = $CONFIGDIR_OPTION
+let datadir = $DATADIR_OPTION
+let docdir = "$DOCDIR"
let ocaml = "$ocamlexec"
let ocamlc = "$bytecamlc"
let ocamlopt = "$nativecamlc"
@@ -979,6 +1089,7 @@ let cflags = "$cflags"
let best = "$best_compiler"
let arch = "$ARCH"
let has_coqide = "$COQIDE"
+let gtk_platform = \`$IDEARCHDEF
let has_natdynlink = $HASNATDYNLINK
let natdynlinkflag = "$NATDYNLINKFLAG"
let osdeplibs = "$OSDEPLIBS"
@@ -994,7 +1105,7 @@ let browser = "$BROWSER"
let wwwcoq = "$WWWCOQ"
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-let localwwwrefman = "file://$HTMLREFMANDIR/"
+let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
END_OF_COQ_CONFIG
@@ -1022,57 +1133,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|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"
+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"
@@ -1085,4 +1282,3 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 15089 2012-03-26 16:41:59Z notin $
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-26 11:48:45 +0000