From 93817b4c2b8d96d6eb990dcfaf21cf2e8f2375df Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 20 Mar 2018 20:13:59 +0100
Subject: coq_makefile: FLAG make variables should not contain LIBS

---
 tools/CoqMakefile.in | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index e9f64542c1..8ab843fd5a 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -168,9 +168,11 @@ DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 endif
 
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
-COQCHKFLAGS?=-silent -o $(COQLIBS)
+# these flags do NOT contain the libraries, to make them easier to overwrite
+COQFLAGS?=-q $(OPT) $(OTHERFLAGS)
+COQCHKFLAGS?=-silent -o
 COQDOCFLAGS?=-interpolate -utf8
+
 COQDOCLIBS?=$(COQLIBS_NOML)
 
 # The version of Coq being run and the version of coq_makefile that
@@ -384,7 +386,7 @@ quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
 vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
@@ -396,17 +398,17 @@ quick2vo:
 	done); \
 	echo "VIO2VO: $$VIOFILES"; \
 	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
 	fi
 .PHONY: quick2vo
 
 checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: checkproofs
 
 validate: $(VOFILES)
-	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
+	$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
 .PHONY: validate
 
 only: $(TGTS)
@@ -654,15 +656,15 @@ endif
 
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
 
 # FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
-	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
 
 $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
@@ -670,7 +672,7 @@ $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-tim
 
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
 
 $(GFILES): %.g: %.v
 	$(SHOW)'GALLINA $<'
@@ -764,6 +766,7 @@ printenv::
 	@echo 'OCAMLFIND = $(OCAMLFIND)'
 	@echo 'PP = $(PP)'
 	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIB = $(COQLIBS)'
 	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
 	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
 .PHONY:	printenv
-- 
cgit v1.2.3


From b716378fce3611d06060c4f71da4b6d87f89c09c Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 20 Mar 2018 20:25:12 +0100
Subject: coq_makefile: provide variables to override for adding extra flags

---
 tools/CoqMakefile.in | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8ab843fd5a..7bcc340ac7 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -168,10 +168,15 @@ DYNOBJ:=.cmxs
 DYNLIB:=.cmxs
 endif
 
+# these variables are meant to be overriden if you want to add *extra* flags
+COQEXTRAFLAGS?=
+COQCHKEXTRAFLAGS?=
+COQDOCEXTRAFLAGS?=
+
 # these flags do NOT contain the libraries, to make them easier to overwrite
-COQFLAGS?=-q $(OPT) $(OTHERFLAGS)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
+COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS)
+COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
+COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
 
 COQDOCLIBS?=$(COQLIBS_NOML)
 
-- 
cgit v1.2.3


From c0e34f2700f769e87f1449ae27b20e0d0546aec7 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 21 Mar 2018 19:40:30 +0100
Subject: docs

---
 tools/CoqMakefile.in | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 7bcc340ac7..f6539d80be 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -148,7 +148,11 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 
 # Flags #######################################################################
 #
-# We define a bunch of variables combining the parameters
+# We define a bunch of variables combining the parameters.
+# To add additional flags to coq, coqchk or coqdoc, set the
+# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
+# To overwrite the default choice and set your own flags entirely, set the
+# {COQ,COQCHK,COQDOC}FLAGS variable.
 
 SHOW := $(if $(VERBOSE),@true "",@echo "")
 HIDE := $(if $(VERBOSE),,@)
-- 
cgit v1.2.3