Commit e4f105d2 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

fixed compilation of Coq plug-in with make -j

test-api no longer depends on why3.cma
parent f1beb06a
...@@ -128,7 +128,8 @@ why3.conf ...@@ -128,7 +128,8 @@ why3.conf
# /src/coq-plugin/ # /src/coq-plugin/
/src/coq-plugin/g_why3tac.ml /src/coq-plugin/g_why3tac.ml
/src/coq-plugin/why3tac.cma /src/coq-plugin/.why3-vo-*
/lib/coq-plugin/why3tac.cma
# /src/driver/ # /src/driver/
/src/driver/driver_lexer.ml /src/driver/driver_lexer.ml
......
...@@ -815,14 +815,8 @@ $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES) ...@@ -815,14 +815,8 @@ $(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
$(COQPDEP): $(COQPGENERATED) $(COQPDEP): $(COQPGENERATED)
byte: lib/coq-plugin/why3tac.cma lib/coq-plugin/Why3.vo byte: src/coq-plugin/.why3-vo-byte
opt: lib/coq-plugin/why3tac.cmxs lib/coq-plugin/Why3.vo opt: src/coq-plugin/.why3-vo-opt
byte: WHY3TAC = lib/coq-plugin/why3tac.cma
opt: WHY3TAC = lib/coq-plugin/why3tac.cmxs
byte: WHY3COQ = $(COQC) -byte
opt: WHY3COQ = $(COQC) -opt
lib/coq-plugin/why3tac.cma: BFLAGS+=-rectypes -I +camlp5 lib/coq-plugin/why3tac.cma: BFLAGS+=-rectypes -I +camlp5
lib/coq-plugin/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5 lib/coq-plugin/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5
...@@ -836,8 +830,13 @@ lib/coq-plugin/why3tac.cma: src/why3.cma $(COQPCMO) ...@@ -836,8 +830,13 @@ lib/coq-plugin/why3tac.cma: src/why3.cma $(COQPCMO)
src/coq-plugin/g_why3tac.ml: src/coq-plugin/g_why3tac.ml4 src/coq-plugin/g_why3tac.ml: src/coq-plugin/g_why3tac.ml4
$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@ $(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
lib/coq-plugin/Why3.vo: lib/coq-plugin/Why3.v $(WHY3TAC) src/coq-plugin/.why3-vo-byte: lib/coq-plugin/Why3.v lib/coq-plugin/why3tac.cma
$(WHY3COQ) -I lib/coq-plugin/ $< $(COQC) -byte -I lib/coq-plugin/ lib/coq-plugin/Why3.v
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
# depend and clean targets # depend and clean targets
...@@ -850,7 +849,9 @@ depend: $(COQPDEP) ...@@ -850,7 +849,9 @@ depend: $(COQPDEP)
clean:: clean::
rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
rm -f lib/coq-plugin/*.cma lib/coq-plugin/*.cmxs rm -f lib/coq-plugin/*.cma lib/coq-plugin/*.cmxs
rm -f lib/coq-plugin/*.vo lib/coq-plugin/*.glob
rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~ rm -f src/coq-plugin/*.annot src/coq-plugin/*.dep src/coq-plugin/*~
rm -f src/coq-plugin/.why3-vo-*
rm -f $(COQPGENERATED) rm -f $(COQPGENERATED)
install_no_local:: install_no_local::
...@@ -1019,7 +1020,7 @@ install_local: bin/why3doc ...@@ -1019,7 +1020,7 @@ install_local: bin/why3doc
.PHONY: bench test .PHONY: bench test
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
$(MAKE) test-api $(MAKE) test-api.@OCAMLBEST@
sh bench/bench \ sh bench/bench \
"bin/why3.@OCAMLBEST@" \ "bin/why3.@OCAMLBEST@" \
"bin/why3ml.@OCAMLBEST@" "bin/why3ml.@OCAMLBEST@"
...@@ -1063,16 +1064,20 @@ testl-ide: bin/why3ide.opt ...@@ -1063,16 +1064,20 @@ testl-ide: bin/why3ide.opt
testl-type: bin/why3ml.byte testl-type: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
test-api: src/why3.cma test-api.byte: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \ ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2) || (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)
@rm -f test-api.opt
test-shape: src/why3.cma test-shape: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml ocaml -I src/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
bts12244: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
################ ################
# documentation # documentation
......
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