From 419e7cac23d7b8ac97d46a6c0d3228d591273d2b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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.common | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index d5f79d76b..3d4e7829a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,10 +41,11 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 # Object and Source files
 ###########################################################################
 
-ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
-  DEPNATDYN:=
+ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
+ # static link of plugins, do not mention them in .v.d
+ DYNDEP:=-dyndep no
 else
-  DEPNATDYN:=-natdynlink no
+ DYNDEP:=-dyndep $(BEST)
 endif
 
 INSTALLBIN:=install
-- 
cgit v1.2.3


From 9b175072b04195d612615c68ff379dd09aa06f0f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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.common')

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