aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-03 15:09:00 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-03 15:11:13 +0200
commit23d46960f4c90a7caaf412504e13d4f4031cbab3 (patch)
tree541e0d406fb7cdac85fb5485bd941bdfcaace3ca /Makefile.build
parentfad6eee8ddb28fa7840044c65aa02557285e23f0 (diff)
Add .byte targets for every bestocaml target
This makes it easier to compile our executables for debug purposes.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build64
1 files changed, 62 insertions, 2 deletions
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
###########################################################################