diff options
| -rw-r--r-- | config/Makefile.template | 8 | ||||
| -rwxr-xr-x | configure | 133 |
2 files changed, 77 insertions, 64 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index a4242ae0e..0749c3540 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -24,10 +24,10 @@ LOCAL=LOCALINSTALLATION # 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 -COQLIB=COQLIBDIRECTORY -MANDIR=MANDIRDIRECTORY -EMACSLIB=EMACSLIBDIRECTORY +BINDIR="BINDIRDIRECTORY" +COQLIB="COQLIBDIRECTORY" +MANDIR="MANDIRDIRECTORY" +EMACSLIB="EMACSLIBDIRECTORY" EMACS=EMACSCOMMAND # Path to Coq distribution @@ -125,7 +125,7 @@ case $arch_spec in ARCH=`/usr/ucb/arch` elif test -x /bin/uname && (/bin/uname -s | grep -q -i CYGWIN) ; then ARCH=win32 - # cygwin returns a name of the form \\cygdrive\\c\\... + # cygwin returns a name of the form /cygdrive/c/... # that coqc does not understand; need to transform it COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"` elif test -x /usr/bin/uname ; then @@ -143,10 +143,10 @@ esac case $ARCH in win32) - bindir_def=\\coq\\bin - libdir_def=\\coq\\lib - mandir_def=\\coq\\man - emacslib_def=\\coq\\emacs;; + bindir_def=C:\\coq\\bin + libdir_def=C:\\coq\\lib + mandir_def=C:\\coq\\man + emacslib_def=C:\\coq\\emacs;; *) bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq @@ -341,9 +341,9 @@ fi # Tell on windows if ocaml understands cygwin or windows path formats -"$CAMLC" -o config/giveostype config/giveostype.ml -CAMLOSTYPE=`config/giveostype` -rm config/giveostype +#"$CAMLC" -o config/giveostype config/giveostype.ml +#CAMLOSTYPE=`config/giveostype` +#rm config/giveostype case $ARCH in win32) @@ -385,16 +385,75 @@ echo " man pages will be copied in $MANDIR" echo " emacs mode will be copied in $EMACSLIB" echo "" +##################################################### +# Building the $COQTOP/config/coq_config.ml file +##################################################### + +# damned backslashes under M$Windows +case $ARCH in + win32) + CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` + BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` + LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` + MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` + ;; +esac + +mlconfig_file=$COQTOP/config/coq_config.ml +rm -f $mlconfig_file +cat << END_OF_COQ_CONFIG > $mlconfig_file +(* DO NOT EDIT THIS FILE: automatically generated by ../configure *) + +let local = $local +let bindir = "$BINDIR" +let coqlib = "$LIBDIR" +let coqtop = "$COQTOP" +let camllib = "$CAMLLIB" +let camlp4lib = "$CAMLP4LIB" +let best = "$best_compiler" +let arch = "$ARCH" +let osdeplibs = "$OSDEPLIBS" +let version = "$VERSION" +let versionsi = "$VERSIONSI" +let date = "$DATE" +let compile_date = "$COMPILEDATE" +let exec_extension = "$EXE" + +END_OF_COQ_CONFIG + +# to be sure printf is found on windows when spaces occur in PATH variable +PRINTF=`which printf` + +# Subdirectories of theories/ added in coq_config.ml +subdirs () { + (cd $1; find * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file) +} + +echo "let theories_dirs = [" >> $mlconfig_file +subdirs theories +echo "]" >> $mlconfig_file + +echo "let contrib_dirs = [" >> $mlconfig_file +subdirs contrib +echo "]" >> $mlconfig_file + +chmod a-w $mlconfig_file + + +############################################### # Building the $COQTOP/config/Makefile file +############################################### rm -f $COQTOP/config/Makefile +# damned backslashes under M$Windows (bis) case $ARCH in win32) - BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'` - LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'` - MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'` - EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|/|g'` + BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` + LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` + MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` ;; esac @@ -426,7 +485,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \ chmod a-w $COQTOP/config/Makefile +################################################## # Building the $COQTOP/dev/ocamldebug-v7 file +#################################################### if test "$coq_debug_flag" = "-g" ; then rm -f $COQTOP/dev/ocamldebug-v7 @@ -443,54 +504,6 @@ if test "$coq_debug_flag" = "-g" ; then chmod a-w,a+x $COQTOP/dev/ocamldebug-v7 fi -# Building the $COQTOP/config/coq_config.ml file - -mlconfig_file=$COQTOP/config/coq_config.ml -rm -f $mlconfig_file -cat << END_OF_COQ_CONFIG > $mlconfig_file -(* DO NOT EDIT THIS FILE: automatically generated by ../configure *) - -let local = $local -let bindir = "$BINDIR" -let coqlib = "$LIBDIR" -let coqtop = "$COQTOP" -let camllib = "$CAMLLIB" -let camlp4lib = "$CAMLP4LIB" -let best = "$best_compiler" -let arch = "$ARCH" -let osdeplibs = "$OSDEPLIBS" -let version = "$VERSION" -let versionsi = "$VERSIONSI" -let date = "$DATE" -let compile_date = "$COMPILEDATE" -let exec_extension = "$EXE" - -END_OF_COQ_CONFIG - -# to be sure printf is found on windows when spaces occur in PATH variable -PRINTF=`which printf` - -# Subdirectories of theories/ added in coq_config.ml -subdirs () { - (cd $1; find * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file) -} - -echo "let theories_dirs = [" >> $mlconfig_file -subdirs theories -echo "]" >> $mlconfig_file - -echo "let contrib_dirs = [" >> $mlconfig_file -subdirs contrib -echo "]" >> $mlconfig_file - -if test "$CAMLOSTYPE" = "Win32" ; then -# We change: / -> \\ and \ -> \\ (dos paths) -# This is a bit tricky -sed -e "s|\\\\\\\\\\\\\\\|\\\|" -e "s|/|\\\|g" -e "s|\\\|\\\\\\\|g" $mlconfig_file > $mlconfig_file.win -mv $mlconfig_file.win $mlconfig_file -fi -chmod a-w $mlconfig_file - echo "If anything in the above is wrong, please restart './configure'" echo echo "*Warning* To compile the system for a new architecture" |