From d4cebff2033b0f68162feaa118cb5e43a9277fe1 Mon Sep 17 00:00:00 2001 From: glondu Date: Wed, 11 Feb 2009 12:46:19 +0000 Subject: Add -coqtoolsbyteflags and -custom to ./configure... ...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 7 ++++--- INSTALL | 2 +- Makefile.build | 14 +++++++------- config/Makefile.template | 1 + configure | 40 ++++++++++++++++++++++++++++++++++------ 5 files changed, 47 insertions(+), 17 deletions(-) diff --git a/CHANGES b/CHANGES index 1ccda6344f..d1a8e41bd1 100644 --- a/CHANGES +++ b/CHANGES @@ -491,9 +491,10 @@ Miscellaneous "Test Printing Let for ref" and "Test Printing If for ref". - An overhauled build system (new Makefiles); see dev/doc/build-system.txt. - Add -browser option to configure script. -- Build a shared library for the C part of Coq, and use it by default. - Bytecode executables are now pure. The behaviour is configurable with - the -coqrunbyteflags configure option. +- Build a shared library for the C part of Coq, and use it by default on + non-(Windows or MacOS) systems. Bytecode executables are now pure. The + behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and + -custom configure options. - Complexity tests can be skipped by setting the environment variable COQTEST_SKIPCOMPLEXITY. diff --git a/INSTALL b/INSTALL index b9b7a6194f..00feb16812 100644 --- a/INSTALL +++ b/INSTALL @@ -344,6 +344,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. where is the directory where the dllcoqrun.so is installed; - (not recommended) compile bytecode executables with a custom OCaml runtime by using: - ./configure -coqrunbyteflags -custom ... + ./configure -custom ... be aware that stripping executables generated this way, or performing other executable-specific operations, will make them useless. diff --git a/Makefile.build b/Makefile.build index a7442c457f..c95c053df5 100644 --- a/Makefile.build +++ b/Makefile.build @@ -200,7 +200,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -593,27 +593,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS) $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^ $(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^ $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^ $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^ $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $^ ########################################################################### # Installation diff --git a/config/Makefile.template b/config/Makefile.template index 35e2a2d7d9..6f9fac3c1d 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION # Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun") COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS +COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS BUILDLDPATH= # Paths for true installation diff --git a/configure b/configure index ec6eab64b9..037e9f73ba 100755 --- a/configure +++ b/configure @@ -36,7 +36,11 @@ usage () { echo "-local" printf "\tSet installation directory to the current source tree\n" echo "-coqrunbyteflags" - printf "\tSet link flags for VM-dependent bytecode\n" + 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" @@ -114,6 +118,8 @@ ranlib_exec=ranlib local=false coqrunbyteflags_spec=no +coqtoolsbyteflags_spec=no +custom_spec=no src_spec=no prefix_spec=no bindir_spec=no @@ -150,6 +156,11 @@ while : ; do -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;; @@ -780,12 +791,25 @@ case $coqdocdir_spec/$prefix_spec/$local in esac;; esac +# Determine if we enable -custom by default (Windows and MacOS) +CUSTOM_OS=no +if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then + CUSTOM_OS=yes +fi + BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!" -case $coqrunbyteflags_spec/$local in - yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";; - */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";; - *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR" - BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";; +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 @@ -809,6 +833,7 @@ 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" @@ -877,6 +902,7 @@ case $ARCH in ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'` ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'` ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` + ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'` ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'` ;; *) @@ -895,6 +921,7 @@ case $ARCH in ESCCAMLP4LIB="$CAMLP4LIB" ESCLABLGTKINCLUDES="$LABLGTKINCLUDES" ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS" + ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS" ESCBUILDLDPATH="$BUILDLDPATH" ;; esac @@ -954,6 +981,7 @@ rm -f "$COQSRC/config/Makefile" sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \ + -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \ -e "s|COQSRCDIRECTORY|$COQSRC|" \ -e "s|COQVERSION|$VERSION|" \ -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ -- cgit v1.2.3