diff options
| author | Enrico Tassi | 2017-05-27 19:47:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-05-27 19:47:33 +0200 |
| commit | 7d5873c1008a458247517d0c6200c0004340fd63 (patch) | |
| tree | 13f1cbe8ed70a4438d24e1993d97876e7f89df7b | |
| parent | 9c8cdd5f6c1cb4bda2f8558c17df3ffe69c49264 (diff) | |
coq_makefile: build .cma for each .mlpack
It used to generate only .cmo (the packed one).
While this works if the plugin has no external dependencies,
it does not if it does.
The bug affected only bytecode builds
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc1/run.sh | 1 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc2/run.sh | 1 | ||||
| -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 | 6 |
6 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e071f1db7a..7d82f5fae8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index e071f1db7a..7d82f5fae8 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,6 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 418a2fb775..da4d31cdc4 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/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 418a2fb775..da4d31cdc4 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/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 097bd6398a..b14327a2f8 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -17,6 +17,7 @@ sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 5231899c6e..fb064c495f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -184,7 +184,7 @@ CMOFILES = \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) CMXAFILES = $(CMAFILES:.cma=.cmxa) CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ @@ -474,6 +474,10 @@ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ |