Imported Upstream version 8.5~beta1+dfsg

1 files changed, 97 insertions, 85 deletions

diff --git a/Makefile.common b/Makefile.common
index 444a7ee5..d752a5be 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -12,28 +12,16 @@
 # Executables
 ###########################################################################
 
-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)
 
-FAKEIDE:=bin/fake_ide$(EXE)
-
 ifeq ($(CAMLP4),camlp4)
 CAMLP4MOD:=camlp4lib
 else
@@ -41,12 +29,8 @@ CAMLP4MOD:=gramlib
 endif
 
 ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
-  DYNLINKCMXA:=dynlink.cmxa
-  NATDYNLINKDEF:=-DHasDynlink
   DEPNATDYN:=
 else
-  DYNLINKCMXA:=
-  NATDYNLINKDEF:=
   DEPNATDYN:=-natdynlink no
 endif
 
@@ -56,8 +40,9 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 COQIDEBYTE:=bin/coqide.byte$(EXE)
-COQIDEOPT:=bin/coqide.opt$(EXE)
 COQIDE:=bin/coqide$(EXE)
+COQIDEAPP:=bin/CoqIDE_$(VERSION).app
+COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 
 ifeq ($(BEST),opt)
 OPT:=opt
@@ -66,35 +51,39 @@ OPT:=
 endif
 
 BESTOBJ:=$(if $(OPT),.cmx,.cmo)
+BESTLIB:=$(if $(OPT),.cmxa,.cma)
+BESTDYN:=$(if $(OPT),.cmxs,.cma)
 
-COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \
-  $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN)
+COQBINARIES:= $(COQMKTOP) \
+  $(COQTOPBYTE) $(COQTOPEXE) \
+  $(CHICKENBYTE) $(CHICKEN)
 
 CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
 CORESRCDIRS:=\
   config 	lib		kernel		kernel/byterun	library \
-  proofs 	tactics 	pretyping	interp		toplevel \
-  parsing
+  proofs 	tactics 	pretyping	interp		stm \
+  toplevel	parsing	printing	grammar	        intf
 
 PLUGINS:=\
-  omega		romega 		micromega 	quote		ring \
-  setoid_ring 	xml 		extraction 	fourier \
-  cc 		funind 		firstorder 	field 		subtac \
-  rtauto 	nsatz           syntax          decl_mode
+  omega		romega 		micromega 	quote \
+  setoid_ring 	extraction 	fourier \
+  cc 		funind 		firstorder 	derive \
+  rtauto 	nsatz           syntax          decl_mode	btauto
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
-  tools 	tools/coqdoc 	scripts		ide/utils	ide \
+  tools 	tools/coqdoc	\
   $(addprefix plugins/, $(PLUGINS))
 
-# Order is relevent here because kernel and checker contain files
+IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
+
+# Order is relevant here because kernel and checker contain files
 # with the same name
-CHKSRCDIRS:= checker lib config kernel
+CHKSRCDIRS:= checker lib config kernel parsing
 
 ###########################################################################
-# tools
+# Tools
 ###########################################################################
 
 COQDEP:=bin/coqdep$(EXE)
@@ -104,8 +93,13 @@ GALLINA:=bin/gallina$(EXE)
 COQTEX:=bin/coq-tex$(EXE)
 COQWC:=bin/coqwc$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
+FAKEIDE:=bin/fake_ide$(EXE)
+COQWORKMGR:=bin/coqworkmgr$(EXE)
+
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
+	$(COQWORKMGR)
 
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
+PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT)
 
 ###########################################################################
 # Documentation
@@ -130,11 +124,11 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-cic.v.tex RefMan-lib.v.tex \
   RefMan-tacex.v.tex RefMan-syn.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
-  RefMan-decl.v.tex RefMan-sch.v.tex \
-  RefMan-pro.v.tex \
-  Cases.v.tex Coercion.v.tex Extraction.v.tex \
+  RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
+  Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Helm.tex Classes.v.tex )
+  Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \
+  Misc.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
@@ -158,8 +152,6 @@ COQRUN := coqrun
 LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
 DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT)
 
-CONFIG:=config/coq_config.cmo
-
 BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
@@ -168,28 +160,27 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \
+CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
-        parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
-        parsing/highparsing.cma tactics/hightactics.cma 
+        parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
+	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
+
+TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
-GRAMMARCMA:=parsing/grammar.cma
+GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
 
 OMEGACMA:=plugins/omega/omega_plugin.cma
 ROMEGACMA:=plugins/romega/romega_plugin.cma
 MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
 QUOTECMA:=plugins/quote/quote_plugin.cma
-RINGCMA:=plugins/ring/ring_plugin.cma
-NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+RINGCMA:=plugins/setoid_ring/newring_plugin.cma
 NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-FIELDCMA:=plugins/field/field_plugin.cma
-XMLCMA:=plugins/xml/xml_plugin.cma
 FOURIERCMA:=plugins/fourier/fourier_plugin.cma
 EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
 FUNINDCMA:=plugins/funind/recdef_plugin.cma
 FOCMA:=plugins/firstorder/ground_plugin.cma
 CCCMA:=plugins/cc/cc_plugin.cma
-SUBTACCMA:=plugins/subtac/subtac_plugin.cma
+BTAUTOCMA:=plugins/btauto/btauto_plugin.cma
 RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
 NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
 OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
@@ -199,17 +190,19 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
 	ascii_syntax_plugin.cma \
         string_syntax_plugin.cma )
 DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
+DERIVECMA:=plugins/derive/derive_plugin.cma
 
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
-        $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
-        $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
-        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
-        $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
+        $(QUOTECMA) $(RINGCMA) \
+        $(FOURIERCMA) $(EXTRACTIONCMA) \
+        $(CCCMA)  $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
+        $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \
+	$(DERIVECMA)
 
 ifneq ($(HASNATDYNLINK),false)
  STATICPLUGINS:=
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
-	$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA)
+	$(FUNINDCMA) $(NATSYNTAXCMA)
  INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
  PLUGINS:=$(PLUGINSCMA)
  PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs)
@@ -221,34 +214,29 @@ else
  PLUGINSOPT:=
 endif
 
-INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
+LINKCMO:=$(CORECMA) $(STATICPLUGINS)
+LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-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
+IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
 IDECMA:=ide/ide.cma
+IDETOPLOOPCMA=ide/coqidetop.cma
 
-LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTDEPS) $(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
+LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
 
 # modules known by the toplevel of Coq
 
-OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib))
+OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
 
 IDEMOD:=$(shell cat ide/ide.mllib)
 
 # coqmktop, coqc
 
-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/errors.cmo lib/system.cmo \
-  lib/envars.cmo
+COQENVCMO:=lib/clib.cma lib/errors.cmo
 
-COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
+COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo
 
-COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo
 
 ## Misc
 
@@ -260,9 +248,11 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
 COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
 
-COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
+COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
+COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
+
 ###########################################################################
 # vo files
 ###########################################################################
@@ -299,13 +289,16 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
 PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
 
 THEORIESVO:=\
-  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
-  $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \
-  $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
-  $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \
-  $(VECTORSVO)
+  $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
+  $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \
+  $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \
+  $(LISTSVO) $(STRINGSVO) \
+  $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
+  $(SETSVO) $(FSETSVO) $(MSETSVO) \
+  $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
+  $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO)
 
-THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
+THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)
 
 ## Plugins
 
@@ -313,21 +306,20 @@ OMEGAVO:=$(call cat_vo_itarget, plugins/omega)
 ROMEGAVO:=$(call cat_vo_itarget, plugins/romega)
 MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega)
 QUOTEVO:=$(call cat_vo_itarget, plugins/quote)
-RINGVO:=$(call cat_vo_itarget, plugins/ring)
-FIELDVO:=$(call cat_vo_itarget, plugins/field)
-NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
+RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
 NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
 FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
 FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
+BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
 RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
 EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
-XMLVO:=
 CCVO:=
+DERIVEVO:=$(call cat_vo_itarget, plugins/derive)
 
-PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
-	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \
-            $(NSATZVO) $(EXTRACTIONVO)
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
+	    $(FOURIERVO) $(CCVO) $(FUNINDVO) \
+	    $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
+            $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO)
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
@@ -337,9 +329,20 @@ ALLSTDLIB := test-suite/misc/universes/all_stdlib
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
 vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+
 ALLMODS:=$(call vo_to_mod,$(ALLVO))
 
-LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
+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)
+
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
 ###########################################################################
@@ -357,15 +360,24 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 
 OCAMLDOCDIR=dev/ocamldoc
 
-DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \
-	./pretyping/*.mli ./interp/*.mli \
+DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
+	./pretyping/*.mli ./interp/*.mli printing/*.mli \
 	./parsing/*.mli ./proofs/*.mli \
-	./tactics/*.mli ./toplevel/*.mli)
+	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli)
 
 # Defining options to generate dependencies graphs
 DOT=dot
 ODOCDOTOPTS=-dot -dot-reduce
 
+###########################################################################
+# GTK for Coqide MacOS bundle
+###########################################################################
+
+GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
+GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
+GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
+
+
 # For emacs: 
 # Local Variables: 
 # mode: makefile