Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 63 insertions, 45 deletions

diff --git a/Makefile.common b/Makefile.common
index 49fe1fd9..1e63d52f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -1,10 +1,12 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \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)         ##
+##########################################################################
 
 -include config/Makefile
 
@@ -12,8 +14,6 @@
 # Executables
 ###########################################################################
 
-COQMKTOP:=bin/coqmktop$(EXE) 
-
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
 
@@ -25,9 +25,15 @@ COQWC:=bin/coqwc$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
 COQC:=bin/coqc$(EXE)
 COQWORKMGR:=bin/coqworkmgr$(EXE)
+COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
+COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
+COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
+COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
 
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
 	$(COQWORKMGR)
+TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
+	$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
 
 COQDEPBOOT:=bin/coqdep_boot$(EXE)
 OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
@@ -41,28 +47,44 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 # Object and Source files
 ###########################################################################
 
-ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
-  DEPNATDYN:=
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ # static link of plugins, do not mention them in .v.d
+ DYNDEP:=-dyndep no
+else
+ DYNDEP:=-dyndep var
+endif
+
+# Which coqtop do we use to build .vo file ? The best ;-)
+# Note: $(BEST) could be overridden by the user if a byte build is desired
+# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions
+# for Declare ML Module files.
+
+ifeq ($(BEST),opt)
+COQTOPBEST:=$(COQTOPEXE)
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
 else
-  DEPNATDYN:=-natdynlink no
+COQTOPBEST:=$(COQTOPBYTE)
+DYNOBJ:=.cmo
+DYNLIB:=.cma
 endif
 
 INSTALLBIN:=install
-INSTALLLIB:=install -m 644 
+INSTALLLIB:=install -m 644
 INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 CORESRCDIRS:=\
-  config 	lib		kernel		kernel/byterun	library \
-  proofs 	tactics 	pretyping	interp		stm \
-  toplevel	parsing 	printing	intf	engine	ltac
+  config 	clib 		lib		kernel	intf	kernel/byterun	library \
+  engine 	pretyping	interp	proofs	parsing 	printing \
+  tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
-  rtauto 	nsatz           syntax          decl_mode	btauto \
-  ssrmatching
+  rtauto 	nsatz           syntax          btauto \
+  ssrmatching	ltac		ssr
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
@@ -77,18 +99,17 @@ BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
-# Beware that highparsing.cma should appear before ltac.cma
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
+CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
-        parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
-	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
+        parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
+	stm/stm.cma toplevel/toplevel.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
-GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma
+GRAMMARCMA:=grammar/grammar.cma
 
 # modules known by the toplevel of Coq
 
@@ -114,20 +135,21 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
 NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
 OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         z_syntax_plugin.cmo \
-        numbers_syntax_plugin.cmo \
         r_syntax_plugin.cmo \
+	int31_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
         string_syntax_plugin.cmo )
-DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
 DERIVECMO:=plugins/derive/derive_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
+SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
-PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
+PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
         $(QUOTECMO) $(RINGCMO) \
         $(FOURIERCMO) $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
@@ -145,16 +167,10 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 # vo files
 ###########################################################################
 
-## we now retrieve the names of .vo file to compile in */vo.itarget files
-
-THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \
-                $(addprefix $(dir $(f)),$(shell cat $(f))))
-
-PLUGINSVO:=  $(foreach f, $(wildcard plugins/*/vo.itarget), \
-                $(addprefix $(dir $(f)),$(shell cat $(f))))
-
-ALLVO:= $(THEORIESVO) $(PLUGINSVO)
-VFILES:= $(ALLVO:.vo=.v)
+THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
+ALLVO := $(THEORIESVO) $(PLUGINSVO)
+VFILES := $(ALLVO:.vo=.v)
 
 ## More specific targets
 
@@ -176,13 +192,15 @@ vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theo
 
 vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
 
-LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \
-	    $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \
-	    $(call vo_to_obj,$(PLUGINSVO)) \
-	    $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \
-	    $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob)
+GLOBFILES:=$(ALLVO:.vo=.glob)
+ifdef NATIVECOMPUTE
+NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
+else
+NATIVEFILES :=
+endif
+LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
+# For emacs:
+# Local Variables:
+# mode: makefile
 # End: