summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /Makefile
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile249
1 files changed, 114 insertions, 135 deletions
diff --git a/Makefile b/Makefile
index 97afdfd6..bb5ec3bc 100644
--- a/Makefile
+++ b/Makefile
@@ -6,69 +6,46 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 14090 2011-05-03 13:34:16Z pboutill $
-
# Makefile for Coq
#
-# To be used with GNU Make.
+# To be used with GNU Make >= 3.81.
#
-# This is the only Makefile. You won't find Makefiles in sub-directories
-# and this is done on purpose. If you are not yet convinced of the advantages
-# of a single Makefile, please read
+# This Makefile is now separated into Makefile.{common,build,doc}.
+# You won't find Makefiles in sub-directories and this is done on purpose.
+# If you are not yet convinced of the advantages of a single Makefile, please
+# read
# http://miller.emu.id.au/pmiller/books/rmch/
# before complaining.
#
# When you are working in a subdir, you can compile without moving to the
# upper directory using "make -C ..", and the output is still understood
# by Emacs' next-error.
-###########################################################################
-
-
-# Specific command-line options to this Makefile
#
-# make GOTO_STAGE=N # perform only stage N (with N=1,2)
+# Specific command-line options to this Makefile:
+#
# make VERBOSE=1 # restore the raw echoing of commands
# make NO_RECALC_DEPS=1 # avoid recomputing dependencies
# make NO_RECOMPILE_LIB=1 # a coqtop rebuild does not trigger a stdlib rebuild
#
# Nota: the 1 above can be replaced by any non-empty value
-# More details in dev/doc/build-system*.txt
+#
+# ----------------------------------------------------------------------
+# See dev/doc/build-system*.txt for more details/FAQ about this Makefile
+# ----------------------------------------------------------------------
-# FAQ: special features used in this Makefile
-#
-# * Order-only dependencies: |
-#
-# Dependencies placed after a bar (|) should be built before
-# the current rule, but having one of them is out-of-date do not
-# trigger a rebuild of the current rule.
-# See http://www.gnu.org/software/make/manual/make.html#Prerequisite-Types
-#
-# * Annotation before commands: +/-/@
-#
-# a command starting by - is always successful (errors are ignored)
-# a command starting by + is runned even if option -n is given to make
-# a command starting by @ is not echoed before being runned
-#
-# * Custom functions
-#
-# Definition via "define foo" followed by commands (arg is $(1) etc)
-# Call via "$(call foo,arg1)"
-#
-# * Useful builtin functions
-#
-# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...)
-#
-# * Behavior of -include
-#
-# If the file given to -include doesn't exist, make tries to build it,
-# but doesn't care if this build fails. This can be quite surprising,
-# see in particular the -include in Makefile.stage*
+###########################################################################
+# File lists
+###########################################################################
+
+# NB: due to limitations in Win32, please refrain using 'export' too much
+# to communicate between make sub-calls (in Win32, 8kb max per env variable,
+# 32kb total)
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
-export FIND_VCS_CLAUSE:='(' \
+FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
-name '_darcs' -o \
@@ -78,41 +55,60 @@ export FIND_VCS_CLAUSE:='(' \
-name "$${GIT_DIR}" -o \
-name '_build' \
')' -prune -o
-export PRUNE_CHECKER := -wholename ./checker/\* -prune -o
-FIND_PRINTF_P:=-print | sed 's|^\./||'
+define find
+ $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
+endef
+
+## Files in the source tree
+
+YACCFILES:=$(call find, '*.mly')
+LEXFILES := $(call find, '*.mll')
+export MLLIBFILES := $(call find, '*.mllib')
+export ML4FILES := $(call find, '*.ml4')
+export CFILES := $(call find, '*.c')
+
+# NB: The lists of currently existing .ml and .mli files will change
+# before and after a build or a make clean. Hence we do not export
+# these variables, but cleaned-up versions (see below MLFILES and co)
+
+EXISTINGML := $(call find, '*.ml')
+EXISTINGMLI := $(call find, '*.mli')
-export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P))
-export LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P))
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+## Files that will be generated
+
+GENML4FILES:= $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
scripts/tolink.ml kernel/copcodes.ml
-export GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
-export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \
- while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \
- $(GENMLFILES)
-export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
- $(GENMLIFILES)
-export MLLIBFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mllib' ')' $(FIND_PRINTF_P))
-export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-#export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \
-# $(GENVFILES)
-export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) '(' -name '*.c' ')' -print)
-
-export ML4FILESML:= $(ML4FILES:.ml4=.ml)
-
-# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior
-MAKEFLGS:=--warn-undefined-variable --no-builtin-rules
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
+
+# NB: all files in $(GENFILES) can be created initially, while
+# .ml files in $(GENML4FILES) might need some intermediate building.
+# That's why we keep $(GENML4FILES) out of $(GENFILES)
+
+## More complex file lists
+
+define diff
+ $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
+endef
+
+export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
+export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
include Makefile.common
-NOARG: world
+###########################################################################
+# Starting rules
+###########################################################################
-.PHONY: NOARG help always tags otags
+NOARG: world
-always: ;
+.PHONY: NOARG help always
help:
@echo "Please use either"
@@ -124,76 +120,44 @@ help:
@echo
@echo "For make to be verbose, add VERBOSE=1"
-ifdef COQ_CONFIGURED
-define stage-template
- @echo '*****************************************************'
- @echo '*****************************************************'
- @echo '****************** Entering stage$(1) ******************'
- @echo '*****************************************************'
- @echo '*****************************************************'
- +$(MAKE) $(MAKEFLGS) -f Makefile.stage$(1) "$@"
-endef
-else
-define stage-template
- @echo "Please run ./configure first" >&2; exit 1
-endef
-endif
-
-UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.mli' -o -name '.\#*.ml4')
+UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
ifdef UNSAVED_FILES
-$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; cancel them or save before proceeding. \
-Or your editor crashed. Then, you may want to consider whether you want to restore the autosaves)
+$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \
+cancel them or save before proceeding. Or your editor crashed. \
+Then, you may want to consider whether you want to restore the autosaves)
#If you try to simply remove this explicit test, the compilation may
#fail later. In particular, if a .#*.v file exists, coqdep fails to
#run.
endif
-ifdef GOTO_STAGE
-config/Makefile Makefile.common Makefile.build Makefile: ;
+# Apart from clean and tags, everything will be done in a sub-call to make
+# on Makefile.build. This way, we avoid doing here the -include of .d :
+# since they trigger some compilations, we do not want them for a mere clean
-%: always
- $(call stage-template,$(GOTO_STAGE))
+ifdef COQ_CONFIGURED
+%:: always
+ $(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@"
else
-
-.PHONY: stage1 stage2 world revision
-
-stage1 $(STAGE1_TARGETS) : always
- $(call stage-template,1)
-
-ifneq (,$(STAGE1_IMPLICITS))
-$(STAGE1_IMPLICITS) : always
- $(call stage-template,1)
-endif
-
-stage2 $(STAGE2_TARGETS) : stage1
- $(call stage-template,2)
-
-ifneq (,$(STAGE2_IMPLICITS))
-$(STAGE2_IMPLICITS) : stage1
- $(call stage-template,2)
+%:: always
+ @echo "Please run ./configure first" >&2; exit 1
endif
-# Nota:
-# - world is one of the targets in $(STAGE2_TARGETS), hence launching
-# "make" or "make world" leads to recursion into stage1 then stage2
-# - the aim of stage1 is to build grammar.cma and q_constr.cmo
-# More details in dev/doc/build-system*.txt
-
+always : ;
-# This is to remove the built-in rule "%: %.o" :
-%: %.o
-# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
+# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
-endif #GOTO_STAGE
+Makefile Makefile.build Makefile.common config/Makefile : ;
###########################################################################
# Cleaning
###########################################################################
-.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean doclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
clean: objclean cruftclean depclean docclean devdocclean
+cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean
+
objclean: archclean indepclean
cruftclean: ml4clean
@@ -202,10 +166,8 @@ cruftclean: ml4clean
indepclean:
rm -f $(GENFILES)
- rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
+ rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) bin/fake_ide
find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
- find . -name '*_mod.ml' | xargs rm -f
- find plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
rm -f */*.pp[iox] plugins/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -221,9 +183,9 @@ docclean:
doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \
doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html
rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \
- doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \
- doc/stdlib/library.files.ls
- rm -f doc/*/*.ps doc/*/*.pdf
+ doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
+ doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
+ rm -f doc/*/*.ps doc/*/*.pdf
rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
rm -f doc/refman/euclid.ml doc/refman/euclid.mli
rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
@@ -232,22 +194,24 @@ docclean:
rm -f doc/coq.tex
rm -f doc/refman/styles.hva doc/refman/cover.html
-archclean: clean-ide cleantheories
+archclean: clean-ide optclean voclean
+ rm -rf _build myocamlbuild_config.ml
+ rm -f $(ALLSTDLIB).*
+
+optclean:
rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
- find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
rm -f $(TOOLS) $(CSDPCERT)
- rm -rf _build myocamlbuild_config.ml
+ find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
clean-ide:
rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
rm -f ide/input_method_lexer.ml
- rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
- rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
+ rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
rm -f ide/utf8_convert.ml
ml4clean:
- rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed)
+ rm -f $(GENML4FILES)
ml4depclean:
find . -name '*.ml4.d' | xargs rm -f
@@ -259,21 +223,25 @@ cleanconfig:
rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
distclean: clean cleanconfig
- $(MAKE) -C test-suite distclean
-cleantheories:
+voclean:
rm -f states/*.coq
- find theories -name '*.vo' -o -name '*.glob' | xargs rm -f
+ find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
devdocclean:
- find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \;
+ find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
+ rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc
+ rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
+ rm -f $(OCAMLDOCDIR)/html/*.html
###########################################################################
# Emacs tags
###########################################################################
+.PHONY: tags otags
+
tags:
- echo $(MLIFILES) $(MLFILES) $(ML4FILES) | sort -r | xargs \
+ echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
etags --language=none\
"--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -288,7 +256,7 @@ tags:
otags:
- echo $(MLIFILES) $(MLFILES) | sort -r | xargs otags
+ echo $(MLIFILES) $(MLSTATICFILES) | sort -r | xargs otags
echo $(ML4FILES) | sort -r | xargs \
etags --append --language=none\
"--regex=/let[ \t]+\([^ \t]+\)/\1/" \
@@ -309,3 +277,14 @@ ifdef COQ_CONFIGURED
else
@echo "Please run ./configure first" >&2; exit 1
endif
+
+# Useful to check that the exported variables are within the win32 limits
+
+printenv:
+ @env
+ @echo
+ @echo -n "Maxsize (win32 limit is 8k) : "
+ @env | wc -L
+ @echo -n "Total (win32 limit is 32k) : "
+ @env | wc -m
+