From ff820359e7adb4a414f4796e342f43b5264580a5 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 next commit about coq_makedile) 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.install | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'Makefile.install') diff --git a/Makefile.install b/Makefile.install index 4dad8cf0d..b4aad7bdd 100644 --- a/Makefile.install +++ b/Makefile.install @@ -61,15 +61,26 @@ endif install-coq: install-binaries install-library install-coq-info install-devfiles +ifeq ($(BEST),byte) +install-coq: install-byte +endif + install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ ifeq ($(BEST),opt) $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif +install-byte: install-ide-byte + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR) + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS) +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif install-tools: $(MKDIR) $(FULLBINDIR) @@ -93,7 +104,7 @@ install-devfiles: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) @@ -101,11 +112,8 @@ endif install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(MKDIR) $(FULLCOQLIB)/user-contrib -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) -- cgit v1.2.3