diff options
-rw-r--r-- | CHANGES | 7 | ||||
-rw-r--r-- | INSTALL | 2 | ||||
-rw-r--r-- | Makefile.build | 14 | ||||
-rw-r--r-- | config/Makefile.template | 1 | ||||
-rwxr-xr-x | configure | 40 |
5 files changed, 47 insertions, 17 deletions
@@ -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. @@ -344,6 +344,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. where <path> 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 a7442c457..c95c053df 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 35e2a2d7d..6f9fac3c1 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 @@ -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|" \ |