From 64fe7f462c4dd204ac5ffaed48edbf9698485d94 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 17 Apr 2020 17:26:15 +0200 Subject: Simplify the generation of driver/Version.ml Don't use sed, just echo the contents of the file. --- Makefile | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index af069e3f..aed0da28 100644 --- a/Makefile +++ b/Makefile @@ -14,6 +14,11 @@ ####################################################################### include Makefile.config +include VERSION + +BUILDVERSION ?= $(version) +BUILDNR ?= $(buildnr) +TAG ?= $(tag) ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) ARCHDIRS=$(ARCH) @@ -220,9 +225,9 @@ compcert.ini: Makefile.config > compcert.ini 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)"';) > driver/Version.ml cparser/Parser.v: cparser/Parser.vy @rm -f $@ -- cgit From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 29 Apr 2020 15:40:13 +0200 Subject: Install "compcert.config" file along the Coq development The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script. --- Makefile | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index aed0da28..df5fb03f 100644 --- a/Makefile +++ b/Makefile @@ -147,6 +147,9 @@ endif ifeq ($(CLIGHTGEN),true) $(MAKE) clightgen endif +ifeq ($(INSTALL_COQDEV),true) + $(MAKE) compcert.config +endif proof: $(FILES:.v=.vo) @@ -224,6 +227,19 @@ 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)" \ + ) > compcert.config + driver/Version.ml: VERSION (echo 'let version = "$(BUILDVERSION)"'; \ echo 'let buildnr = "$(BUILDNR)"'; \ @@ -258,6 +274,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 @@ -267,7 +284,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 -- cgit From 5b8578daeed73483b130618c954abb24afa8ddb9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 19:19:49 +0200 Subject: Preliminary support for Coq 8.12 Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index df5fb03f..d91c5f37 100644 --- a/Makefile +++ b/Makefile @@ -35,7 +35,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) -COQCOPTS ?= -w -undeclared-scope +COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" -- cgit From f8cfbc1bc22c06835e9ea7b0cab41a8f25b523ba Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Jul 2020 14:52:34 +0200 Subject: Introduce additional "branch" build information. --- Makefile | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index d91c5f37..5e97ebbf 100644 --- a/Makefile +++ b/Makefile @@ -19,6 +19,7 @@ include VERSION BUILDVERSION ?= $(version) BUILDNR ?= $(buildnr) TAG ?= $(tag) +BRANCH ?= $(branch) ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) ARCHDIRS=$(ARCH) @@ -238,12 +239,14 @@ compcert.config: Makefile.config echo "COMPCERT_VERSION=$(BUILDVERSION)"; \ echo "COMPCERT_BUILDNR=$(BUILDNR)"; \ echo "COMPCERT_TAG=$(TAG)" \ + echo "COMPCERT_BRANCH=$(BRANCH)" \ ) > compcert.config driver/Version.ml: VERSION (echo 'let version = "$(BUILDVERSION)"'; \ echo 'let buildnr = "$(BUILDNR)"'; \ - echo 'let tag = "$(TAG)"';) > driver/Version.ml + echo 'let tag = "$(TAG)"'; \ + echo 'let branch = "$(BRANCH)"') > driver/Version.ml cparser/Parser.v: cparser/Parser.vy @rm -f $@ -- cgit From 6b854265e261b8c9e2e068364ef1405412b89063 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Jul 2020 10:25:36 +0200 Subject: Bytecode-only build, continued If ocamlopt is not available, use ocamlc instead of ocamlopt to build auxiliary tools (tools/modorder, tools/ndfun). This is a follow-up to commit 9af28924. --- Makefile | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 5e97ebbf..ae095a09 100644 --- a/Makefile +++ b/Makefile @@ -191,9 +191,18 @@ 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 +else + ocamlc -o tools/ndfun str.cma tools/ndfun.ml +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) -- cgit From 72f78307cec2ac8fb33d657b118a930b2acfe8ad Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 15 Jul 2020 11:37:16 +0200 Subject: Added missing semicolon. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ae095a09..127ed5d2 100644 --- a/Makefile +++ b/Makefile @@ -247,7 +247,7 @@ compcert.config: Makefile.config echo "COMPCERT_SYSTEM=$(SYSTEM)"; \ echo "COMPCERT_VERSION=$(BUILDVERSION)"; \ echo "COMPCERT_BUILDNR=$(BUILDNR)"; \ - echo "COMPCERT_TAG=$(TAG)" \ + echo "COMPCERT_TAG=$(TAG)"; \ echo "COMPCERT_BRANCH=$(BRANCH)" \ ) > compcert.config -- cgit From ab0d9476db875a82cf293623d18552b62f239d5c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Sep 2020 14:15:57 +0200 Subject: Support the use of already-installed MenhirLib and Flocq libraries configure flags -use-external-Flocq and -use external-MenhirLib. --- Makefile | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 127ed5d2..4b0b5761 100644 --- a/Makefile +++ b/Makefile @@ -27,14 +27,19 @@ else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ - exportclight MenhirLib cparser +DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser -RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ - MenhirLib cparser +COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d)) -COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 +COQINCLUDES += -R flocq Flocq +endif + +ifeq ($(LIBRARY_MENHIRLIB),local) +DIRS += MenhirLib +COQINCLUDES += -R MenhirLib MenhirLib +endif COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) @@ -50,6 +55,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 \ @@ -57,6 +63,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/) @@ -117,9 +126,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/) @@ -259,7 +272,7 @@ driver/Version.ml: VERSION 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 @@ -318,6 +331,9 @@ check-proof: $(FILES) print-includes: @echo $(COQINCLUDES) +CoqProject: + @echo $(COQINCLUDES) > _CoqProject + -include .depend FORCE: -- cgit