From 419e7cac23d7b8ac97d46a6c0d3228d591273d2b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 24 Jun 2016 04:40:34 +0200 Subject: Makefile: no bytecode compilation in make world, see make byte instead On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see a future commit about coq_makefile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first --- Makefile.build | 53 +++++++++++++++++------------------------------------ 1 file changed, 17 insertions(+), 36 deletions(-) (limited to 'Makefile.build') 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 $ Date: Wed, 29 Jun 2016 15:13:13 +0200 Subject: Makefile: $(BEST) controls which coqtop is used to build .vo This allows to grant a wish by Hugo: to build coqtop.byte and prelude with it, you could do: make -j BEST=byte states --- Makefile.build | 4 ++-- Makefile.common | 17 ++++++++++++++++- 2 files changed, 18 insertions(+), 3 deletions(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index e3a74aaee..6203dd759 100644 --- a/Makefile.build +++ b/Makefile.build @@ -108,7 +108,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # TIME="%C (%U user, %S sys, %e total, %M maxres)" COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -190,7 +190,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 diff --git a/Makefile.common b/Makefile.common index 3d4e7829a..d19cbd6ad 100644 --- a/Makefile.common +++ b/Makefile.common @@ -45,7 +45,22 @@ ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) # static link of plugins, do not mention them in .v.d DYNDEP:=-dyndep no else - DYNDEP:=-dyndep $(BEST) + DYNDEP:=-dyndep var +endif + +# Which coqtop do we use to build .vo file ? The best ;-) +# Note: $(BEST) could be overridden by the user if a byte build is desired +# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions +# for Declare ML Module files. + +ifeq ($(BEST),opt) +COQTOPBEST:=$(COQTOPEXE) +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +else +COQTOPBEST:=$(COQTOPBYTE) +DYNOBJ:=.cmo +DYNLIB:=.cma endif INSTALLBIN:=install -- cgit v1.2.3 From fd8c2ff85c098149f11280af5f1a257dd6af3622 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 1 Jun 2017 17:35:58 +0200 Subject: mention 'make world' without 'byte' in CHANGES + 2 minor suggestions --- CHANGES | 9 +++++++++ Makefile | 2 +- Makefile.build | 2 +- 3 files changed, 11 insertions(+), 2 deletions(-) (limited to 'Makefile.build') diff --git a/CHANGES b/CHANGES index 30bea7a7b..7038b490a 100644 --- a/CHANGES +++ b/CHANGES @@ -74,6 +74,15 @@ Tools warnings when a deprecated feature is used. Please upgrade your _CoqProject accordingly. +Build Infrastructure + +- Note that 'make world' does not build the bytecode binaries anymore. + For that, you can use 'make byte' (and 'make install-byte' afterwards). + Warning: native and byte compilations should *not* be mixed in the same + instance of 'make -j', otherwise both ocamlc and ocamlopt might race for + access to the same .cmi files. In short, use "make -j && make -j byte" + instead of "make -j world byte". + Changes from V8.6beta1 to V8.6 ============================== diff --git a/Makefile b/Makefile index 23c6ea638..91b024913 100644 --- a/Makefile +++ b/Makefile @@ -123,7 +123,7 @@ help: @echo " make clean" @echo "or make archclean" @echo "For make to be verbose, add VERBOSE=1" - @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" + @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo @echo "Bytecode compilation is now a separate target:" @echo " make byte" diff --git a/Makefile.build b/Makefile.build index 6203dd759..064f89aa0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -53,7 +53,7 @@ world: coq coqide documentation revision coq: coqlib coqbinaries tools -# Note: 'world' do not build the bytecode binaries anymore. +# Note: 'world' does 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. -- cgit v1.2.3