Commit cdb9f34d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean a bit the handling of VERBOSEMAKE.

parent 27451f70
......@@ -12,9 +12,11 @@
VERBOSEMAKE ?= @enable_verbose_make@
ifeq ($(VERBOSEMAKE),yes)
QUIET =
SHOW = @true
HIDE =
else
QUIET = yes
SHOW = @echo
HIDE = @
endif
# install the binaries
......@@ -117,6 +119,8 @@ COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TARGET_EMACS = share/emacs/why3.elc
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
###############
# main target
###############
......@@ -247,20 +251,20 @@ byte: lib/why3/why3.cma
opt: lib/why3/why3.cmxa
lib/why3/why3.cma: lib/why3/why3.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3.cmxa: lib/why3/why3.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
lib/why3/why3.cmo: $(LIBCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3.cmx: $(LIBCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
# clean and depend
......@@ -414,36 +418,36 @@ plugins.byte: $(LIBPLUGCMO)
plugins.opt : $(LIBPLUGCMXS)
lib/plugins/%.cmxs: plugins/parser/%.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/%.cmo: plugins/parser/%.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/%.cmxs: plugins/printer/%.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/%.cmo: plugins/printer/%.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/%.cmxs: plugins/transform/%.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/%.cmo: plugins/transform/%.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/tptp.cmxs: $(TPTPCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/tptp.cmo: $(TPTPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
# depend and clean targets
......@@ -486,68 +490,68 @@ byte: bin/why3.byte $(TOOLS_BIN:%=bin/%.byte)
opt: bin/why3.opt $(TOOLS_BIN:%=bin/%.opt)
bin/why3.opt: lib/why3/why3.cmxa src/tools/main.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3.byte: lib/why3/why3.cma src/tools/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3config.opt: lib/why3/why3.cmxa src/tools/why3config.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3config.byte: lib/why3/why3.cma src/tools/why3config.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3execute.opt: lib/why3/why3.cmxa src/tools/why3execute.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3execute.byte: lib/why3/why3.cma src/tools/why3execute.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3extract.opt: lib/why3/why3.cmxa src/tools/why3extract.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3extract.byte: lib/why3/why3.cma src/tools/why3extract.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/why3realize.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
bin/why3wc.opt: src/tools/why3wc.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3wc.byte: src/tools/why3wc.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
clean_old_install::
rm -f $(TOOLS_BIN:%=$(TOOLDIR)/%$(EXE)) $(BINDIR)/why3$(EXE)
......@@ -708,16 +712,16 @@ bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt: lib/why3/why3.cmxa src/ide/resetgc.o $(IDECMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3ide.byte: lib/why3/why3.cma src/ide/resetgc.o $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
src/ide/resetgc.o: src/ide/resetgc.c
$(if $(QUIET),@echo 'Ocamlc $<' &&) \
$(OCAMLC) -c -ccopt "-Wall -o $@" $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
# depend and clean targets
......@@ -763,12 +767,12 @@ byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: lib/why3/why3.cmxa $(SESSIONCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3session.byte: lib/why3/why3.cma $(SESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -825,25 +829,25 @@ lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cma, @ZIPLIB@)
lib/coq-tactic/why3tac.cma: BFLAGS += $(addsuffix .cmo, @MENHIRLIB@)
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(if $(QUIET),@echo 'Camlp $<' &&) \
$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
$(SHOW) 'Camlp $<'
$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -931,8 +935,8 @@ endif
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV)
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
$(SHOW) 'Generate $@'
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \
for f in $(COQLIBS_INT_FILES); do \
......@@ -1036,12 +1040,12 @@ COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(if $(QUIET),@echo 'Coqc $<' &&) \
$(COQC) -R lib/coq Why3 $<
$(SHOW) 'Coqc $<'
$(HIDE)$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -R lib/coq Why3 $< > $@
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
opt byte: $(COQVO)
......@@ -1104,8 +1108,8 @@ PVSLIBS_FILES = $(PVSLIBS_INT) $(PVSLIBS_REAL) $(PVSLIBS_LIST) \
$(PVSLIBS_NUMBER) $(PVSLIBS_FP)
drivers/pvs-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
$(SHOW) 'Generate $@'
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
for f in $(PVSLIBS_INT_FILES); do \
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
for f in $(PVSLIBS_REAL_FILES); do \
......@@ -1199,8 +1203,8 @@ ISABELLELIBS_BV_FILES = Pow2int BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix lib/isabelle/bv/, $(ISABELLELIBS_BV_FILES)))
drivers/isabelle-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
$(SHOW) 'Generate $@'
$(HIDE)(echo "(* generated automatically at compilation time *)"; \
echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
for f in $(ISABELLELIBS_INT_FILES); do \
echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
......@@ -1341,20 +1345,20 @@ byte: lib/why3/why3extract.cma
opt: lib/why3/why3extract.cmxa
lib/why3/why3extract.cma: lib/why3/why3extract.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) -a $(BFLAGS) -o $@ $^
lib/why3/why3extract.cmxa: lib/why3/why3extract.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -pack -o $@ $^
lib/why3/why3extract.cmx: $(OCAMLLIBS_CMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
install_no_local_lib::
mkdir -p $(OCAMLINSTALLLIB)/why3
......@@ -1440,12 +1444,12 @@ byte: bin/why3doc.byte
opt: bin/why3doc.opt
bin/why3doc.opt: lib/why3/why3.cmxa $(WHY3DOCCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3doc.byte: lib/why3/why3.cma $(WHY3DOCCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
......@@ -1566,40 +1570,40 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
###############
test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
|| (rm -f test-api-logic.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-logic.byte;
test-api-logic.opt: examples/use_api/logic.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-logic.opt > /dev/null) \
|| (rm -f test-api-logic.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-logic.opt
test-api-mlw-tree.byte: examples/use_api/mlw_tree.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f test-api-mlw-tree.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-tree.byte;
test-api-mlw-tree.opt: examples/use_api/mlw_tree.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-mlw-tree.opt > /dev/null) \
|| (rm -f test-api-mlw-tree.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw-tree.opt
test-api-mlw.byte: examples/use_api/mlw.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
|| (rm -f test-api-mlw.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw.byte;
test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api-mlw.opt > /dev/null) \
|| (rm -f test-api-mlw.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2)
@rm -f test-api-mlw.opt
......@@ -1608,15 +1612,15 @@ test-api-mlw.opt: examples/use_api/mlw.ml lib/why3/why3.cmxa
# ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null\
|| (rm -f why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml why3shapes why3shapes.gz
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
$(SHOW) 'Ocamlopt $<'
$(HIDE)($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-session.opt > /dev/null) \
|| (rm -f test-session.opt why3session.xml why3shapes why3shapes.gz; \
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
......@@ -1849,42 +1853,54 @@ clean::
################
%.cmi: %.mli
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
# suppress "unused rec" warning for Menhir-produced files
%.cmo: %.ml %.mly
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) -w -39 $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $(BFLAGS) -w -39 $<
# suppress "unused rec" warning for Menhir-produced files
%.cmx: %.ml %.mly
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) -w -39 $<
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) -w -39 $<
%.cmo: %.ml
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $(BFLAGS) $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $(BFLAGS) $<
%.cmx: %.ml
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) $<
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
%.cma:
$(if $(QUIET),@echo 'Ocamlc -a $@ $^' &&) $(OCAMLC) $(LIBOPT) -a -o $@ $^
$(SHOW) 'Ocamlc -a $@ $^'
$(HIDE)$(OCAMLC) $(LIBOPT) -a -o $@ $^
%.cmxa:
$(if $(QUIET),@echo 'Ocamlopt -a $@ $^' &&) $(OCAMLOPT) $(LIBOPT) -a -o $@ $^
$(SHOW) 'Ocamlopt -a $@ $^'
$(HIDE)$(OCAMLOPT) $(LIBOPT) -a -o $@ $^
%.cmxs: %.ml
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -shared $(OFLAGS) -o $@ $<
%.ml: %.mll
$(if $(QUIET),@echo 'Ocamllex $<' &&) $(OCAMLLEX) $<
$(SHOW) 'Ocamllex $<'
$(HIDE)$(OCAMLLEX) $<
%.ml %.mli: %.mly
$(if $(QUIET),@echo 'Menhir $<' &&) $(MENHIR) --explain --strict $<
$(SHOW) 'Menhir $<'
$(HIDE)$(MENHIR) --explain --strict $<
%.dep: %.ml %.mli
$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $<i $(TOTARGET)
%.dep: %.ml
$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< > $@
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $(TOTARGET)
# .ml4.ml:
# $(CAMLP4) pr_o.cmo -impl $< > $@
......@@ -1986,8 +2002,8 @@ src/config.sh: src/config.sh.in config.status
./config.status chmod --file $@
src/util/config.ml share/Makefile.config: src/config.sh
$(if $(QUIET),@echo 'Generate $@' &&) \
BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
$(SHOW) 'Generate $@'
$(HIDE)BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
clean::
rm -f share/Makefile.config
......
......@@ -65,19 +65,25 @@ test_makejob: $(TEST_MAKEJOB)
################
%.cmi: %.mli
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $<
%.cmo: %.ml
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -c $<
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -c $<
%.cmx: %.ml
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $<
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $<
%.dep: %.ml
$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@
$(SHOW) 'Ocamldep $<'
$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< $<i $(TOTARGET)
%.opt:
$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -linkpkg -o $@ $^
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -linkpkg -o $@ $^
%.byte:
$(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) -linkpkg -o $@ $^
$(SHOW) 'Ocamlc $<'
$(HIDE)$(OCAMLC) -linkpkg -o $@ $^
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment