diff options
| author |  Ralf Jung <post@ralfj.de> | 2018-03-20 20:13:59 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2018-03-20 20:13:59 +0100 |
| commit | 93817b4c2b8d96d6eb990dcfaf21cf2e8f2375df (patch) | |
| tree | 8b6a84c8a29c7071e3209130de5da9dfaf0ad08a /tools | |
| parent | 17c94dca5fe2fc19137b9cac923d51e8eb818041 (diff) | |
coq_makefile: FLAG make variables should not contain LIBS
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e9f64542c..8ab843fd5 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 |