Imported Upstream version 8.5~beta3+dfsg

1 files changed, 13 insertions, 9 deletions

diff --git a/Makefile.build b/Makefile.build
index 018471b6..0455a247 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,7 +69,7 @@ TIMED=          # non-empty will activate a default time command
 
 TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
                 # e.g. "'time -p'"
-
+CAMLFLAGS:=${CAMLFLAGS} -w -3
 # NB: if you want to collect compilation timings of .v and import them
 # in a spreadsheet, I suggest something like:
 #   make TIMED=1 2> timings.csv
@@ -81,7 +81,7 @@ TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
 STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
-COQOPTS=$(COQ_XML) $(VM)
+COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
@@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
 
-ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin)
+ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
 LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
 CODESIGN:=codesign -s -
 else
@@ -282,11 +282,11 @@ $(COQC):  $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
 
 # For the checker, different flags may be used
 
-checker/check.cma: | checker/check.mllib.d
+checker/check.cma: | md5chk checker/check.mllib.d
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^
 
-checker/check.cmxa: | checker/check.mllib.d
+checker/check.cmxa: | md5chk checker/check.mllib.d
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^
 
@@ -479,7 +479,7 @@ md5chk:
 
 VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
 
-validate: $(CHICKEN) md5chk | $(ALLVO)
+validate: $(CHICKEN) | $(ALLVO)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
@@ -524,6 +524,7 @@ hightactics: tactics/hightactics.cma
 .PHONY: init theories theories-light
 .PHONY: logic arith bool narith zarith qarith lists strings sets
 .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
+.PHONY: msets mmaps compat
 
 init: $(INITVO)
 
@@ -551,6 +552,9 @@ classes: $(CLASSESVO)
 program: $(PROGRAMVO)
 structures: $(STRUCTURESVO)
 vectors: $(VECTORSVO)
+msets: $(MSETSVO)
+mmaps: $(MMAPSVO)
+compat: $(COMPATVO)
 
 noreal: unicode logic arith bool zarith qarith lists sets fsets \
 	relations wellfounded setoids sorting
@@ -584,7 +588,7 @@ pluginsbyte: $(PLUGINS)
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
 	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
@@ -654,7 +658,7 @@ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ)
 
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
+bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker,)
 
@@ -1035,7 +1039,7 @@ plugins/%_mod.ml: plugins/%.mllib
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
-	$(HIDE)$(BOOTCOQC) $*
+	$(HIDE)$(BOOTCOQC) $<
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
 	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \