From d05961c7e6cb4a2f8cb70b136f58ef3dee2a9b32 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 23 May 2012 13:37:51 +0000 Subject: configure: add support of MinGW Win32 environment (fix #2526) * Since MinGW/Msys doesn't provide a cygpath utility, we emulate it via an ocaml script tools/mingwpath.ml * Avoid the crazy sed portions for backslash escaping, instead use a more robust ocaml script tools/escape_string.ml based on String.escaped * No more config/Makefile.template + sed on it, but rather a "cat << EOF > ..." as for config/coq_config.ml * Normally, support of Cygwin should be preserved, as well as mingw32 cross-compilation from linux (cf. myocamlbuild.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7 --- configure | 389 ++++++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 237 insertions(+), 152 deletions(-) (limited to 'configure') diff --git a/configure b/configure index ed9a99e8f1..9a1970fb9a 100755 --- a/configure +++ b/configure @@ -297,17 +297,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 @@ -442,9 +444,19 @@ if test ! -f "$CAMLC" ; then exit 1 fi -# Under Windows, OCaml only understands Windows filenames (C:\...) +# 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" "$COQSRC/tools/mingwpath.ml" "$1" ;; + *) echo "$1" ;; + esac +} + case $ARCH in - win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;; + win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;; esac CAMLVERSION=`"$bytecamlc" -version` @@ -490,7 +502,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 @@ -600,18 +612,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 @@ -691,9 +702,6 @@ esac # strip command case $ARCH in - win32) - # true -> strip : it exists under cygwin ! - STRIPCOMMAND="strip";; Darwin) if [ "$HASNATDYNLINK" = "true" ] then STRIPCOMMAND="true" @@ -709,13 +717,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" @@ -739,20 +740,20 @@ esac # OCaml only understand Windows filenames (C:\...) case $ARCH in - win32) COQTOP=`cygpath -m ${COQTOP}` + win32) COQTOP=`mk_win_path "$COQTOP"` 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 @@ -761,7 +762,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 @@ -770,7 +771,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;; @@ -787,7 +788,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 @@ -796,11 +797,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 @@ -810,7 +806,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;; @@ -818,17 +814,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;; @@ -836,17 +827,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;; @@ -858,7 +843,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;; @@ -874,7 +859,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;; @@ -890,7 +875,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;; @@ -920,14 +905,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 @@ -1007,51 +992,65 @@ 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 < "$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 +TYPEREX=$coq_typerex_wrapper + +# 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 + +# Your C compiler and co +CC="$gcc_exec" +AR="$ar_exec" +RANLIB="$ranlib_exec" + +# 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" -- cgit v1.2.3