diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-07-04 19:48:05 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-04 19:48:05 +0200 |
commit | b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385 (patch) | |
tree | 32e966816e22fc332007790c48eb810219fe8539 /Makefile.build | |
parent | da99355b4d6de31aec5a660f7afe100190a8e683 (diff) | |
parent | 073178a9821d10b72fe581d3ba7814afd7dfbb05 (diff) |
Merge remote-tracking branch 'github/pr/229' into trunk
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
Diffstat (limited to 'Makefile.build')
-rw-r--r-- | Makefile.build | 57 |
1 files changed, 19 insertions, 38 deletions
diff --git a/Makefile.build b/Makefile.build index ebf2996f1..90834ec8c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -17,9 +17,16 @@ 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 @@ -84,7 +91,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -174,7 +181,7 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(COQTOPEXE) +VO_TOOLS_DEP := $(COQTOPBEST) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif @@ -313,11 +320,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) @@ -503,18 +510,13 @@ test-suite: world $(ALLSTDLIB).v # 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) @@ -530,27 +532,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: @@ -561,11 +542,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 $@' @@ -650,7 +631,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) ########################################################################### |