diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 53 |
1 files changed, 17 insertions, 36 deletions
diff --git a/Makefile.build b/Makefile.build index 8aedd9cec..e3a74aaee 100644 --- a/Makefile.build +++ b/Makefile.build @@ -51,9 +51,16 @@ COQ_XML ?= world: coq coqide documentation revision -coq: coqlib coqbinaries tools printers +coq: coqlib coqbinaries tools -.PHONY: world coq +# Note: 'world' do not build the bytecode binaries anymore. +# For that, you can use the 'byte' rule. Native and byte compilations +# shouldn't be done in a same make -j... run, otherwise both ocamlc and +# ocamlopt might race for access to the same .cmi files. + +byte: coqbyte coqide-byte pluginsbyte printers + +.PHONY: world coq byte ########################################################################### # Includes @@ -290,11 +297,11 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries +.PHONY: coqbinaries coqbyte -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ - $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) @@ -486,18 +493,13 @@ kernel/kernel.cma: kernel/kernel.mllib # For plugin packs -# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's -# apparently no way to avoid that (no -intf-suffix hack as below). -# We at least ensure that these two commands won't run at the same time, by a fake -# dependency from the packed .cmx to the packed .cmo. - %.cmo: %.mlpack $(SHOW)'OCAMLC -pack -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -%.cmx: %.mlpack %.cmo +%.cmx: %.mlpack $(SHOW)'OCAMLOPT -pack -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^) + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) @@ -513,27 +515,6 @@ COND_OPTFLAGS= \ $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< -## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. -## This can lead to nasty things with make -j. To avoid that: -## 1) We make .cmx always depend on .cmi -## 2) This .cmi will be created from the .mli, or trigger the compilation of the -## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) -## 3) We tell ocamlopt to use the .cmi as the interface source file. With this -## hack, everything goes as if there is a .mli, and the .cmi is preserved -## and the .cmx is checked with respect to this .cmi - -HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) - -define diff - $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) -endef - -MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) - -$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case - -$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo - # NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep # The only exceptions are the sources of the csdpcert binary. # To avoid warnings, we set them manually here: @@ -544,11 +525,11 @@ plugins/micromega/csdpcert_FORPACK:= plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $< %.cmx: %.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $< %.cmxs: %.cmx $(SHOW)'OCAMLOPT -shared -o $@' @@ -633,7 +614,7 @@ endif %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) ########################################################################### |