diff options
| author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2020-01-03 15:01:12 (GMT) |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2020-01-04 08:33:53 (GMT) |
| commit | af5df6ab27d6d23735359f9852ed6a0aaa43ebc3 (patch) | |
| tree | 991d3bd1d735d90f6aeb54a9c7f5bc4148d582bb /test-suite | |
| parent | 74030dbccac0176ef9a4820d4778834ba3942868 (diff) | |
| download | coq-af5df6ab27d6d23735359f9852ed6a0aaa43ebc3.zip coq-af5df6ab27d6d23735359f9852ed6a0aaa43ebc3.tar.gz coq-af5df6ab27d6d23735359f9852ed6a0aaa43ebc3.tar.bz2 | |
coq_makefile: test with CAMLPKGS and mllib
(cherry picked from commit 665ddac62b7f028f582fbf8fca842e920ed2268c)
Diffstat (limited to 'test-suite')
7 files changed, 51 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local new file mode 100644 index 0000000..0f4a7d9 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject new file mode 100644 index 0000000..cbdb43f --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mllib +src/test.mlg +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META new file mode 100644 index 0000000..ff5f1c7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/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-unpacked/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile new file mode 100644 index 0000000..1615bfd --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/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-unpacked/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml new file mode 100644 index 0000000..81306fb --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/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-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh new file mode 100755 index 0000000..e53a7ed --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +. ../template/init.sh +mv src/test_plugin.mlpack src/test_plugin.mllib + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +if which cygpath 2>/dev/null; then + # the only way I found to pass OCAMLPATH on win is to have it contain + # only one entry + OCAMLPATH=$(cygpath -w "$PWD"/findlib) + export OCAMLPATH +fi +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte |