diff options
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc1/run.sh | 1 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc2/run.sh | 1 | ||||
| -rw-r--r-- | test-suite/coq-makefile/findlib-package/Makefile.local | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/mlpack1/run.sh | 1 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/mlpack2/run.sh | 1 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native1/run.sh | 1 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 12 |
7 files changed, 14 insertions, 5 deletions
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479..dc5a500db 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 1feff7479..dc5a500db 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,6 +15,7 @@ sort -u > desired <<EOT ./test ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.glob ./test/test.v diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local index 5373b0219..0f4a7d995 100644 --- a/test-suite/coq-makefile/findlib-package/Makefile.local +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -1,3 +1 @@ CAMLPKGS += -package foo -CAMLLINK := "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink str -CAMLOPTLINK := "$(OCAMLFIND)" ocamlopt -rectypes -thread -linkpkg -dontlink str diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 51669f28f..03df9cf05 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 51669f28f..03df9cf05 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,6 +15,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3bec11cb7..89bafe9ad 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,6 +18,7 @@ sort > desired <<EOT ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx +./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v ./test/test.vo diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fc8c450ec..e919db4a9 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -592,9 +592,14 @@ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' @@ -611,7 +616,8 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< ifneq (,$(TIMING)) TIMING_EXTRA = > $<.$(TIMING_EXT) |