3
##################################
5
# Configuration script for Coq
7
##################################
12
DATE=`LANG=C date +"%B %Y"`
14
# Create the bin/ directory if non-existent
15
test -d bin || mkdir bin
17
# a local which command for sh
19
IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
21
if test -z "$i"; then i=.; fi
22
if [ -f "$i/$1" ] ; then
31
printf "Available options for configure are:\n"
33
printf "\tDisplays this help page\n"
35
printf "\tSet installation directory to <dir>\n"
37
printf "\tSet installation directory to the current source tree\n"
38
echo "-coqrunbyteflags"
39
printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
40
echo "-coqtoolsbyteflags"
41
printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
43
printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
45
printf "\tSpecifies the source directory\n"
50
printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
53
printf "\tSpecifies where emacs files are to be installed\n"
55
printf "\tSpecifies where Coqdoc style files are to be installed\n"
57
printf "\tSpecifies the path to the OCaml library\n"
59
printf "\tSpecifies the path to the Lablgtk library\n"
61
printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
63
printf "\tSpecifies the architecture\n"
65
printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
66
echo "-fsets (all|basic)"
67
echo "-reals (all|basic)"
68
printf "\tSpecifies whether or not to compile full FSets/Reals library\n"
69
echo "-coqide (opt|byte|no)"
70
printf "\tSpecifies whether or not to compile Coqide\n"
71
echo "-browser <command>"
72
printf "\tUse <command> to open URL %%s\n"
73
echo "-with-doc (yes|no)"
74
printf "\tSpecifies whether or not to compile the documentation\n"
75
echo "-with-geoproof (yes|no)"
76
printf "\tSpecifies whether or not to use Geoproof binding\n"
77
echo "-with-cc <file>"
78
echo "-with-ar <file>"
79
echo "-with-ranlib <file>"
80
printf "\tTells configure where to find gcc/ar/ranlib executables\n"
82
printf "\tCompiles only bytecode version of Coq\n"
84
printf "\tAdd debugging information in the Coq executables\n"
86
printf "\tAdd profiling information in the Coq executables\n"
88
printf "\tCompiles Coq with -dtypes option\n"
92
# Default OCaml binaries
95
ocamlmklibexec=ocamlmklib
100
ocamlyaccexec=ocamlyacc
101
ocamlmktopexec=ocamlmktop
110
cflags="-fno-defer-pop -Wall -Wno-unused"
117
coqrunbyteflags_spec=no
118
coqtoolsbyteflags_spec=no
143
# Parse command-line arguments
150
-prefix|--prefix) prefix_spec=yes
153
-local|--local) local=true;;
154
-coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
157
-coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
158
coqtoolsbyteflags="$2"
160
-custom|--custom) custom_spec=yes
162
-src|--src) src_spec=yes
165
-bindir|--bindir) bindir_spec=yes
168
-libdir|--libdir) libdir_spec=yes
171
-mandir|--mandir) mandir_spec=yes
174
-docdir|--docdir) docdir_spec=yes
177
-emacslib|--emacslib) emacslib_spec=yes
180
-emacs |--emacs) emacs_spec=yes
183
-coqdocdir|--coqdocdir) coqdocdir_spec=yes
186
-camldir|--camldir) camldir_spec=yes
189
-lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
192
-camlp5dir|--camlp5dir)
195
-arch|--arch) arch_spec=yes
198
-opt|--opt) bytecamlc=ocamlc.opt
199
camlp4oexec=camlp4o # can't add .opt since dyn load'll be required
200
nativecamlc=ocamlopt.opt;;
201
-fsets|--fsets) case "$2" in
206
-reals|--reals) case "$2" in
211
-coqide|--coqide) coqide_spec=yes
213
byte|opt) COQIDE=$2;;
217
-browser|--browser) browser_spec=yes
220
-coqwebsite|--coqwebsite) wwwcoq_spec=yes
223
-with-doc|--with-doc) with_doc_spec=yes
225
yes|all) with_doc=all;;
229
-with-geoproof|--with-geoproof)
231
yes) with_geoproof=true;;
232
no) with_geoproof=false;;
235
-with-cc|-with-gcc|--with-cc|--with-gcc)
243
-with-ranlib|--with-ranlib)
247
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
248
-debug|--debug) coq_debug_flag=-g;;
249
-profile|--profile) coq_profile_flag=-p;;
250
-annotate|--annotate) coq_annotate_flag=-dtypes;;
251
*) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
256
if [ $prefix_spec = yes -a $local = true ] ; then
257
echo "Options -prefix and -local are incompatible"
258
echo "Configure script failed!"
265
"") echo "I can't find the program \"date\" in your path."
266
echo "Please give me the current date"
268
*) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
275
# First we test if we are running a Cygwin system
276
if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
279
# If not, we determine the architecture
280
if test -x /bin/arch ; then
282
elif test -x /usr/bin/arch ; then
284
elif test -x /usr/ucb/arch ; then
286
elif test -x /bin/uname ; then
288
elif test -x /usr/bin/uname ; then
289
ARCH=`/usr/bin/uname -s`
291
echo "I can not automatically find the name of your architecture"
293
"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
300
# executable extension
310
# Is the source tree checked out from a recognised
311
# version control system ?
312
if test -e .svn/entries ; then
314
elif [ -d '{arch}' ]; then
316
elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
325
if [ "$MAKE" != "" ]; then
326
MAKEVERSION=`$MAKE -v | head -1`
329
echo "You have GNU Make 3.81. Good!";;
332
if [ -x ./make ]; then
333
MAKEVERSION=`./make -v | head -1`
334
if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
336
if [ $OK = "no" ]; then
337
echo "GNU Make >= 3.81 is needed"
338
echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
339
echo "then locally installed on a Unix-style system by issuing:"
340
echo " tar xzvf make-3.81.tar.gz"
346
echo "Restart then the configure script and later use ./make instead of make"
349
echo "You have locally installed GNU Make 3.81. Good!"
353
echo "Cannot find GNU Make 3.81"
358
if [ "$browser_spec" = "no" ]; then
360
win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
361
*) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
365
if [ "$wwwcoq_spec" = "no" ]; then
366
WWWCOQ="http://www.lix.polytechnique.fr/coq/"
369
#########################################
370
# Objective Caml programs
372
case $camldir_spec in
373
no) CAMLC=`which $bytecamlc`
375
"") echo "$bytecamlc is not present in your path!"
376
echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
380
"") CAMLC=/usr/local/bin/$bytecamlc;;
381
*/ocamlc|*/ocamlc.opt) true;;
382
*/) CAMLC="${CAMLC}"$bytecamlc;;
383
*) CAMLC="${CAMLC}"/$bytecamlc;;
386
CAMLBIN=`dirname "$CAMLC"`;;
387
yes) CAMLC=$camldir/$bytecamlc
389
CAMLBIN=`dirname "$CAMLC"`
391
nativecamlc=$CAMLBIN/$nativecamlc
392
ocamlexec=$CAMLBIN/ocaml
393
ocamldepexec=$CAMLBIN/ocamldep
394
ocamldocexec=$CAMLBIN/ocamldoc
395
ocamllexexec=$CAMLBIN/ocamllex
396
ocamlyaccexec=$CAMLBIN/ocamlyacc
397
ocamlmktopexec=$CAMLBIN/ocamlmktop
398
ocamlmklibexec=$CAMLBIN/ocamlmklib
399
camlp4oexec=$CAMLBIN/camlp4o
402
if test ! -f "$CAMLC" ; then
403
echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
404
echo "Configuration script failed!"
408
# Under Windows, OCaml only understands Windows filenames (C:\...)
410
win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
413
# this fixes a camlp4 bug under FreeBSD
414
# ("native-code program cannot do a dynamic load")
415
if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
417
CAMLVERSION=`"$bytecamlc" -version`
420
1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.08.0)
421
echo "Your version of Objective-Caml is $CAMLVERSION."
422
if [ "$CAMLVERSION" = "3.08.0" ] ; then
423
echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!"
425
echo "You need Objective-Caml 3.07 or later!"
427
echo "Configuration script failed!"
430
echo "You have Objective-Caml $CAMLVERSION. Good!";;
432
CAMLP4COMPAT="-loc loc"
433
echo "You have Objective-Caml $CAMLVERSION. Good!";;
435
echo "I found the Objective-Caml compiler but cannot find its version number!"
436
echo "Is it installed properly?"
437
echo "Configuration script failed!"
441
CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
443
# For coqmktop & bytecode compiler
446
win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
447
CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
449
CAMLLIB=`"$CAMLC" -where`
452
# We need to set va special flag for OCaml 3.07
455
cflags="$cflags -DOCAML_307";;
458
if [ "$coq_debug_flag" = "-g" ]; then
461
# Compilation debug flag
462
coq_debug_flag_opt="-g"
468
if test -f `"$CAMLC" -where`/dynlink.cmxa; then
474
# Camlp4 / Camlp5 configuration
476
if [ "$camlp5dir" != "" ]; then
479
if [ ! -f $camlp5dir/camlp5.cma ]; then
480
echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)"
481
echo "Configuration script failed!"
484
camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
485
if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
486
echo "Error: Camlp5 found, but in strict mode!"
487
echo "Please compile Camlp5 in transitional mode."
493
if [ -x "${CAMLLIB}/camlp5" ]; then
495
elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
496
CAMLP4LIB=+site-lib/camlp5
498
echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
499
echo "Configuration script failed!"
503
camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
504
if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then
505
echo "Error: Camlp5 found, but in strict mode!"
506
echo "Please compile Camlp5 in transitional mode."
517
if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
518
echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
519
echo "Configuration script failed!"
525
+*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
526
*) FULLCAMLP4LIB=$CAMLP4LIB;;
529
# Assume that camlp(4|5) binaries are at the same place as ocaml ones
530
# (this should become configurable some day)
533
# do we have a native compiler: test of ocamlopt and its version
535
if [ "$best_compiler" = "opt" ] ; then
536
if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
537
CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
538
if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
539
case $CAMLOPTVERSION in
541
*) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
543
echo "only the bytecode version of Coq will be available."
545
elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
547
echo "Cannot find native-code $CAMLP4,"
548
echo "only the bytecode version of Coq will be available."
550
if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
551
echo "Native and bytecode compilers do not have the same version!"
553
echo "You have native-code compilation. Good!"
557
echo "You have only bytecode compilation."
561
# OS dependent libraries
566
5*) OS="Sun Solaris $OS"
567
OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
569
OSDEPLIBS="-cclib -lunix"
571
alpha) OSDEPLIBS="-cclib -lunix";;
573
OSDEPLIBS="-cclib -lunix"
574
cflags="-mno-cygwin $cflags";;
575
*) OSDEPLIBS="-cclib -lunix"
578
# lablgtk2 and CoqIDE
580
# -byte-only should imply -coqide byte, unless the user decides otherwise
582
if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then
587
# Which coqide is asked ? which one is possible ?
589
if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
590
echo "CoqIde disabled as requested."
592
case $lablgtkdir_spec in
594
if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
595
lablgtkdir=${CAMLLIB}/lablgtk2
596
elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
597
lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
600
if [ ! -f "$lablgtkdir/glib.mli" ]; then
601
echo "Incorrect LablGtk2 library (glib.mli not found)."
602
echo "Configuration script failed!"
606
if [ "$lablgtkdir" = "" ]; then
607
echo "LablGtk2 not found: CoqIde will not be available."
609
elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
610
echo "LablGtk2 found but too old: CoqIde will not be available."
612
elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
613
echo "LablGtk2 found, bytecode CoqIde will be used as requested."
615
elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
616
echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
619
echo "LablGtk2 found, native threads: native CoqIde will be available."
626
case $lablgtkdir_spec in
627
no) LABLGTKLIB=+lablgtk2 # Pour le message
628
LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
629
yes) LABLGTKLIB="$lablgtkdir" # Pour le message
630
LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
632
no) LABLGTKINCLUDES="";;
635
# Tell on windows if ocaml understands cygwin or windows path formats
637
#"$CAMLC" -o config/giveostype config/giveostype.ml
638
#CAMLOSTYPE=`config/giveostype`
639
#rm config/giveostype
645
# true -> strip : it exists under cygwin !
646
STRIPCOMMAND="strip";;
648
if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
649
[ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
658
#MKTEXLSR=`which mktexlsr`
660
# "") MKTEXLSR=true;;
664
### Test if documentation can be compiled (latex, hevea)
666
if test "$with_doc" = "all"
668
if test "`which latex`" = ""
670
echo "latex was not found; documentation will not be available"
673
if test "`which hevea`" = ""
676
echo "hevea was not found: documentation will not be available"
681
###########################################
682
# bindir, libdir, mandir, docdir, etc.
688
# OCaml only understand Windows filenames (C:\...)
690
win32) COQTOP=`cygpath -m ${COQTOP}`
695
bindir_def='C:\coq\bin'
696
libdir_def='C:\coq\lib'
697
mandir_def='C:\coq\man'
698
docdir_def='C:\coq\doc'
699
emacslib_def='C:\coq\emacs'
700
coqdocdir_def='C:\coq\latex';;
702
bindir_def=/usr/local/bin
703
libdir_def=/usr/local/lib/coq
704
mandir_def=/usr/local/man
705
docdir_def=/usr/local/share/doc/coq
706
emacslib_def=/usr/local/share/emacs/site-lisp
707
coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
712
case $bindir_spec/$prefix_spec/$local in
713
yes/*/*) BINDIR=$bindir ;;
714
*/yes/*) BINDIR=$prefix/bin ;;
715
*/*/true) BINDIR=$COQTOP/bin ;;
716
*) printf "Where should I install the Coq binaries [$bindir_def]? "
719
"") BINDIR=$bindir_def;;
724
case $libdir_spec/$prefix_spec/$local in
725
yes/*/*) LIBDIR=$libdir;;
728
win32) LIBDIR=$prefix ;;
729
*) LIBDIR=$prefix/lib/coq ;;
731
*/*/true) LIBDIR=$COQTOP ;;
732
*) printf "Where should I install the Coq library [$libdir_def]? "
735
"") LIBDIR=$libdir_def;;
740
case $mandir_spec/$prefix_spec/$local in
741
yes/*/*) MANDIR=$mandir;;
742
*/yes/*) MANDIR=$prefix/man ;;
743
*/*/true) MANDIR=$COQTOP/man ;;
744
*) printf "Where should I install the Coq man pages [$mandir_def]? "
747
"") MANDIR=$mandir_def;;
752
case $docdir_spec/$prefix_spec/$local in
753
yes/*/*) DOCDIR=$docdir;;
754
*/yes/*) DOCDIR=$prefix/share/doc/coq ;;
755
*/*/true) DOCDIR=$COQTOP/man ;;
756
*) printf "Where should I install the Coq documentation [$docdir_def]? "
759
"") DOCDIR=$docdir_def;;
764
case $emacslib_spec/$prefix_spec/$local in
765
yes/*/*) EMACSLIB=$emacslib;;
768
win32) EMACSLIB=$prefix/emacs ;;
769
*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
771
*/*/true) EMACSLIB=$COQTOP/tools/emacs ;;
772
*) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
775
"") EMACSLIB=$emacslib_def;;
780
case $coqdocdir_spec/$prefix_spec/$local in
781
yes/*/*) COQDOCDIR=$coqdocdir;;
784
win32) COQDOCDIR=$prefix/latex ;;
785
*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
787
*/*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
788
*) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
791
"") COQDOCDIR=$coqdocdir_def;;
796
# Determine if we enable -custom by default (Windows and MacOS)
798
if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
802
BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
803
case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
804
yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
805
*/*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
806
*/true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
808
COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
809
BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
811
case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
812
yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
813
*/yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
814
*) COQTOOLSBYTEFLAGS="";;
817
# case $emacs_spec in
818
# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
822
# "") EMACS=$emacs_def;;
825
# yes) EMACS=$emacs;;
828
###########################################
829
# Summary of the configuration
832
echo " Coq top directory : $COQTOP"
833
echo " Architecture : $ARCH"
834
if test ! -z "$OS" ; then
835
echo " Operating system : $OS"
837
echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS"
838
echo " Coq tools bytecode link flags : $COQTOOLSBYTEFLAGS"
839
echo " OS dependent libraries : $OSDEPLIBS"
840
echo " Objective-Caml/Camlp4 version : $CAMLVERSION"
841
echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN"
842
echo " Objective-Caml library in : $CAMLLIB"
843
echo " Camlp4 library in : $CAMLP4LIB"
844
if test "$COQIDE" != "no"; then
845
echo " Lablgtk2 library in : $LABLGTKLIB"
847
if test "$fsets" = "all"; then
848
echo " FSets theory : All"
850
echo " FSets theory : Basic"
852
if test "$reals" = "all"; then
853
echo " Reals theory : All"
855
echo " Reals theory : Basic"
857
if test "$with_doc" = "all"; then
858
echo " Documentation : All"
860
echo " Documentation : None"
862
echo " CoqIde : $COQIDE"
863
echo " Web browser : $BROWSER"
864
echo " Coq web site : $WWWCOQ"
867
echo " Paths for true installation:"
868
echo " binaries will be copied in $BINDIR"
869
echo " library will be copied in $LIBDIR"
870
echo " man pages will be copied in $MANDIR"
871
echo " documentation will be copied in $DOCDIR"
872
echo " emacs mode will be copied in $EMACSLIB"
875
#####################################################
876
# Building the $COQTOP/config/coq_config.ml file
877
#####################################################
879
# An escaped version of a variable
881
"$ocamlexec" 2>&1 1>/dev/null <<EOF
882
prerr_endline(String.escaped(Sys.getenv"$VAR"));;
886
# Escaped version of browser command
888
ESCBROWSER=`VAR=BROWSER escape_var`
890
# damned backslashes under M$Windows
893
ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
894
ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
895
ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
896
ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
897
ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
898
ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
899
ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
900
ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
901
ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
902
ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
903
ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
904
ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
905
ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
906
ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
907
ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
908
ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
915
ESCCAMLDIR="$CAMLBIN"
916
ESCCAMLLIB="$CAMLLIB"
919
ESCEMACSLIB="$EMACSLIB"
920
ESCCOQDOCDIR="$COQDOCDIR"
921
ESCCAMLP4BIN="$CAMLP4BIN"
922
ESCCAMLP4LIB="$CAMLP4LIB"
923
ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
924
ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
925
ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
929
mlconfig_file="$COQSRC/config/coq_config.ml"
930
rm -f "$mlconfig_file"
931
cat << END_OF_COQ_CONFIG > $mlconfig_file
932
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
935
let coqrunbyteflags = "$ESCCOQRUNBYTEFLAGS"
936
let coqlib = "$ESCLIBDIR"
937
let coqsrc = "$ESCSRCDIR"
938
let camlbin = "$ESCCAMLDIR"
939
let camllib = "$ESCCAMLLIB"
940
let camlp4 = "$CAMLP4"
941
let camlp4bin = "$ESCCAMLP4BIN"
942
let camlp4lib = "$ESCCAMLP4LIB"
943
let best = "$best_compiler"
945
let has_natdynlink = $HASNATDYNLINK
946
let osdeplibs = "$OSDEPLIBS"
947
let version = "$VERSION"
948
let caml_version = "$CAMLVERSION"
950
let compile_date = "$COMPILEDATE"
951
let vo_magic_number = $VOMAGIC
952
let state_magic_number = $STATEMAGIC
953
let exec_extension = "$EXE"
954
let with_geoproof = ref $with_geoproof
955
let browser = "$ESCBROWSER"
956
let wwwcoq = "$WWWCOQ"
957
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
958
let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
962
# to be sure printf is found on windows when spaces occur in PATH variable
963
PRINTF=`which printf`
965
# Subdirectories of theories/ added in coq_config.ml
967
(cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) | grep -v correctness >> "$mlconfig_file")
970
echo "let theories_dirs = [" >> "$mlconfig_file"
972
echo "]" >> "$mlconfig_file"
974
echo "let contrib_dirs = [" >> "$mlconfig_file"
976
echo "]" >> "$mlconfig_file"
978
chmod a-w "$mlconfig_file"
981
###############################################
982
# Building the $COQTOP/config/Makefile file
983
###############################################
985
rm -f "$COQSRC/config/Makefile"
987
sed -e "s|LOCALINSTALLATION|$local|" \
988
-e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
989
-e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
990
-e "s|COQSRCDIRECTORY|$COQSRC|" \
991
-e "s|COQVERSION|$VERSION|" \
992
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
993
-e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
994
-e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \
995
-e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
996
-e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
997
-e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
998
-e "s|EMACSCOMMAND|$EMACS|" \
999
-e "s|COQDOCDIRECTORY|$ESCCOQDOCDIR|" \
1000
-e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
1001
-e "s|ARCHITECTURE|$ARCH|" \
1002
-e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
1003
-e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
1004
-e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
1005
-e "s|CAMLTAG|$CAMLTAG|" \
1006
-e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
1007
-e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
1008
-e "s|CAMLP4TOOL|$camlp4oexec|" \
1009
-e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
1010
-e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
1011
-e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
1012
-e "s|COQDEBUGFLAG|$coq_debug_flag|" \
1013
-e "s|COQPROFILEFLAG|$coq_profile_flag|" \
1014
-e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
1015
-e "s|CCOMPILEFLAGS|$cflags|" \
1016
-e "s|BESTCOMPILER|$best_compiler|" \
1017
-e "s|DLLEXTENSION|$DLLEXT|" \
1018
-e "s|EXECUTEEXTENSION|$EXE|" \
1019
-e "s|BYTECAMLC|$bytecamlc|" \
1020
-e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
1021
-e "s|NATIVECAMLC|$nativecamlc|" \
1022
-e "s|OCAMLEXEC|$ocamlexec|" \
1023
-e "s|OCAMLDEPEXEC|$ocamldepexec|" \
1024
-e "s|OCAMLDOCEXEC|$ocamldocexec|" \
1025
-e "s|OCAMLLEXEXEC|$ocamllexexec|" \
1026
-e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
1027
-e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
1028
-e "s|CCEXEC|$gcc_exec|" \
1029
-e "s|AREXEC|$ar_exec|" \
1030
-e "s|RANLIBEXEC|$ranlib_exec|" \
1031
-e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
1032
-e "s|FSETSOPT|$fsets|" \
1033
-e "s|REALSOPT|$reals|" \
1034
-e "s|COQIDEOPT|$COQIDE|" \
1035
-e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
1036
-e "s|WITHDOCOPT|$with_doc|" \
1037
-e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
1038
"$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
1040
chmod a-w "$COQSRC/config/Makefile"
1042
##################################################
1043
# Building the $COQTOP/dev/ocamldebug-coq file
1044
##################################################
1046
OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
1048
if test "$coq_debug_flag" = "-g" ; then
1049
rm -f $OCAMLDEBUGCOQ
1050
sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
1051
-e "s|COQLIBDIRECTORY|$LIBDIR|" \
1052
-e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
1053
-e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
1054
$OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
1055
chmod a-w,a+x $OCAMLDEBUGCOQ
1058
####################################################
1059
# Fixing lablgtk types (before/after 2.6.0)
1060
####################################################
1062
if [ ! "$COQIDE" = "no" ]; then
1063
if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
1064
if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
1065
cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
1067
cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
1070
cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
1074
##################################################
1076
####################################################
1078
echo "If anything in the above is wrong, please restart './configure'"
1080
echo "*Warning* To compile the system for a new architecture"
1081
echo " don't forget to do a 'make archclean' before './configure'."
1083
# $Id: configure 12219 2009-07-01 09:58:00Z notin $