Merge branch 'kvx-work' into aarch64-peephole

1 files changed, 75 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 3fd002cc..1289b364 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,12 @@
 #######################################################################
 
 include Makefile.config
+include VERSION
+
+BUILDVERSION ?= $(version)
+BUILDNR ?= $(buildnr)
+TAG ?= $(tag)
+BRANCH ?= $(branch)
 
 ifeq ($(wildcard $(ARCH)_$(BITSIZE)),)
 ARCHDIRS?=$(ARCH)
@@ -23,16 +29,27 @@ endif
 
 BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v
 
-DIRS=lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
-  flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \
-  exportclight MenhirLib cparser
+DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \
+	exportclight cparser
+
+RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
+  cparser
 
-RECDIRS=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \
-  MenhirLib cparser
+COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d))
 
-COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d)))
+ifeq ($(LIBRARY_FLOCQ),local)
+DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754
+RECDIRS += flocq
+COQINCLUDES += -R flocq Flocq
+endif
 
-COQCOPTS ?= -w -undeclared-scope
+ifeq ($(LIBRARY_MENHIRLIB),local)
+DIRS += MenhirLib
+RECDIRS += MenhirLib
+COQINCLUDES += -R MenhirLib MenhirLib
+endif
+
+COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
 COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
 COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
 COQDOC="$(COQBIN)coqdoc"
@@ -46,6 +63,7 @@ GPATH=$(DIRS)
 
 # Flocq
 
+ifeq ($(LIBRARY_FLOCQ),local)
 FLOCQ=\
   Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
   Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
@@ -53,6 +71,9 @@ FLOCQ=\
   Div_sqrt_error.v Mult_error.v Plus_error.v \
   Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
   Binary.v Bits.v
+else
+FLOCQ=
+endif
 
 # General-purpose libraries (in lib/)
 
@@ -136,9 +157,13 @@ PARSER=Cabs.v Parser.v
 
 # MenhirLib
 
+ifeq ($(LIBRARY_MENHIRLIB),local)
 MENHIRLIB=Alphabet.v Automaton.v Grammar.v Interpreter_complete.v \
   Interpreter_correct.v Interpreter.v Main.v Validator_complete.v \
   Validator_safe.v Validator_classes.v
+else
+MENHIRLIB=
+endif
 
 # Putting everything together (in driver/)
 
@@ -168,6 +193,9 @@ endif
 ifeq ($(CLIGHTGEN),true)
 	$(MAKE) clightgen
 endif
+ifeq ($(INSTALL_COQDEV),true)
+	$(MAKE) compcert.config
+endif
 
 proof: $(FILES:.v=.vo)
 
@@ -212,11 +240,25 @@ documentation: $(FILES)
           $(filter-out doc/coq2html cparser/Parser.v, $^)
 
 tools/ndfun: tools/ndfun.ml
+ifeq ($(OCAML_NATIVE_COMP),true)
 	ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml
-tools/modorder: tools/modorder.ml
-	ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
+else
+	ocamlc -o tools/ndfun str.cma tools/ndfun.ml
+endif
+
 tools/compiler_expand: tools/compiler_expand.ml
+ifeq ($(OCAML_NATIVE_COMP),true)
 	ocamlopt -o $@ $+
+	ocamlc -o $@ $+
+else
+endif
+
+tools/modorder: tools/modorder.ml
+ifeq ($(OCAML_NATIVE_COMP),true)
+	ocamlopt -o tools/modorder str.cmxa tools/modorder.ml
+else
+	ocamlc -o tools/modorder str.cma tools/modorder.ml
+endif
 
 latexdoc:
 	cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES)
@@ -254,14 +296,29 @@ compcert.ini: Makefile.config
 	 echo "response_file_style=$(RESPONSEFILE)";) \
         > compcert.ini
 
+compcert.config: Makefile.config
+	(echo "# CompCert configuration parameters"; \
+        echo "COMPCERT_ARCH=$(ARCH)"; \
+        echo "COMPCERT_MODEL=$(MODEL)"; \
+        echo "COMPCERT_ABI=$(ABI)"; \
+        echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \
+        echo "COMPCERT_BITSIZE=$(BITSIZE)"; \
+        echo "COMPCERT_SYSTEM=$(SYSTEM)"; \
+        echo "COMPCERT_VERSION=$(BUILDVERSION)"; \
+        echo "COMPCERT_BUILDNR=$(BUILDNR)"; \
+        echo "COMPCERT_TAG=$(TAG)"; \
+        echo "COMPCERT_BRANCH=$(BRANCH)" \
+        ) > compcert.config
+
 driver/Version.ml: VERSION
-	cat VERSION \
-	| sed -e 's|\(.*\)=\(.*\)|let \1 = \"\2\"|g' \
-	>driver/Version.ml
+	(echo 'let version = "$(BUILDVERSION)"'; \
+         echo 'let buildnr = "$(BUILDNR)"'; \
+         echo 'let tag = "$(TAG)"'; \
+         echo 'let branch = "$(BRANCH)"') > driver/Version.ml
 
 cparser/Parser.v: cparser/Parser.vy
 	@rm -f $@
-	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
+	$(MENHIR) --coq --coq-no-version-check cparser/Parser.vy
 	@chmod a-w $@
 
 depend: $(GENERATED) depend1
@@ -288,6 +345,7 @@ ifeq ($(INSTALL_COQDEV),true)
           install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
 	done
 	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
+	install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
 endif
 
@@ -297,7 +355,7 @@ clean:
 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
 	rm -rf doc/html doc/*.glob
 	rm -f driver/Version.ml
-	rm -f compcert.ini
+	rm -f compcert.ini compcert.config
 	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
 	rm -f $(GENERATED) .depend
@@ -319,6 +377,9 @@ check-proof: $(FILES)
 print-includes:
 	@echo $(COQINCLUDES)
 
+CoqProject:
+	@echo $(COQINCLUDES) > _CoqProject
+
 -include .depend
 
 FORCE: