diff options
| -rw-r--r-- | config/Makefile.template | 155 | ||||
| -rwxr-xr-x | configure | 389 | ||||
| -rw-r--r-- | tools/escape_string.ml | 1 | ||||
| -rw-r--r-- | tools/mingwpath.ml | 15 |
4 files changed, 253 insertions, 307 deletions
diff --git a/config/Makefile.template b/config/Makefile.template deleted file mode 100644 index f406ab6fb..000000000 --- a/config/Makefile.template +++ /dev/null @@ -1,155 +0,0 @@ -################################## -# -# Configuration file for Coq -# -################################## - -############################################################################# -# -# This file is generated by the script "configure" -# -# DO NOT EDIT IT !! 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=LOCALINSTALLATION - -# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun") -COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS -COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS -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="BINDIRDIRECTORY" -COQLIBINSTALL="COQLIBDIRECTORY" -CONFIGDIR="CONFIGDIRDIRECTORY" -DATADIR="DATADIRDIRECTORY" -MANDIR="MANDIRDIRECTORY" -DOCDIR="DOCDIRDIRECTORY" -EMACSLIB="EMACSLIBDIRECTORY" -EMACS=EMACSCOMMAND - -# Path to Coq distribution -COQSRC=COQSRCDIRECTORY -VERSION=COQVERSION - -# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH -CAMLP4BIN="CAMLP4BINDIRECTORY" - -# Ocaml version number -CAMLVERSION=CAMLTAG - -# Ocaml libraries -CAMLLIB="CAMLLIBDIRECTORY" - -# Ocaml .h directory -CAMLHLIB="CAMLLIBDIRECTORY" - -# Camlp4 library directory (avoid CAMLP4LIB used on Windows) -CAMLP4=CAMLP4VARIANT -CAMLP4O=CAMLP4TOOL -CAMLP4COMPAT=CAMLP4COMPATFLAGS -MYCAMLP4LIB="CAMLP4LIBDIRECTORY" - -# 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="CAMLMKTOPEXEC" - -# Caml flags -CAMLFLAGS=-rectypes CAMLANNOTATEFLAG -TYPEREX=TYPEREXCMD - -# Compilation debug flags -CAMLDEBUG=COQDEBUGFLAG -CAMLDEBUGOPT=COQDEBUGFLAGOPT - -# User compilation flag -USERFLAGS= - -# Flags for GCC -CFLAGS=CCOMPILEFLAGS - -# Compilation profile flag -CAMLTIMEPROF=COQPROFILEFLAG - -# The best compiler: native (=opt) or bytecode (=byte) if no native compiler -BEST=BESTCOMPILER - -# Your architecture -# Can be obtain by UNIX command arch -ARCH=ARCHITECTURE -HASNATDYNLINK=HASNATIVEDYNLINK - -# Your C compiler and co -CC="CCEXEC" -AR="AREXEC" -RANLIB="RANLIBEXEC" - -# Supplementary libs for some systems, currently: -# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket -# . others : -cclib -lunix -# . windows : -cclib -lunix - -OSDEPLIBS=OSDEPENDENTLIBS - -# executable files extension, currently: -# Unix systems: -# Win32 systems : .exe -EXE=EXECUTEEXTENSION -DLLEXT=DLLEXTENSION - -# 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="COQDOCDIRECTORY" - -# command to update TeX' kpathsea database -#MKTEXLSR=MKTEXLSRCOMMAND - -#the command STRIP -# Unix systems and profiling: true -# Unix systems and no profiling: strip -# Win32 systems: true (actually strip is bogus) -STRIP=STRIPCOMMAND - -# CoqIde (no/byte/opt) -HASCOQIDE=COQIDEOPT -IDEOPTFLAGS=IDEARCHFLAGS -IDEOPTDEPS=IDEARCHFILE -IDEOPTINT=IDEARCHDEF - -# Defining REVISION -CHECKEDOUT=CHECKEDOUTSOURCETREE - -# Option to control compilation and installation of the documentation -WITHDOC=WITHDOCOPT - -# make or sed are bogus and believe lines not terminating by a return -# are inexistent @@ -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 <<EOF - prerr_endline(String.escaped(Sys.getenv"$VAR"));; -EOF +escape_string () { + "$ocamlexec" "$COQSRC/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'` + COQSRC=`mk_win_path "$COQSRC"` + + 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 ##################################################### @@ -1131,63 +1130,149 @@ ln -sf "$mlconfig_file" "$mymlconfig_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|TYPEREXCMD|$coq_typerex_wrapper|" \ - -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 +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" diff --git a/tools/escape_string.ml b/tools/escape_string.ml new file mode 100644 index 000000000..50e8faada --- /dev/null +++ b/tools/escape_string.ml @@ -0,0 +1 @@ +print_string (String.escaped Sys.argv.(1)) diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml new file mode 100644 index 000000000..f01b62cce --- /dev/null +++ b/tools/mingwpath.ml @@ -0,0 +1,15 @@ +(** Mingwpath *) + +(** Converts mingw-encoded filenames such as: + + /c/Program Files/Ocaml/bin + + to a more windows-friendly form (but still with / instead of \) : + + c:/Program Files/Ocaml/bin + + This nice hack was suggested by Benjamin Monate (cf bug #2526) + to mimic the cygwin-specific tool cygpath +*) + +print_string Sys.argv.(1) |