diff options
| author | Gaëtan Gilbert | 2019-02-05 15:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-06 11:17:49 +0100 |
| commit | f29aa6720eba884533972530b4283bf19d8410aa (patch) | |
| tree | 8f48cdb1cf3ccf5218cc7597000675514085ae06 /test-suite | |
| parent | 37b900aeda68ae1e067a7770c16c11ea327a14dc (diff) | |
Makefiles: Fixes for byte compilation
- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files
cf https://github.com/coq/coq/issues/9464
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 24 | ||||
| -rwxr-xr-x | test-suite/misc/poly-capture-global-univs.sh | 2 |
2 files changed, 17 insertions, 9 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 68acb6f04d..03bfc5ffac 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -260,6 +260,7 @@ ifeq ($(LOCAL),true) endif OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) # ML files from unit-test framework, not containing tests UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) @@ -267,24 +268,31 @@ UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) -UNIT_CMXS=utest.cmx +ifneq ($(BEST),opt) +UNIT_LINK:=utest.cmo +OCAMLBEST:=$(OCAMLC) +else +UNIT_LINK:=utest.cmx +OCAMLBEST:=$(OCAMLOPT) +endif unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi $(SHOW) 'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $< +unit-tests/src/utest.cmo: unit-tests/src/utest.ml unit-tests/src/utest.cmi + $(SHOW) 'OCAMLC $<' + $(HIDE)$(OCAMLC) -c -I unit-tests/src -package oUnit $< unit-tests/src/utest.cmi: unit-tests/src/utest.mli - $(SHOW) 'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) -package oUnit $< - -$(UNIT_LOGFILES): unit-tests/src/utest.cmx + $(SHOW) 'OCAMLC $<' + $(HIDE)$(OCAMLC) -package oUnit -c $< unit-tests: $(UNIT_LOGFILES) # Build executable, run it to generate log file -unit-tests/%.ml.log: unit-tests/%.ml +unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \ - -I unit-tests/src $(UNIT_CMXS) $< -o $<.test; + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ + -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test ####################################################################### diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh index e066ac039b..39d20fd524 100755 --- a/test-suite/misc/poly-capture-global-univs.sh +++ b/test-suite/misc/poly-capture-global-univs.sh @@ -11,7 +11,7 @@ coq_makefile -f _CoqProject -o Makefile make clean -make src/evil_plugin.cmxs +make src/evil_plugin.cma if make; then >&2 echo 'Should have failed!' |