diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 136 |
1 files changed, 91 insertions, 45 deletions
@@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-osay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## # Makefile for Coq @@ -15,9 +17,9 @@ # 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/ +# http://aegis.sourceforge.net/auug97.pdf # 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. @@ -42,9 +44,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 \ @@ -52,27 +54,31 @@ FIND_VCS_CLAUSE:='(' \ -name '.bzr' -o \ -name 'debian' -o \ -name "$${GIT_DIR}" -o \ - -name '_build' \ + -name '_build' -o \ + -name '_build_ci' -o \ + -name '_install_ci' -o \ + -name 'user-contrib' -o \ + -name 'coq-makefile' -o \ + -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') +export MERLINFILES := $(call find, '.merlin') # 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 @@ -84,10 +90,9 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) # NB: all files in $(GENFILES) can be created initially, while # .ml files in $(GENML4FILES) might need some intermediate building. @@ -95,11 +100,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) ## 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 @@ -113,16 +114,19 @@ NOARG: world .PHONY: NOARG help noconfig submake help: - @echo "Please use either" + @echo "Please use either:" @echo " ./configure" @echo " make world" @echo " make install" @echo " make clean" @echo "or make archclean" - @echo @echo "For make to be verbose, add VERBOSE=1" + @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo - @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" + @echo "Bytecode compilation is now a separate target:" + @echo " make byte" + @echo " make install-byte" + @echo "Please do not mix bytecode and native targets in the same make -j" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES @@ -134,6 +138,40 @@ 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. + +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) + +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)) + +ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii +ifndef ACCEPT_ALIEN_VO +ifdef ALIENVO +$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ +remove them first, for instance via 'make voclean' or 'make alienclean' \ +(or skip this check via 'make ACCEPT_ALIEN_VO=1')) +endif +endif + +ifndef ACCEPT_ALIEN_OBJ +ifdef ALIENOBJS +$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ +remove them first, for instance via 'make clean' or 'make alienclean' \ +(or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) +endif +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. @@ -163,7 +201,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean clean: objclean cruftclean depclean docclean devdocclean @@ -185,6 +223,7 @@ indepclean: rm -f test-suite/check.log rm -f glob.dump rm -f config/revision.ml revision + rm -f plugins/micromega/.micromega.ml.generated $(MAKE) -C test-suite clean docclean: @@ -197,22 +236,19 @@ docclean: doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t - rm -f doc/faq/axioms.png - 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 + rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html rm -f doc/common/version.tex - rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex + rm -rf doc/sphinx/_build archclean: clean-ide optclean voclean rm -rf _build rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(COQTOPEXE) $(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) @@ -225,26 +261,37 @@ 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 cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist -distclean: clean cleanconfig cacheclean +distclean: clean cleanconfig cacheclean timingclean voclean: find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete find theories plugins test-suite -name .coq-native -empty -delete +timingclean: + find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -delete + devdocclean: 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)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + +########################################################################### +# Continuous Intregration Tests +########################################################################### +include Makefile.ci + ########################################################################### # Emacs tags ########################################################################### @@ -288,4 +335,3 @@ printenv: @env | wc -L @echo -n "Total (win32 limit is 32k) : " @env | wc -m - |