#!/bin/sh ################################## # # Configuration script for Coq # ################################## VERSION=8.4 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 # a local which command for sh which () { IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames) for i in $PATH; do if test -z "$i"; then i=.; fi if [ -f "$i/$1" ] ; then IFS=" " echo "$i/$1" break fi done } usage () { printf "Available options for configure are:\n" echo "-help" printf "\tDisplays this help page\n" echo "-prefix " printf "\tSet installation directory to \n" echo "-local" printf "\tSet installation directory to the current source tree\n" echo "-coqrunbyteflags" printf "\tSet link flags for VM-dependent bytecode (coqtop)\n" echo "-coqtoolsbyteflags" 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" printf "\tSpecifies the source directory\n" echo "-bindir" echo "-libdir" echo "-configdir" echo "-datadir" echo "-mandir" echo "-docdir" printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n" echo "-emacslib" echo "-emacs" printf "\tSpecifies where emacs files are to be installed\n" echo "-coqdocdir" printf "\tSpecifies where Coqdoc style files are to be installed\n" echo "-camldir" printf "\tSpecifies the path to the OCaml library\n" echo "-lablgtkdir" printf "\tSpecifies the path to the Lablgtk library\n" echo "-usecamlp5" printf "\tSpecifies to use camlp5 instead of camlp4\n" echo "-usecamlp4" printf "\tSpecifies to use camlp4 instead of camlp5\n" echo "-camlp5dir" printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n" echo "-arch" printf "\tSpecifies the architecture\n" echo "-opt" printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n" echo "-natdynlink (yes|no)" 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 " printf "\tUse 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 "-byte-only" printf "\tCompiles only bytecode version of Coq\n" echo "-debug" printf "\tAdd debugging information in the Coq executables\n" echo "-profile" printf "\tAdd profiling information in the Coq executables\n" echo "-annotate" printf "\tCompiles Coq with -dtypes option\n" echo "-makecmd " printf "\tName of GNU Make command.\n" } # Default OCaml binaries bytecamlc=ocamlc nativecamlc=ocamlopt ocamlmklibexec=ocamlmklib ocamlexec=ocaml ocamldepexec=ocamldep ocamldocexec=ocamldoc ocamllexexec=ocamllex ocamlyaccexec=ocamlyacc ocamlmktopexec=ocamlmktop camlp4oexec=camlp4o coq_debug_flag= coq_debug_flag_opt= coq_profile_flag= coq_annotate_flag= best_compiler=opt cflags="-fno-defer-pop -Wall -Wno-unused" natdynlink=yes local=false coqrunbyteflags_spec=no coqtoolsbyteflags_spec=no custom_spec=no 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 emacs_spec=no camldir_spec=no lablgtkdir_spec=no coqdocdir_spec=no arch_spec=no coqide_spec=no nomacintegration_spec=no browser_spec=no wwwcoq_spec=no with_geoproof=false with_doc=all with_doc_spec=no force_caml_version=no force_caml_version_spec=no usecamlp5=yes COQSRC=`pwd` # Parse command-line arguments while : ; do case "$1" in "") break;; -help|--help) usage exit;; -prefix|--prefix) prefix_spec=yes prefix="$2" shift;; -local|--local) local=true;; -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes coqrunbyteflags="$2" shift;; -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes coqtoolsbyteflags="$2" shift;; -custom|--custom) custom_spec=yes shift;; -src|--src) src_spec=yes COQSRC="$2" shift;; -bindir|--bindir) bindir_spec=yes bindir="$2" shift;; -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;; -docdir|--docdir) docdir_spec=yes docdir="$2" shift;; -emacslib|--emacslib) emacslib_spec=yes emacslib="$2" shift;; -emacs |--emacs) emacs_spec=yes emacs="$2" shift;; -coqdocdir|--coqdocdir) coqdocdir_spec=yes coqdocdir="$2" shift;; -camldir|--camldir) camldir_spec=yes camldir="$2" shift;; -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 arch=$2 shift;; -opt|--opt) bytecamlc=ocamlc.opt camlp4oexec=camlp4o # can't add .opt since dyn load'll be required nativecamlc=ocamlopt.opt;; -natdynlink|--natdynlink) case "$2" in yes) natdynlink=yes;; *) natdynlink=no esac shift;; -coqide|--coqide) coqide_spec=yes case "$2" in byte|opt) COQIDE=$2;; *) COQIDE=no esac shift;; -nomacintegration) nomacintegration_spec=yes shift;; -browser|--browser) browser_spec=yes BROWSER=$2 shift;; -coqwebsite|--coqwebsite) wwwcoq_spec=yes WWWCOQ=$2 shift;; -with-doc|--with-doc) with_doc_spec=yes case "$2" in yes|all) with_doc=all;; *) with_doc=no esac shift;; -with-geoproof|--with-geoproof) case "$2" in yes) with_geoproof=true;; no) with_geoproof=false;; esac 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;; -annotate|--annotate) coq_annotate_flag=-dtypes;; -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) force_caml_version_spec=yes force_caml_version=yes;; *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;; esac shift done if [ $prefix_spec = yes -a $local = true ] ; then echo "Options -prefix and -local are incompatible." echo "Configure script failed!" exit 1 fi # compile date DATEPGM=`which date` 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 +"%b %d %Y %H:%M:%S"`;; esac # Architecture case $arch_spec in no) # 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 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` else echo "I can not automatically find the name of your architecture." printf "%s"\ "Give me a name, please [win32 for Win95, Win98 or WinNT]: " read ARCH fi fi;; yes) ARCH=$arch esac # executable extension case $ARCH in win32) EXE=".exe" DLLEXT=".dll";; *) EXE="" DLLEXT=".so" esac # Is the source tree checked out from a recognised # version control system ? if test -e .svn/entries ; then checkedout=svn elif [ -d '{arch}' ]; then checkedout=gnuarch elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then checkedout=git else checkedout=0 fi # make command MAKE=`which ${makecmd:-make}` if [ "$MAKE" != "" ]; then MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; 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 fi if [ $OK = "no" ]; then echo "GNU Make >= 3.81 is needed." echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz" echo "then locally installed on a Unix-style system by issuing:" echo " tar xzvf make-3.81.tar.gz" echo " cd make-3.81" echo " ./configure" echo " make" echo " mv make .." echo " cd .." echo "Restart then the configure script and later use ./make instead of make." exit 1 else echo "You have locally installed GNU Make 3.81. Good!" fi fi else echo "Cannot find GNU Make >= 3.81." fi # Browser command if [ "$browser_spec" = "no" ]; then case $ARCH in win32) BROWSER='start %s' ;; Darwin) BROWSER='open %s' ;; *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;; esac fi if [ "$wwwcoq_spec" = "no" ]; then WWWCOQ="http://coq.inria.fr/" fi ######################################### # Objective Caml programs case $camldir_spec in no) CAMLC=`which $bytecamlc` case "$CAMLC" in "") echo "$bytecamlc is not present in your path!" echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: " read CAMLC case "$CAMLC" in "") CAMLC=/usr/local/bin/$bytecamlc;; */ocamlc|*/ocamlc.opt) true;; */) CAMLC="${CAMLC}"$bytecamlc;; *) CAMLC="${CAMLC}"/$bytecamlc;; esac esac CAMLBIN=`dirname "$CAMLC"`;; yes) CAMLC=$camldir/$bytecamlc CAMLBIN=`dirname "$CAMLC"` bytecamlc="$CAMLC" nativecamlc=$CAMLBIN/$nativecamlc ocamlexec=$CAMLBIN/ocaml ocamldepexec=$CAMLBIN/ocamldep ocamldocexec=$CAMLBIN/ocamldoc ocamllexexec=$CAMLBIN/ocamllex ocamlyaccexec=$CAMLBIN/ocamlyacc ocamlmktopexec=$CAMLBIN/ocamlmktop ocamlmklibexec=$CAMLBIN/ocamlmklib camlp4oexec=$CAMLBIN/camlp4o esac if test ! -f "$CAMLC" ; then echo "I can not find the executable '$CAMLC'. Have you installed it?" echo "Configuration script failed!" exit 1 fi # 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 # 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.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.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!";; *) echo "I found the Objective-Caml compiler but cannot find its version number!" echo "Is it installed properly?" echo "Configuration script failed!" exit 1;; esac CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` # For coqmktop & bytecode compiler if [ "$coq_debug_flag" = "-g" ]; then case $CAMLTAG in OCAML31*|OCAML4*) # Compilation debug flag coq_debug_flag_opt="-g" ;; esac fi # Native dynlink if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then HASNATDYNLINK=true else HASNATDYNLINK=false fi 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 #May just be a 32 vs 64 problem for all 10.6.* true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 NATDYNLINKFLAG=os5fixme;; true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 NATDYNLINKFLAG=os5fixme;; true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 NATDYNLINKFLAG=os5fixme;; true,Darwin,10.*,3.11.*) if [ `getconf LONG_BIT` = "32" ]; then # Still a problem for x86_32 NATDYNLINKFLAG=os5fixme else # Not a problem for x86_64 NATDYNLINKFLAG=$HASNATDYNLINK fi;; *) NATDYNLINKFLAG=$HASNATDYNLINK;; esac # Camlp4 / Camlp5 configuration # 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 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 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 esac # 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 if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then echo "No Camlp4 installation found." echo "Configuration script failed!" exit 1 fi 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 [ ! -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!" fi else best_compiler=byte echo "You have only bytecode compilation." fi fi # OS dependent libraries OSDEPLIBS="-cclib -lunix" case $ARCH,$CYGWIN in sun4*) OS=`uname -r` case $OS in 5*) OS="Sun Solaris $OS" OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";; *) OS="Sun OS $OS" esac;; win32,yes) OS="Win32 (Cygwin)" cflags="-mno-cygwin $cflags";; win32,*) OS="Win32 (MinGW)";; 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 coqide_spec=yes COQIDE=byte fi # Which coqide is asked ? which one is possible ? if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then echo "CoqIde disabled as requested." else case $lablgtkdir_spec in no) if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then lablgtkdir_spec=yes elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then lablgtkdir=${CAMLLIB}/lablgtk2 fi;; yes) if [ ! -f "$lablgtkdir/glib.mli" ]; then echo "Incorrect LablGtk2 library (glib.mli not found)." echo "Configuration script failed!" exit 1 fi;; esac if [ "$lablgtkdir" = "" ]; then 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." COQIDE=no; elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then echo "LablGtk2 found, 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." COQIDE=byte else echo "LablGtk2 found, native threads: native CoqIde will be available." COQIDE=opt if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration; then cflags=$cflags" `pkg-config --cflags gtk-mac-integration`" IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"' IDEARCHFILE=ide/ide_mac_stubs.o 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="";; esac # strip command case $ARCH in Darwin) if [ "$HASNATDYNLINK" = "true" ] then STRIPCOMMAND="true" else STRIPCOMMAND="strip" fi;; *) if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] then STRIPCOMMAND="true" else STRIPCOMMAND="strip" fi esac ### Test if documentation can be compiled (latex, hevea) if test "$with_doc" = "all" then for cmd in "latex" "hevea" ; do if test ! -x "`which $cmd`" then echo "$cmd was not found; documentation will not be available" with_doc=no break fi done fi ########################################### # bindir, libdir, mandir, docdir, etc. # OCaml only understand Windows filenames (C:\...) case $ARCH in win32) COQSRC=`mk_win_path "$COQSRC"` CAMLBIN=`mk_win_path "$CAMLBIN"` CAMLP4BIN=`mk_win_path "$CAMLP4BIN"` esac case $src_spec in no) COQTOP=${COQSRC} 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";; *) bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq 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;; esac emacs_def=emacs 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 [%s]? " "$bindir_def" read BINDIR case $BINDIR in "") BINDIR=$bindir_def;; *) true;; esac;; 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 [%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/share/man ;; */*/true) MANDIR=$COQTOP/man ;; *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def" read MANDIR case $MANDIR in "") MANDIR=$mandir_def;; *) true;; esac;; esac 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 [%s]? " "$docdir_def" read DOCDIR case $DOCDIR in "") DOCDIR=$docdir_def;; *) true;; esac;; esac case $emacslib_spec/$prefix_spec/$local in yes/*/*) EMACSLIB=$emacslib;; */yes/*) case $ARCH in win32) EMACSLIB=$prefix/emacs ;; *) EMACSLIB=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) EMACSLIB=$COQTOP/tools/emacs ;; *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def" read EMACSLIB case $EMACSLIB in "") EMACSLIB=$emacslib_def;; *) true;; esac;; esac case $coqdocdir_spec/$prefix_spec/$local in yes/*/*) COQDOCDIR=$coqdocdir;; */yes/*) case $ARCH in win32) COQDOCDIR=$prefix/latex ;; *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def" read COQDOCDIR case $COQDOCDIR in "") COQDOCDIR=$coqdocdir_def;; *) true;; esac;; esac # Determine if we enable -custom by default (Windows and MacOS) CUSTOM_OS=no if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then CUSTOM_OS=yes fi BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!" case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";; */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";; */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";; *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'" BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";; esac case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";; *) COQTOOLSBYTEFLAGS="";; esac # case $emacs_spec in # no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def" # read EMACS # case $EMACS in # "") EMACS="$emacs_def";; # *) true;; # esac;; # yes) EMACS="$emacs";; # esac ########################################### # Summary of the configuration echo "" echo " Coq top directory : $COQTOP" echo " Architecture : $ARCH" if test ! -z "$OS" ; then echo " Operating system : $OS" fi echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS" echo " Coq tools bytecode link flags : $COQTOOLSBYTEFLAGS" echo " OS dependent libraries : $OSDEPLIBS" echo " Objective-Caml/Camlp4 version : $CAMLVERSION" echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN" echo " Objective-Caml library in : $CAMLLIB" echo " Camlp4 library in : $CAMLP4LIB" if test "$best_compiler" = opt ; then echo " Native dynamic link support : $HASNATDYNLINK" 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 echo " Documentation : None" fi echo " CoqIde : $COQIDE" echo " Web browser : $BROWSER" echo " Coq web site : $WWWCOQ" 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" echo "" ################################################## # Building the $COQTOP/dev/ocamldebug-coq file ################################################## OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq if test "$coq_debug_flag" = "-g" ; then rm -f $OCAMLDEBUGCOQ sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ chmod a-w,a+x $OCAMLDEBUGCOQ fi #################################################### # Fixing lablgtk types (before/after 2.6.0) #################################################### if [ ! "$COQIDE" = "no" ]; then if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli else cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli fi else cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli fi fi ############################################## # Creation of configuration files ############################################## mlconfig_file="$COQSRC/config/coq_config.ml" config_file="$COQSRC/config/Makefile" config_template="$COQSRC/config/Makefile.template" ### Warning !! ### After this line, be careful when using variables, ### since some of them (e.g. $COQSRC) will be escaped escape_string () { "$ocamlexec" "tools/escape_string.ml" "$1" } # Escaped version of browser command BROWSER=`escape_string "$BROWSER"` # Under Windows, we now escape the backslashes that will ends in # ocaml strings (coq_config.ml) or in Makefile variables. case $ARCH in win32) 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 ##################################################### rm -f "$mlconfig_file" cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) let local = $local let coqrunbyteflags = "$COQRUNBYTEFLAGS" let coqlib = $LIBDIR_OPTION let configdir = $CONFIGDIR_OPTION let datadir = $DATADIR_OPTION let docdir = "$DOCDIR" let ocaml = "$ocamlexec" let ocamlc = "$bytecamlc" let ocamlopt = "$nativecamlc" let ocamlmklib = "$ocamlmklibexec" let ocamldep = "$ocamldepexec" let ocamldoc = "$ocamldocexec" let ocamlyacc = "$ocamlyaccexec" let ocamllex = "$ocamllexexec" let camlbin = "$CAMLBIN" let camllib = "$CAMLLIB" let camlp4 = "$CAMLP4" let camlp4o = "$camlp4oexec" let camlp4bin = "$CAMLP4BIN" let camlp4lib = "$CAMLP4LIB" let camlp4compat = "$CAMLP4COMPAT" let coqideincl = "$LABLGTKINCLUDES" 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" let version = "$VERSION" let caml_version = "$CAMLVERSION" let date = "$DATE" let compile_date = "$COMPILEDATE" let vo_magic_number = $VOMAGIC let state_magic_number = $STATEMAGIC let exec_extension = "$EXE" let with_geoproof = ref $with_geoproof let browser = "$BROWSER" let wwwcoq = "$WWWCOQ" let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/" let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/" let localwwwrefman = "file:/" ^ docdir ^ "html/refman" 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 * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file") } echo "let theories_dirs = [" >> "$mlconfig_file" subdirs theories echo "]" >> "$mlconfig_file" echo "let plugins_dirs = [" >> "$mlconfig_file" subdirs plugins echo "]" >> "$mlconfig_file" chmod a-w "$mlconfig_file" ############################################### # Building the $COQTOP/config/Makefile file ############################################### rm -f "$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" ################################################## # The end #################################################### echo "If anything in the above is wrong, please restart './configure'." echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'."