Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 91 insertions, 45 deletions

diff --git a/Makefile b/Makefile
index 1dd4efca..86ff596a 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-