cosmetic

3634f58d · Andrei Paskevich · cc3461e6 · 3634f58d
Commit 3634f58d authored 13 years ago by Andrei Paskevich
--- a/Makefile.in
+++ b/Makefile.in
@@ -41,7 +41,6 @@ MANDIR  = $(DESTDIR)@mandir@

 # OS specific stuff
 EXE   = @EXE@
-STRIP = true

 # other variables
 CC        = @CC@
@@ -76,12 +75,10 @@ BLINKFLAGS = -linkall $(EXTCMA)

 ifeq (@enable_debug@,yes)
 OFLAGS += -g
-STRIP = true
 endif

 ifeq (@enable_profiling@,yes)
 OFLAGS += -g -p
-STRIP = true
 endif

 # external libraries common to all binaries
@@ -172,16 +169,20 @@ byte: src/why3.cma
 opt:  src/why3.cmxa

 src/why3.cma: src/why3.cmo
-	$(OCAMLC) -a $(BFLAGS) -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) -a $(BFLAGS) -o $@ $^

 src/why3.cmxa: src/why3.cmx
-	$(OCAMLOPT) -a $(OFLAGS) -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) -a $(OFLAGS) -o $@ $^

 src/why3.cmo: $(LIBCMO)
-	$(OCAMLC) $(BFLAGS) -pack -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -pack -o $@ $^

 src/why3.cmx: $(LIBCMX)
-	$(OCAMLOPT) $(OFLAGS) -pack -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -pack -o $@ $^

 # clean and depend

@@ -295,7 +296,7 @@ plugins.byte: $(addsuffix .cmo, $(addprefix lib/plugins/, $(PLUGINS)))
 plugins.opt : $(addsuffix .cmxs, $(addprefix lib/plugins/, $(PLUGINS)))

 lib/plugins/%.cmxs: plugins/parser/%.cmx
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

 lib/plugins/%.cmo: plugins/parser/%.cmo
@@ -303,7 +304,7 @@ lib/plugins/%.cmo: plugins/parser/%.cmo
 	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

 lib/plugins/%.cmxs: plugins/printer/%.cmx
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

 lib/plugins/%.cmo: plugins/printer/%.cmo
@@ -311,7 +312,7 @@ lib/plugins/%.cmo: plugins/printer/%.cmo
 	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

 lib/plugins/%.cmxs: plugins/transform/%.cmx
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $<

 lib/plugins/%.cmo: plugins/transform/%.cmo
@@ -319,7 +320,7 @@ lib/plugins/%.cmo: plugins/transform/%.cmo
 	    $(OCAMLC) $(BFLAGS) -pack -o $@ $<

 lib/plugins/tptp.cmxs: $(TPTPCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -shared -o $@ $^

 lib/plugins/tptp.cmo: $(TPTPCMO)
@@ -362,7 +363,6 @@ opt:  bin/why3.opt
 bin/why3.opt: src/why3.cmxa src/main.cmx
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3.byte: src/why3.cma src/main.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -439,9 +439,8 @@ byte: bin/why3ml.byte
 opt:  bin/why3ml.opt

 bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -539,9 +538,8 @@ byte: bin/why3config.byte
 opt:  bin/why3config.opt

 bin/why3config.opt: src/why3.cmxa $(CONFIGCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3config.byte: src/why3.cma $(CONFIGCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -599,9 +597,8 @@ bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
 bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2

 bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(IDECMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3ide.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(IDECMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -653,9 +650,8 @@ byte: bin/why3replayer.byte
 opt:  bin/why3replayer.opt

 bin/why3replayer.opt: src/why3.cmxa $(PGMCMX) $(REPLAYERCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3replayer.byte: src/why3.cma $(PGMCMO) $(REPLAYERCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -704,9 +700,8 @@ byte: bin/why3session.byte
 opt:  bin/why3session.opt

 bin/why3session.opt: src/why3.cmxa $(PGMCMX) $(SESSIONCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3session.byte: src/why3.cma $(PGMCMO) $(SESSIONCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -760,9 +755,8 @@ bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE
 bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3

 bin/why3bench.opt: src/why3.cmxa $(PGMCMX) $(BENCHCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3bench.byte: src/why3.cma  $(PGMCMO) $(BENCHCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -822,21 +816,26 @@ lib/coq-plugin/why3tac.cma:  BFLAGS+=-rectypes -I +camlp5
 lib/coq-plugin/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5

 lib/coq-plugin/why3tac.cmxs: src/why3.cmxa $(COQPCMX)
-	$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^

 lib/coq-plugin/why3tac.cma: src/why3.cma $(COQPCMO)
-	$(OCAMLC) -a $(BFLAGS) -o $@ $^
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) -a $(BFLAGS) -o $@ $^

 src/coq-plugin/g_why3tac.ml: src/coq-plugin/g_why3tac.ml4
-	$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
+	$(if $(QUIET),@echo 'Camlp5   $<' &&) \
+	    $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@

 src/coq-plugin/.why3-vo-byte: lib/coq-plugin/Why3.v lib/coq-plugin/why3tac.cma
-	$(COQC) -byte -I lib/coq-plugin/ lib/coq-plugin/Why3.v
-	touch src/coq-plugin/.why3-vo-byte
+	$(if $(QUIET),@echo 'Coqc     $<' &&) \
+	    $(COQC) -byte -I lib/coq-plugin/ $< && \
+	    touch src/coq-plugin/.why3-vo-byte

 src/coq-plugin/.why3-vo-opt: lib/coq-plugin/Why3.v lib/coq-plugin/why3tac.cmxs
-	$(COQC) -opt -I lib/coq-plugin/ lib/coq-plugin/Why3.v
-	touch src/coq-plugin/.why3-vo-opt
+	$(if $(QUIET),@echo 'Coqc     $<' &&) \
+	    $(COQC) -opt -I lib/coq-plugin/ $< && \
+	    touch src/coq-plugin/.why3-vo-opt

 # depend and clean targets

@@ -885,17 +884,22 @@ COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
 COQVD = $(addsuffix .vd, $(COQLIBS_FILES))

 %.vo: %.v
-	$(if $(QUIET),@echo 'Coqc $<' &&) $(COQC) -R lib/coq Why3 $<
+	$(if $(QUIET),@echo 'Coqc     $<' &&) \
+	    $(COQC) -R lib/coq Why3 $<

 %.vd: %.v
-	$(if $(QUIET),@echo 'Coqdep $<' &&) $(COQDEP) -slash -R lib/coq Why3 $< > $@
+	$(if $(QUIET),@echo 'Coqdep   $<' &&) \
+	    $(COQDEP) -slash -R lib/coq Why3 $< > $@

 drivers/coq-realizations.aux: Makefile
 	$(if $(QUIET),@echo 'Generate $@' &&) \
 	(echo "(* generated automatically at compilation time *)"; \
-	for f in $(COQLIBS_INT_FILES); do echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
-	for f in $(COQLIBS_REAL_FILES); do echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
-	for f in $(COQLIBS_FP_FILES); do echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
+	for f in $(COQLIBS_INT_FILES); do \
+	echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
+	for f in $(COQLIBS_REAL_FILES); do \
+	echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
+	for f in $(COQLIBS_FP_FILES); do \
+	echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
 	) > $@

 opt byte: $(COQVO)
@@ -983,9 +987,8 @@ byte: bin/why3doc.byte
 opt:  bin/why3doc.opt

 bin/why3doc.opt: src/why3.cmxa $(WHY3DOCCMX)
-	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
-	$(STRIP) $@

 bin/why3doc.byte: src/why3.cma $(WHY3DOCCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
@@ -1021,9 +1024,7 @@ install_local: bin/why3doc

 bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
 	$(MAKE) test-api.@OCAMLBEST@
-	sh bench/bench \
-	    "bin/why3.@OCAMLBEST@" \
-	    "bin/why3ml.@OCAMLBEST@"
+	sh bench/bench "bin/why3.@OCAMLBEST@" "bin/why3ml.@OCAMLBEST@"

 ###############
 # test targets
@@ -1064,15 +1065,16 @@ testl-ide: bin/why3ide.opt
 testl-type: bin/why3ml.byte
 	ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw

-test-api.byte: src/why3.cma
-	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
+test-api.byte: examples/use_api.ml src/why3.cma
+	$(if $(QUIET),@echo 'Ocaml    $<' &&) \
+	ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma $< \
 	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)

-test-api.opt: src/why3.cmxa
-	$(OCAMLOPT) -o $@ -I src/ $(INCLUDES) $(EXTCMXA) src/why3.cmxa \
-	  examples/use_api.ml
-	@./test-api.opt || \
-	  (printf "Test of Why API calls failed. Please fix it"; exit 2)
+test-api.opt: examples/use_api.ml src/why3.cmxa
+	$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
+	($(OCAMLOPT) -o $@ -I src/ $(INCLUDES) $(EXTCMXA) src/why3.cmxa $< \
+	&& ./test-api.opt) \
+	|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
 	@rm -f test-api.opt

 test-shape: src/why3.cma
@@ -1169,10 +1171,10 @@ clean::
 	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -shared $(OFLAGS) -o $@ $<

 %.ml: %.mll
-	$(OCAMLLEX) $<
+	$(if $(QUIET),@echo 'Ocamllex $<' &&) $(OCAMLLEX) $<

 %.ml %.mli: %.mly
-	$(OCAMLYACC) -v $<
+	$(if $(QUIET),@echo 'Ocamlyacc $<' &&) $(OCAMLYACC) -v $<

 %.dep: %.ml
 	$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@
@@ -1365,7 +1367,8 @@ src/config.sh: src/config.sh.in config.status
 	./config.status chmod --file $@

 src/config.ml: src/config.sh
-	LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh
+	$(if $(QUIET),@echo 'Generate $@' &&) \
+	    LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) src/config.sh

 clean::
 	rm -f src/config.ml