From 23d46960f4c90a7caaf412504e13d4f4031cbab3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 3 May 2018 15:09:00 +0200
Subject: Add .byte targets for every bestocaml target

This makes it easier to compile our executables for debug purposes.
---
 Makefile.build | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 62 insertions(+), 2 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index ffe605757..7d0785a5b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -240,6 +240,10 @@ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ &&
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^)
 endef
 
+define ocamlbyte
+$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^
+endef
+
 # Camlp5 settings
 
 CAMLP5DEPS:=grammar/grammar.cma
@@ -418,6 +422,10 @@ $(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
+$(COQCBYTE): $(COQCCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, $(SYSMOD))
+
 ###########################################################################
 # other tools
 ###########################################################################
@@ -455,10 +463,18 @@ $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools -package unix)
 
+$(COQDEPBOOTBYTE): $(COQDEPBOOTSRC)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -I tools -package unix)
+
 $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools -package unix)
 
+$(OCAMLLIBDEPBYTE): tools/ocamllibdep.cmo
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call ocamlbyte, -I tools -package unix)
+
 # The full coqdep (unused by this build, but distributed by make install)
 
 COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo	\
@@ -468,24 +484,44 @@ $(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
+$(COQDEPBYTE): $(COQDEPCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, $(SYSMOD))
+
 $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,)
 
+$(GALLINABYTE): tools/gallina_lexer.cmo tools/gallina.cmo
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte,)
+
 COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str,unix,threads)
 
+$(COQMAKEFILEBYTE): $(COQMAKEFILECMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -package str,unix,threads)
+
 $(COQTEX): $(call bestobj, tools/coq_tex.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str)
 
+$(COQTEXBYTE): tools/coq_tex.cmo
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -package str)
+
 $(COQWC): $(call bestobj, tools/coqwc.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str)
 
+$(COQWCBYTE): tools/coqwc.cmo
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -package str)
+
 COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
@@ -493,10 +529,20 @@ $(COQDOC): $(call bestobj, $(COQDOCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package str,unix)
 
-$(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo)
+$(COQDOCBYTE): $(COQDOCCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -package str,unix)
+
+COQWORKMGRCMO:=clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo
+
+$(COQWORKMGR): $(call bestobj, $(COQWORKMGRCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(SYSMOD))
 
+$(COQWORKMGRBYTE): $(COQWORKMGRCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, $(SYSMOD))
+
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
@@ -509,12 +555,22 @@ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I ide -package str,unix,threads)
 
+$(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPLOOPCMA)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -I ide -package str,unix,threads)
+
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: $(call bestobj, clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo)
+VOTOURCMO:=clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo
+
+bin/votour: $(call bestobj, $(VOTOURCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker)
 
+bin/votour.byte: $(VOTOURCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -I checker)
+
 ###########################################################################
 # Csdp to micromega special targets
 ###########################################################################
@@ -527,6 +583,10 @@ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO))
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -package num,unix)
 
+$(CSDPCERTBYTE): $(CSDPCERTCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(call ocamlbyte, -package num,unix)
+
 ###########################################################################
 # tests
 ###########################################################################
-- 
cgit v1.2.3