From 9b175072b04195d612615c68ff379dd09aa06f0f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
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(-)

diff --git a/Makefile.build b/Makefile.build
index e3a74aaeeb..6203dd7599 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 3d4e7829ab..d19cbd6ade 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