diff options
| -rw-r--r-- | Makefile | 60 | ||||
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.dev.txt | 20 |
3 files changed, 53 insertions, 29 deletions
@@ -42,9 +42,9 @@ # 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 !! -FIND_VCS_CLAUSE:='(' \ +# !! Before using FIND_SKIP_DIRS, please read how you should in the !! +# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! +FIND_SKIP_DIRS:='(' \ -name '{arch}' -o \ -name '.svn' -o \ -name '_darcs' -o \ @@ -55,25 +55,23 @@ FIND_VCS_CLAUSE:='(' \ -name '_build' -o \ -name '_build_ci' -o \ -name 'coq-makefile' -o \ - -name '.opamcache' \ + -name '.opamcache' -o \ + -name '.coq-native' \ ')' -prune -o define find - $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') + $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') endef define findindir - $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||') -endef - -define findx - $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||') + $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') endef ## Files in the source tree LEXFILES := $(call find, '*.mll') -export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') +export MLLIBFILES := $(call find, '*.mllib') +export MLPACKFILES := $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call findindir, 'kernel/byterun', '*.c') @@ -97,11 +95,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) ## More complex file lists -define diff - $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) -endef - -export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES)) +export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -139,6 +133,36 @@ Then, you may want to consider whether you want to restore the autosaves) #run. endif +# Check that every compiled file around has a known source file. +# This should help preventing weird compilation failures caused by leftover +# compiled files after deleting or moving some source files. + +ifndef ACCEPT_ALIEN_VO +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) +ifdef ALIENVO +$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ +remove them first, for instance via 'make voclean' \ +(or skip this check via 'make ACCEPT_ALIEN_VO=1')) +endif +endif + +ifndef ACCEPT_ALIEN_OBJ +EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ + $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) +KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ + $(MLIFILES:.mli=.cmi) \ + $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma +ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) +ifdef ALIENOBJS +$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ +remove them first, for instance via 'make clean' \ +(or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) +endif +endif + # 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. @@ -218,7 +242,7 @@ archclean: clean-ide optclean voclean optclean: rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) - find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f + find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f clean-ide: rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) @@ -231,7 +255,7 @@ ml4clean: rm -f $(GENML4FILES) depclean: - find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f + find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f cacheclean: find theories plugins test-suite -name '.*.aux' -delete diff --git a/Makefile.build b/Makefile.build index 0dafde997..ed1959cff 100644 --- a/Makefile.build +++ b/Makefile.build @@ -85,7 +85,7 @@ include Makefile.dev ## provides the 'printers' and 'revision' rules # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) -include $(DEPENDENCIES) diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index fefcb0937..f3fc13e96 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -74,25 +74,25 @@ The Makefile is separated in several files : - Makefile.doc : specific rules for compiling the documentation. -FIND_VCS_CLAUSE +FIND_SKIP_DIRS --------------- -The recommended style of using FIND_VCS_CLAUSE is for example +The recommended style of using FIND_SKIP_DIRS is for example - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print 1) The parentheses even in the one-criteria case is so that if one adds other conditions, e.g. change the first example to the second - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print one is not tempted to write - find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print + find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print -because this will not necessarily work as expected; $(FIND_VCS_CLAUSE) +because this will not necessarily work as expected; $(FIND_SKIP_DIRS) ends with an -or, and how it combines with what comes later depends on operator precedence and all that. Much safer to override it with parentheses. @@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why. You are used to write: find . -name '*.example' and it works fine. But the following will not: - find . $(FIND_VCS_CLAUSE) -name '*.example' -it will also list things directly matched by FIND_VCS_CLAUSE + find . $(FIND_SKIP_DIRS) -name '*.example' +it will also list things directly matched by FIND_SKIP_DIRS (directories we want to prune, in which we don't want to find anything). C'est subtil... Il y a effectivement un -print implicite à la fin, qui fait que la commande habituelle sans print fonctionne bien, mais dès que l'on introduit d'autres commandes dans le lot (le --prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de +-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de parenthèses du -print implicite par rapport au parenthésage dans la forme recommandée d'utilisation: |