diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 54 |
1 files changed, 30 insertions, 24 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,7 +17,7 @@ # 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 @@ -87,7 +89,7 @@ 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 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) @@ -139,19 +141,10 @@ endif # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. -ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii -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)) @@ -159,9 +152,20 @@ 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' \ +remove them first, for instance via 'make clean' or 'make alienclean' \ (or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) endif endif @@ -196,7 +200,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean 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 @@ -231,8 +235,7 @@ 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 -rf doc/refman/html doc/stdlib/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 -f doc/common/version.tex @@ -244,7 +247,7 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(COQTOPEXE) $(CHICKEN) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f @@ -265,7 +268,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -delete cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg 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 timingclean @@ -282,6 +285,9 @@ devdocclean: rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + ########################################################################### # Continuous Intregration Tests ########################################################################### |