Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 54 insertions, 104 deletions

diff --git a/Makefile.common b/Makefile.common
index 46bf2175..b560bae5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -1,4 +1,3 @@
-
 #######################################################################
 #  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
 # <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
@@ -17,20 +16,31 @@ COQMKTOPBYTE:=bin/coqmktop.byte$(EXE)
 COQMKTOPOPT:=bin/coqmktop.opt$(EXE)
 BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE)
 COQMKTOP:=bin/coqmktop$(EXE) 
+
 COQCBYTE:=bin/coqc.byte$(EXE)
 COQCOPT:=bin/coqc.opt$(EXE)
 BESTCOQC:=bin/coqc.$(BEST)$(EXE)
 COQC:=bin/coqc$(EXE)
+
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPOPT:=bin/coqtop.opt$(EXE)
 BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
+
 CHICKENBYTE:=bin/coqchk.byte$(EXE)
 CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
 
-ifneq ($(HASNATDYNLINK),false)
+FAKEIDE:=bin/fake_ide$(EXE)
+
+ifeq ($(CAMLP4),camlp4)
+CAMLP4MOD:=camlp4lib
+else
+CAMLP4MOD:=gramlib
+endif
+
+ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
   DYNLINKCMXA:=dynlink.cmxa
   NATDYNLINKDEF:=-DHasDynlink
   DEPNATDYN:=
@@ -50,26 +60,29 @@ COQIDEOPT:=bin/coqide.opt$(EXE)
 COQIDE:=bin/coqide$(EXE)
 
 ifeq ($(BEST),opt)
-COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
+OPT:=opt
 else
-COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE)              $(COQTOPEXE) $(CHICKENBYTE)               $(CHICKEN)
+OPT:=
 endif
-OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
+
+BESTOBJ:=$(if $(OPT),.cmx,.cmo)
+
+COQBINARIES:= $(COQMKTOP) $(COQC) \
+  $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \
+  $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN)
 
 CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
 SRCDIRS:=\
   config 	tools 		tools/coqdoc 	scripts		lib \
   kernel	kernel/byterun	library 	proofs 		tactics \
-  pretyping	interp		toplevel 	parsing 	ide/utils \
-  ide		\
+  pretyping	interp		toplevel/utils	toplevel 	parsing 	\
+  ide/utils	ide		\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring	dp \
     setoid_ring xml 		extraction 	fourier \
     cc 		funind 		firstorder 	field 		subtac \
-    rtauto 	nsatz           syntax)
+    rtauto 	nsatz           syntax          decl_mode)
 
 # Order is relevent here because kernel and checker contain files
 # with the same name
@@ -139,10 +152,6 @@ COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
 DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT)
 
-CLIBS:=unix.cma
-
-CAMLP4OBJS:=gramlib.cma
-
 CONFIG:=config/coq_config.cmo
 
 BYTERUN:=$(addprefix kernel/byterun/, \
@@ -158,6 +167,8 @@ CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \
         parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
         parsing/highparsing.cma tactics/hightactics.cma 
 
+GRAMMARCMA:=parsing/grammar.cma
+
 OMEGACMA:=plugins/omega/omega_plugin.cma
 ROMEGACMA:=plugins/romega/romega_plugin.cma
 MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
@@ -182,8 +193,9 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
         r_syntax_plugin.cma \
 	ascii_syntax_plugin.cma \
         string_syntax_plugin.cma )
+DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
 
-PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \
+PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
         $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
         $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
@@ -204,24 +216,21 @@ else
  PLUGINSOPT:=
 endif
 
-ifeq ($(BEST),opt)
-  INITPLUGINSBEST:=$(INITPLUGINSOPT)
-else
-  INITPLUGINSBEST:=$(INITPLUGINS)
-endif
-
-CMA:=$(CLIBS) $(CAMLP4OBJS)
-CMXA:=$(CMA:.cma=.cmxa)
+INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
 
 LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
+IDEDEPS:=$(CONFIG) lib/flags.cmo lib/xml_lexer.cmo lib/xml_parser.cmo \
+  lib/xml_utils.cmo toplevel/ide_intf.cmo
 IDECMA:=ide/ide.cma
 
+LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTDEPS) $(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
+
 # modules known by the toplevel of Coq
 
-OBJSMOD:=Coq_config \
- $(foreach lib,$(CORECMA),$(shell cat $(lib:.cma=.mllib)))
+OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib))
 
 IDEMOD:=$(shell cat ide/ide.mllib)
 
@@ -229,51 +238,25 @@ IDEMOD:=$(shell cat ide/ide.mllib)
 
 COQENVCMO:=$(CONFIG) \
   lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo \
-  lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/system.cmo \
+  lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \
   lib/envars.cmo
 
 COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
-COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 
 COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
-COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
 ## Misc
 
 CSDPCERTCMO:=$(addprefix plugins/micromega/, \
-  mutils.cmo 	micromega.cmo 	mfourier.cmo 	certificate.cmo \
+  mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
-CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
-
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
-COQDEPBOOTML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml
-COQDEPML:=tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep.ml
-
-COQDEPCMO:=$(COQENVCMO) $(COQDEPML:.ml=.cmo)
-COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx)
-
-GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
-GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
+COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
 
 COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
-COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
-
-# grammar modules with camlp4
-
-GRAMMARCMA:=parsing/grammar.cma
-
-GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
-  parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \
-  parsing/g_prim.ml4 parsing/g_tactic.ml4 \
-  parsing/g_ltac.ml4 parsing/g_constr.ml4 \
-  parsing/lexer.ml4 parsing/q_coqast.ml4
-
-STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4
-STAGE1:=parsing/grammar.cma parsing/q_constr.cmo
-
 
 ###########################################################################
 # vo files
@@ -291,10 +274,12 @@ STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures)
 ARITHVO:=$(call cat_vo_itarget, theories/Arith)
 SORTINGVO:=$(call cat_vo_itarget, theories/Sorting)
 BOOLVO:=$(call cat_vo_itarget, theories/Bool)
+PARITHVO:=$(call cat_vo_itarget, theories/PArith)
 NARITHVO:=$(call cat_vo_itarget, theories/NArith)
 ZARITHVO:=$(call cat_vo_itarget, theories/ZArith)
 QARITHVO:=$(call cat_vo_itarget, theories/QArith)
 LISTSVO:=$(call cat_vo_itarget, theories/Lists)
+VECTORSVO:=$(call cat_vo_itarget, theories/Vectors)
 STRINGSVO:=$(call cat_vo_itarget, theories/Strings)
 SETSVO:=$(call cat_vo_itarget, theories/Sets)
 FSETSVO:=$(call cat_vo_itarget, theories/FSets)
@@ -309,10 +294,11 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
 PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
 
 THEORIESVO:=\
-  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
+  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
   $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO)
+  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \
+  $(VECTORSVO)
 
 THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
 
@@ -341,6 +327,7 @@ PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
+ALLSTDLIB := test-suite/misc/universes/all_stdlib
 
 # convert a (stdlib) filename into a module name:
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
@@ -351,7 +338,6 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO))
 LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
-
 ###########################################################################
 # Miscellaneous
 ###########################################################################
@@ -363,56 +349,20 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 
 DATE=$(shell LANG=C date +"%B %Y")
 
-SOURCEDOCDIR=dev/source-doc
-
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
-
-### Targets forwarded by Makefile to a specific stage:
-
-## Enumeration of targets that require being done at stage1
-
-STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
-  $(GENFILES) \
-  source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
-
-STAGE1_IMPLICITS:=
-
-ifdef CM_STAGE1
- STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
-endif
-
-## Enumeration of targets that require being done at stage2
-
-VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
-  fsets relations wellfounded ints reals \
-  setoids sorting natural integer rational numbers noreal \
-  omega micromega ring setoid_ring dp xml extraction field fourier \
-  funind cc subtac rtauto
-
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \
-  rectutorial refman-quick refman-nodep stdlib-nodep \
-  install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url \
-  ide/index_urls.txt
-
-DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva
-
-STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
-  interp parsing pretyping highparsing toplevel hightactics \
-  coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
-  $(CSDPCERT) coqbinaries $(TOOLS) tools \
-  printers debug initplugins plugins \
-  world install coqide coqide-files coq coqlib \
-  coqlight states check init theories theories-light \
-  $(DOC_TARGETS) $(VO_TARGETS) validate
+###########################################################################
+# Source documentation
+###########################################################################
 
-STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
-  $(DOC_TARGET_PATTERNS)
+OCAMLDOCDIR=dev/ocamldoc
 
-ifndef CM_STAGE1
- STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
-endif
+DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \
+	./pretyping/*.mli ./interp/*.mli \
+	./parsing/*.mli ./proofs/*.mli \
+	./tactics/*.mli ./toplevel/*.mli)
 
+# Defining options to generate dependencies graphs
+DOT=dot
+ODOCDOTOPTS=-dot -dot-reduce
 
 # For emacs: 
 # Local Variables: