diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-08-20 15:24:53 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-08-29 14:25:51 +0200 |
| commit | 2f335733853a062d0a0e21fa0842750b7b897b28 (patch) | |
| tree | 5bc51e733f661b2f6a55cdd79f333518f3b1de48 /tools | |
| parent | 534b8afafc763b382fb3fa747bb95a9a57676d4c (diff) | |
coq_makefile: use dedicated variable for extra packages
CAMLPKGS is now used to hold extra findlib -packages
The previous solution was to use CAMLFLAGS but since 4.05 an
invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx`
fails saying that `useless.cmxa` is not a compilation unit description.
CAMLPKGS is used in all `ocamlopt` invocations but for the one
performing the packing.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6fe6ddeb..9713b8eb5 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -171,6 +171,8 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLPKGS?= CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) @@ -558,46 +560,46 @@ archclean:: $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) -impl $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< $(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) $(FOR_PACK) -impl $< + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< $(MLFILES:.ml=.cmo): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(MLFILES:.ml=.cmx): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FOR_PACK) $< + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) \ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -linkall -shared -o $@ $< $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' @@ -610,7 +612,7 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< ifneq (,$(TIMING)) TIMING_EXTRA = > $<.$(TIMING_EXT) |