From 10a3ad4074fbc85ca146d44449c1fe433515e3db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Aug 2017 14:01:22 +0200 Subject: coq_makefile: test using findlib's package --- test-suite/coq-makefile/findlib-package/Makefile.local | 3 +++ test-suite/coq-makefile/findlib-package/_CoqProject | 10 ++++++++++ test-suite/coq-makefile/findlib-package/findlib/foo/META | 4 ++++ .../coq-makefile/findlib-package/findlib/foo/Makefile | 14 ++++++++++++++ .../coq-makefile/findlib-package/findlib/foo/foo.mli | 0 .../coq-makefile/findlib-package/findlib/foo/foolib.ml | 2 ++ test-suite/coq-makefile/findlib-package/run.sh | 13 +++++++++++++ 7 files changed, 46 insertions(+) create mode 100644 test-suite/coq-makefile/findlib-package/Makefile.local create mode 100644 test-suite/coq-makefile/findlib-package/_CoqProject create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/META create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/Makefile create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli create mode 100644 test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml create mode 100755 test-suite/coq-makefile/findlib-package/run.sh (limited to 'test-suite') diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local new file mode 100644 index 0000000000..e9c4305567 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -0,0 +1,3 @@ +OCAMLLIBS += -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/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject new file mode 100644 index 0000000000..69f47302e1 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mlpack +src/test.ml4 +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META new file mode 100644 index 0000000000..ff5f1c7c96 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META @@ -0,0 +1,4 @@ +archive(byte)="foo.cma" +archive(native)="foo.cmxa" +linkopts="-linkall" +requires="str" diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile new file mode 100644 index 0000000000..31cf116652 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile @@ -0,0 +1,14 @@ +-include ../../Makefile.conf + +CO=$(COQMF_OCAMLFIND) opt +CB=$(COQMF_OCAMLFIND) ocamlc + +all: + $(CO) -c foolib.ml + $(CO) -a foolib.cmx -o foo.cmxa + $(CB) -c foolib.ml + $(CB) -a foolib.cmo -o foo.cma + $(CB) -c foo.mli # empty .mli file, to be understood + +clean: + rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml new file mode 100644 index 0000000000..81306fb89b --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml @@ -0,0 +1,2 @@ +let foo () = + assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3) diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh new file mode 100755 index 0000000000..a0d8a7fea7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte -- cgit v1.2.3 From 2f335733853a062d0a0e21fa0842750b7b897b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 20 Aug 2017 15:24:53 +0200 Subject: coq_makefile: use dedicated variable for extra packages CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing. --- test-suite/coq-makefile/findlib-package/Makefile.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite') diff --git a/test-suite/coq-makefile/findlib-package/Makefile.local b/test-suite/coq-makefile/findlib-package/Makefile.local index e9c4305567..5373b0219f 100644 --- a/test-suite/coq-makefile/findlib-package/Makefile.local +++ b/test-suite/coq-makefile/findlib-package/Makefile.local @@ -1,3 +1,3 @@ -OCAMLLIBS += -package foo +CAMLPKGS += -package foo CAMLLINK := "$(OCAMLFIND)" ocamlc -rectypes -thread -linkpkg -dontlink str CAMLOPTLINK := "$(OCAMLFIND)" ocamlopt -rectypes -thread -linkpkg -dontlink str -- cgit v1.2.3 From 6e07e3a53e56882043b9db49f03fdf1470a16c46 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Aug 2017 14:56:31 +0200 Subject: coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs --- test-suite/coq-makefile/coqdoc1/run.sh | 1 + test-suite/coq-makefile/coqdoc2/run.sh | 1 + test-suite/coq-makefile/findlib-package/Makefile.local | 2 -- test-suite/coq-makefile/mlpack1/run.sh | 1 + test-suite/coq-makefile/mlpack2/run.sh | 1 + test-suite/coq-makefile/native1/run.sh | 1 + 6 files changed, 5 insertions(+), 2 deletions(-) (limited to 'test-suite') diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 1feff7479b..dc5a500db8 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ sort -u > desired < desired < desired < desired < desired <