diff options
| -rw-r--r-- | Makefile | 52 | ||||
| -rw-r--r-- | config/Makefile.template | 15 | ||||
| -rwxr-xr-x | configure | 8 |
3 files changed, 43 insertions, 32 deletions
@@ -26,7 +26,9 @@ include config/Makefile -NOARG: +NOARG: world + +help: @echo "Please use either" @echo " ./configure" @echo " make world" @@ -36,6 +38,7 @@ NOARG: @echo @echo "For make to be verbose, add VERBOSE=1" + # build and install the three subsystems: coq, coqide, pcoq world: revision coq coqide pcoq @@ -1582,6 +1585,19 @@ parsing/lexer.cmo: parsing/lexer.ml4 $(SHOW)'OCAMLC4 $<' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< +# pretty printing of the revision number when compiling a checked out +# source tree +.PHONY: revision + +revision: +ifeq ($(CHECKEDOUT),1) + - /bin/rm -f revision + sed -ne '/url/s/^.*\/\([^\/]\+\)"$$/\1/p' .svn/entries > revision + sed -ne '/revision/s/^.*"\([0-9]\+\)".*$$/r\1/p' .svn/entries >> revision +endif + +archclean:: + /bin/rm -f revision ########################################################################### @@ -1661,22 +1677,22 @@ archclean:: clean:: archclean rm -f *~ */*~ */*/*~ rm -f gmon.out core - rm -f config/*.cm[ioa] - rm -f lib/*.cm[ioa] - rm -f kernel/*.cm[ioa] - rm -f library/*.cm[ioa] - rm -f proofs/*.cm[ioa] - rm -f tactics/*.cm[ioa] - rm -f interp/*.cm[ioa] - rm -f parsing/*.cm[ioa] parsing/*.ppo - rm -f pretyping/*.cm[ioa] - rm -f toplevel/*.cm[ioa] - rm -f ide/*.cm[ioa] - rm -f ide/utils/*.cm[ioa] - rm -f tools/*.cm[ioa] - rm -f tools/*/*.cm[ioa] - rm -f scripts/*.cm[ioa] - rm -f dev/*.cm[ioa] + rm -f config/*.cm[ioa] config/*.annot + rm -f lib/*.cm[ioa] lib/*.annot + rm -f kernel/*.cm[ioa] kernel/*.annot + rm -f library/*.cm[ioa] library/*.annot + rm -f proofs/*.cm[ioa] proofs/*.annot + rm -f tactics/*.cm[ioa] tactics/*.annot + rm -f interp/*.cm[ioa] interp/*.annot + rm -f parsing/*.cm[ioa] parsing/*.ppo parsing/*.annot + rm -f pretyping/*.cm[ioa] pretyping/*.annot + rm -f toplevel/*.cm[ioa] toplevel/*.annot + rm -f ide/*.cm[ioa] ide/*.annot + rm -f ide/utils/*.cm[ioa] ide/utils/*.annot + rm -f tools/*.cm[ioa] tools/*.annot + rm -f tools/*/*.cm[ioa] tools/*/*.annot + rm -f scripts/*.cm[ioa] scripts/*.annot + rm -f dev/*.cm[ioa] dev/*.annot rm -f */*.pp[iox] contrib/*/*.pp[iox] cleanconfig:: @@ -1760,7 +1776,5 @@ devel: clean:: find . -name "\.#*" -exec rm -f {} \; - find . -name "*~" -exec rm -f {} \; - find . -name "*.annot" -exec rm -f {} \; ########################################################################### diff --git a/config/Makefile.template b/config/Makefile.template index 5310aec94..a3465722f 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -61,6 +61,9 @@ CAMLLINK="BYTECAMLC" CAMLOPTLINK="NATIVECAMLC" CAMLMKTOP="CAMLMKTOPEXEC" +# Caml flags +CAMLFLAGS=CAMLANNOTATEFLAG + # Compilation debug flag CAMLDEBUG=COQDEBUGFLAG @@ -125,18 +128,6 @@ HASCOQIDE=COQIDEOPT # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE -.PHONY: revision - -revision: -ifeq ($(CHECKEDOUT),1) - - /bin/rm -f revision - sed -ne '/url/s/^.*\/\([^\/]\+\)"$$/\1/p' .svn/entries > revision - sed -ne '/revision/s/^.*"\([0-9]\+\)".*$$/r\1/p' .svn/entries >> revision -endif - -archclean:: - /bin/rm -f revision - # make or sed are bogus and believe lines not terminating by a return # are inexistent @@ -64,6 +64,8 @@ usage () { echo -e "\tAdd debugging information in the Coq executables\n" echo "-profile" echo -e "\tAdd profiling information in the Coq executables\n" + echo "-annotate" + echo -e "\tCompiles Coq with -dtypes option" } @@ -81,6 +83,7 @@ camlp4oexec=camlp4o coq_debug_flag= coq_profile_flag= +coq_annotate_flag= best_compiler=opt gcc_exec=gcc @@ -190,6 +193,7 @@ while : ; do -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;; *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;; esac shift @@ -279,7 +283,8 @@ case $camldir_spec in */) CAMLC="${CAMLC}"$bytecamlc;; *) CAMLC="${CAMLC}"/$bytecamlc;; esac - esac;; + esac + CAMLBIN=`dirname "$CAMLC"`;; yes) CAMLC=$camldir/$bytecamlc CAMLBIN=`dirname "$CAMLC"` @@ -694,6 +699,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ + -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \ -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ |